From 89fb9a7fdfc3b1be52026ce3b0badf7889a407b6 Mon Sep 17 00:00:00 2001 From: "kr.angelov" Date: Wed, 21 Sep 2011 13:30:09 +0000 Subject: 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 --- src/runtime/haskell/PGF/TypeCheck.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/runtime') 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 -- cgit v1.2.3