git.iko.soy/Idris-dev
on master help sign in
Evaluate Elab scripts in their own environment rather than the internal

reflected environment

commitf3506976d1ed2fc2e17a9eeada1083263df2b01a authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSun 17 May 2015, 12:07 (11 years ago) parentfc709fe
1 file changed−1
compare with master
unifiedsplit
src/Idris/Elab/Term.hs−1
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)