@@ -85,7 +85,8 @@ proofSearch False fromProver ambigok deferonfail depth elab _ nroot [fn] ist
85 isImp (PImp p _ _ _ _) = (True, p)
85 isImp (PImp p _ _ _ _) = (True, p)
86 isImp arg = (True, priority arg) -- try to get all of them by unification
86 isImp arg = (True, priority arg) -- try to get all of them by unification
87proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
87proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
88− = do ty <- goal
89+ ty <- goal
89 argsok <- conArgsOK ty
90 argsok <- conArgsOK ty
90 if ambigok || argsok then
91 if ambigok || argsok then
91 case lookupCtxt nroot (idris_tyinfodata ist) of
92 case lookupCtxt nroot (idris_tyinfodata ist) of