@@ -132,9 +132,10 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
132 psRec _ 0 | fromProver = cantSolveGoal
132 psRec _ 0 | fromProver = cantSolveGoal
133 psRec rec 0 = do attack; defer [] nroot; solve --fail "Maximum depth reached"
133 psRec rec 0 = do attack; defer [] nroot; solve --fail "Maximum depth reached"
134 psRec False d = tryCons d hints
134 psRec False d = tryCons d hints
135+ psRec True d = do compute
135− psRec True d = try' (trivial elab ist)
136+ try' (trivial elab ist)
136− (try' (try' (resolveByCon (d - 1)) (resolveByLocals (d - 1))
137+ (try' (try' (resolveByCon (d - 1)) (resolveByLocals (d - 1))
138 -- if all else fails, make a new metavariable
139 -- if all else fails, make a new metavariable
139 (if fromProver
140 (if fromProver
140 then cantSolveGoal
141 then cantSolveGoal