@@ -477,7 +477,6 @@ elab ist info pattern tcgen fn tm
477 where elabArg n t
477 where elabArg n t
478 = do hs <- get_holes
478 = do hs <- get_holes
479 tm <- get_term
479 tm <- get_term
480− t' <- insertCoerce ina t
481 failed' <- -- trace (show (n, t, hs, tm)) $
480 failed' <- -- trace (show (n, t, hs, tm)) $
482 -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $
481 -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $
483 case n `elem` hs of
482 case n `elem` hs of
@@ -485,7 +484,7 @@ elab ist info pattern tcgen fn tm
486-- then try (do focus n; elabE ina t; return failed)
485-- then try (do focus n; elabE ina t; return failed)
487-- (return ((n,(lazy, t)):failed))
486-- (return ((n,(lazy, t)):failed))
488− do focus n; elab' ina t'; return failed
487+ do focus n; elabE ina t; return failed
489 False -> return failed
488 False -> return failed
490 elabArgs ina failed fc r ns args
489 elabArgs ina failed fc r ns args