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