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