@@ -348,7 +348,8 @@ elab ist info emode opts fn tm
348 try' e1 (trySeq' e1 xs) True
348 try' e1 (trySeq' e1 xs) True
349 trySeq' deferr [] = proofFail deferr
349 trySeq' deferr [] = proofFail deferr
350 trySeq' deferr (x : xs)
350 trySeq' deferr (x : xs)
351− = try' (elab' ina fc x) (trySeq' deferr xs) True
351+ = try' (do elab' ina fc x
352+ solveAutos ist fn False) (trySeq' deferr xs) True
352 elab' ina _ (PPatvar fc n) | bindfree = do patvar n; -- update_term liftPats
353 elab' ina _ (PPatvar fc n) | bindfree = do patvar n; -- update_term liftPats
353-- elab' (_, _, inty) (PRef fc f)
354-- elab' (_, _, inty) (PRef fc f)
354-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty
355-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty