diff --git a/src/Init/Lean/Elab/Tactic/Basic.lean b/src/Init/Lean/Elab/Tactic/Basic.lean index cd475587af..05759532a3 100644 --- a/src/Init/Lean/Elab/Tactic/Basic.lean +++ b/src/Init/Lean/Elab/Tactic/Basic.lean @@ -177,7 +177,7 @@ partial def evalTactic : Syntax → TacticM Unit -- Syntax quotations can return multiple ones stx.forSepArgsM evalTactic else do - trace `Elab.step stx $ fun _ => stx; + trace `Elab.step stx $ fun _ => stx; s ← get; let table := (tacticElabAttribute.ext.getState s.env).table; let k := stx.getKind;