@@ -1990,7 +1990,6 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
1990 set_context ctxt'
1990 set_context ctxt'
1991 updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rFunArgToPArg args) checked) :
1991 updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rFunArgToPArg args) checked) :
1992 new_tyDecls e }
1992 new_tyDecls e }
1994 returnUnit
1993 returnUnit
1995 | n == tacN "prim__DefineFunction", [decl] <- args
1994 | n == tacN "prim__DefineFunction", [decl] <- args
1996 = do defn <- reifyFunDefn decl
1995 = do defn <- reifyFunDefn decl
@@ -2035,17 +2034,23 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
2035 aux <- getAux
2034 aux <- getAux
2036 datatypes <- get_datatypes
2035 datatypes <- get_datatypes
2037 env <- get_env
2036 env <- get_env
2038− (_, ES (p, aux') _ _) <-
2038+ (ctxt', ES (p, aux') _ _) <-
2039 do (ES (current_p, _) _ _) <- get
2039 do (ES (current_p, _) _ _) <- get
2040− lift $ runElab aux (runElabAction ist fc [] script ns)
2041+ (do runElabAction ist fc [] script ns
2042+ ctxt' <- get_context
2041− ((newProof recH ctxt datatypes goalTT)
2044+ ((newProof recH ctxt datatypes goalTT)
2042− { nextname = nextname current_p})
2045+ { nextname = nextname current_p })
2043 let tm_out = getProofTerm (pterm p)
2048 let tm_out = getProofTerm (pterm p)
2044 do (ES (prf, _) s e) <- get
2049 do (ES (prf, _) s e) <- get
2045 let p' = prf { nextname = nextname p }
2050 let p' = prf { nextname = nextname p }
2046 put (ES (p', aux') s e)
2051 put (ES (p', aux') s e)
2047 env' <- get_env
2052 env' <- get_env
2048− (tm, ty, _) <- lift $ recheck ctxt env (forget tm_out) tm_out
2053+ (tm, ty, _) <- lift $ recheck ctxt' env (forget tm_out) tm_out
2049 let (tm', ty') = (reflect tm, reflect ty)
2054 let (tm', ty') = (reflect tm, reflect ty)
2050 fmap fst . checkClosed $
2055 fmap fst . checkClosed $
2051 rawPair (Var $ reflm "TT", Var $ reflm "TT")
2056 rawPair (Var $ reflm "TT", Var $ reflm "TT")