@@ -553,7 +553,9 @@ collectDeferred t = return t
553-- Running tactics directly
553-- Running tactics directly
555runTac :: Bool -> IState -> PTactic -> ElabD ()
555runTac :: Bool -> IState -> PTactic -> ElabD ()
556−runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where
556+runTac autoSolve ist tac = do env <- get_env
557+ runT (fmap (addImplBound ist (map fst env)) tac)
557 runT (Intro []) = do g <- goal
559 runT (Intro []) = do g <- goal
558 attack; intro (bname g)
560 attack; intro (bname g)