@@ -477,7 +477,6 @@ elab ist info pattern tcgen fn tm
477477 where elabArg n t
478478 = do hs <- get_holes
479479 tm <- get_term
480− t' <- insertCoerce ina t
481480 failed' <- -- trace (show (n, t, hs, tm)) $
482481 -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $
483482 case n `elem` hs of
@@ -485,7 +484,7 @@ elab ist info pattern tcgen fn tm
485484-- if r
486485-- then try (do focus n; elabE ina t; return failed)
487486-- (return ((n,(lazy, t)):failed))
488− do focus n; elab' ina t'; return failed
487+ do focus n; elabE ina t; return failed
489488 False -> return failed
490489 elabArgs ina failed fc r ns args
491490