Fix scoping error in proof scripts
Fixes issue #106
commit32c81043498a6ec168e01716a6c6a49915419462
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateThu 29 Nov 2012, 00:39 (14 years ago)
parent817211a
src/Idris/ElabTerm.hs+3−1
@@ -553,7 +553,9 @@ collectDeferred t = return t
553553-- Running tactics directly
554554
555555runTac :: 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)
558+ where
557559 runT (Intro []) = do g <- goal
558560 attack; intro (bname g)
559561 where