@@ -57,7 +57,7 @@ proofSearch False fromProver elab _ nroot [fn] ist
57 tryAllFns all_imps
57 tryAllFns all_imps
59 -- if nothing worked, make a new metavariable
59 -- if nothing worked, make a new metavariable
60− tryAllFns _ | fromProver = cantSolveGoal
60+ tryAllFns [] | fromProver = cantSolveGoal
61 tryAllFns [] = do attack; defer nroot; solve
61 tryAllFns [] = do attack; defer nroot; solve
62 tryAllFns (f : fs) = try' (tryFn f) (tryAllFns fs) True
62 tryAllFns (f : fs) = try' (tryFn f) (tryAllFns fs) True
@@ -96,7 +96,7 @@ proofSearch rec fromProver elab fn nroot hints ist
96 toUN (App f a) = App (toUN f) (toUN a)
96 toUN (App f a) = App (toUN f) (toUN a)
97 toUN t = t
97 toUN t = t
99− psRec _ _ | fromProver = cantSolveGoal
99+ psRec _ 0 | fromProver = cantSolveGoal
100 psRec rec 0 = do attack; defer nroot; solve --fail "Maximum depth reached"
100 psRec rec 0 = do attack; defer nroot; solve --fail "Maximum depth reached"
101 psRec False d = tryCons d hints
101 psRec False d = tryCons d hints
102 psRec True d = try' (trivial elab ist)
102 psRec True d = try' (trivial elab ist)