Finalise terms before evaluation in new-style tactics
This prevents lots of mysterious-looking errors where variables don't
get set in binds.
commit1d64b2c5867d96874e3b46e18938cc223da84ea4
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateMon 2 Mar 2015, 16:54 (12 years ago)
parent212c0bd
src/Idris/ElabTerm.hs+1−1
@@ -1508,7 +1508,7 @@ case_ ind autoSolve ist fn tm = do
15081508runTactical :: FC -> Context -> Env -> Term -> ElabD ()
15091509runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
15101510 where
1511− eval = normaliseAll ctxt env
1511+ eval = normaliseAll ctxt env . finalise
15121512 tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]
15131513 returnUnit = fmap fst $ get_type_val (Var unitCon)
15141514