diff options
| author | kr.angelov <kr.angelov@gmail.com> | 2011-09-21 13:30:09 +0000 |
|---|---|---|
| committer | kr.angelov <kr.angelov@gmail.com> | 2011-09-21 13:30:09 +0000 |
| commit | 89fb9a7fdfc3b1be52026ce3b0badf7889a407b6 (patch) | |
| tree | 140957dfae389c539f5955dc646c9516745112d2 /src/runtime/haskell | |
| parent | 958e81126d9bee7d190e738102836918f37b756b (diff) | |
fix in the proof search. when we start the generation from a template, we must start the refinement from the expression that the typecheker generated
Diffstat (limited to 'src/runtime/haskell')
| -rw-r--r-- | src/runtime/haskell/PGF/TypeCheck.hs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/runtime/haskell/PGF/TypeCheck.hs b/src/runtime/haskell/PGF/TypeCheck.hs index 237721aa6..890e77bb4 100644 --- a/src/runtime/haskell/PGF/TypeCheck.hs +++ b/src/runtime/haskell/PGF/TypeCheck.hs @@ -574,7 +574,7 @@ checkResolvedMetaStore scope e = do generateForMetas :: Selector s => (Scope -> TType -> TcM s Expr) -> Expr -> TcM s Expr generateForMetas prove e = do - infExpr emptyScope e + (e,_) <- infExpr emptyScope e fillinVariables refineExpr e where |