Merge pull request #2286 from david-christiansen/wip/tactical
Evaluate Elab scripts in their own environment rather than the internal
commita52c76e08435fb28c5884e6172fe58511385a318
authorDavid Christiansen <david@davidchristiansen.dk>
dateSun 17 May 2015, 15:06 (11 years ago)
parentd1ad414f350697
src/Idris/Elab/Term.hs−1
@@ -1635,7 +1635,6 @@ runTactical ist fc env tm = do tm' <- eval tm
16351635 return ()
16361636 where
16371637 eval tm = do ctxt <- get_context
1638− env <- get_env
16391638 return $ normaliseAll ctxt env (finalise tm)
16401639
16411640 returnUnit = return $ P (DCon 0 0 False) unitCon (P (TCon 0 0) unitTy Erased)