@@ -1990,7 +1990,6 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
19901990 set_context ctxt'
19911991 updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rFunArgToPArg args) checked) :
19921992 new_tyDecls e }
1993− aux <- getAux
19941993 returnUnit
19951994 | n == tacN "prim__DefineFunction", [decl] <- args
19961995 = do defn <- reifyFunDefn decl
@@ -2035,17 +2034,23 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
20352034 aux <- getAux
20362035 datatypes <- get_datatypes
20372036 env <- get_env
2038− (_, ES (p, aux') _ _) <-
2037+
2038+ (ctxt', ES (p, aux') _ _) <-
20392039 do (ES (current_p, _) _ _) <- get
2040− lift $ runElab aux (runElabAction ist fc [] script ns)
2041− ((newProof recH ctxt datatypes goalTT)
2042− { nextname = nextname current_p})
2040+ lift $ runElab aux
2041+ (do runElabAction ist fc [] script ns
2042+ ctxt' <- get_context
2043+ return ctxt')
2044+ ((newProof recH ctxt datatypes goalTT)
2045+ { nextname = nextname current_p })
2046+ set_context ctxt'
2047+
20432048 let tm_out = getProofTerm (pterm p)
20442049 do (ES (prf, _) s e) <- get
20452050 let p' = prf { nextname = nextname p }
20462051 put (ES (p', aux') s e)
20472052 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
20492054 let (tm', ty') = (reflect tm, reflect ty)
20502055 fmap fst . checkClosed $
20512056 rawPair (Var $ reflm "TT", Var $ reflm "TT")