Expand ! binds in tactics
commit2a1de7a196d7e0acfaeff28d27e9f75771f3ac60
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateFri 20 Feb 2015, 15:41 (12 years ago)
parent933fcbb
src/Idris/DSL.hs+1
@@ -162,6 +162,7 @@ debind b tm = let (tm', (bs, _)) = runState (db' tm) ([], 0) in
162162 db' (PDPair fc p l t r) = do l' <- db' l
163163 r' <- db' r
164164 return (PDPair fc p l' t r')
165+ db' (PRunTactics fc t) = fmap (PRunTactics fc) (db' t)
165166 db' t = return t
166167
167168 dbArg a = do t' <- db' (getTm a)