Readded solveAll
commit86e32fbd5c687ef4f1387704e7014ae256aa650e
authorAhmad Salim Al-Sibahi <asal@itu.dk>
dateTue 10 Dec 2013, 13:23 (13 years ago)
parent5bc16ae
src/Idris/ElabTerm.hs+1−1
@@ -842,7 +842,7 @@ runTac autoSolve ist tac
842842 when autoSolve solveAll
843843 runT (Induction nm)
844844 = do induction nm
845− -- when autoSolve solveAll
845+ when autoSolve solveAll
846846 runT (LetTac n tm)
847847 = do attack
848848 tyn <- unique_hole (MN 0 "letty")