diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean index a62cd4143b..f254f0f4d9 100644 --- a/src/Lean/Elab/Do.lean +++ b/src/Lean/Elab/Do.lean @@ -1451,7 +1451,8 @@ mutual partial def doSeqToCode : List Syntax → M CodeBlock | [] => do liftMacroM mkPureUnitAction - | doElem::doElems => withRef doElem do + | doElem::doElems => withIncRecDepth <| withRef doElem do + checkMaxHeartbeats "'do'-expander" match (← liftMacroM <| expandMacro? doElem) with | some doElem => doSeqToCode (doElem::doElems) | none =>