git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2286 from david-christiansen/wip/tactical
a52c76eDavid Christiansen
src/Idris/Elab/Term.hs−1
compare with master
unifiedsplit
@@ -1635,7 +1635,6 @@ runTactical ist fc env tm = do tm' <- eval tm
1635 return ()
1635 return ()
1636 where
1636 where
1637 eval tm = do ctxt <- get_context
1637 eval tm = do ctxt <- get_context
1638− env <- get_env
1639 return $ normaliseAll ctxt env (finalise tm)
1638 return $ normaliseAll ctxt env (finalise tm)
1640
1639
1641 returnUnit = return $ P (DCon 0 0 False) unitCon (P (TCon 0 0) unitTy Erased)
1640 returnUnit = return $ P (DCon 0 0 False) unitCon (P (TCon 0 0) unitTy Erased)