@@ -147,6 +147,8 @@ getUnifyLog :: Elab' aux Bool
147getUnifyLog = do ES (ps, a) l p <- get
147getUnifyLog = do ES (ps, a) l p <- get
148 return (unifylog ps)
148 return (unifylog ps)
150+-- | Process a tactic within the current elaborator state
151+processTactic' :: Tactic -> Elab' aux ()
150processTactic' t = do ES (p, a) logs prev <- get
152processTactic' t = do ES (p, a) logs prev <- get
151 (p', log) <- lift $ processTactic t p
153 (p', log) <- lift $ processTactic t p
152 put (ES (p', a) (logs ++ log) prev)
154 put (ES (p', a) (logs ++ log) prev)