@@ -57,7 +57,7 @@ proofSearch False fromProver elab _ nroot [fn] ist
5757 tryAllFns all_imps
5858 where
5959 -- if nothing worked, make a new metavariable
60− tryAllFns _ | fromProver = cantSolveGoal
60+ tryAllFns [] | fromProver = cantSolveGoal
6161 tryAllFns [] = do attack; defer nroot; solve
6262 tryAllFns (f : fs) = try' (tryFn f) (tryAllFns fs) True
6363
@@ -96,7 +96,7 @@ proofSearch rec fromProver elab fn nroot hints ist
9696 toUN (App f a) = App (toUN f) (toUN a)
9797 toUN t = t
9898
99− psRec _ _ | fromProver = cantSolveGoal
99+ psRec _ 0 | fromProver = cantSolveGoal
100100 psRec rec 0 = do attack; defer nroot; solve --fail "Maximum depth reached"
101101 psRec False d = tryCons d hints
102102 psRec True d = try' (trivial elab ist)