git.iko.soy/Idris-dev
on master help sign in
Finalise terms before evaluation in new-style tactics
1d64b2cDavid Raymond Christiansen
src/Idris/ElabTerm.hs+1−1
compare with master
unifiedsplit
@@ -1508,7 +1508,7 @@ case_ ind autoSolve ist fn tm = do
1508runTactical :: FC -> Context -> Env -> Term -> ElabD ()
1508runTactical :: FC -> Context -> Env -> Term -> ElabD ()
1509runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
1509runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
1510 where
1510 where
1511− eval = normaliseAll ctxt env
1511+ eval = normaliseAll ctxt env . finalise
1512 tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]
1512 tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]
1513 returnUnit = fmap fst $ get_type_val (Var unitCon)
1513 returnUnit = fmap fst $ get_type_val (Var unitCon)
1514
1514