@@ -483,7 +483,7 @@ elab ist info pattern tcgen fn tm
484-- then try (do focus n; elabE ina t; return failed)
484-- then try (do focus n; elabE ina t; return failed)
485-- (return ((n,(lazy, t)):failed))
485-- (return ((n,(lazy, t)):failed))
486− do focus n; elabE ina t'; return failed
486+ do focus n; elab' ina t'; return failed
487 False -> return failed
487 False -> return failed
488 elabArgs ina failed fc r ns args
488 elabArgs ina failed fc r ns args