fix: fresh macro scope per command

This commit is contained in:
Sebastian Ullrich 2020-01-09 12:36:18 -05:00 committed by Leonardo de Moura
parent 82078fba84
commit 8d021e0cec

View file

@ -197,7 +197,7 @@ private def elabCommandUsing (stx : Syntax) : List CommandElab → CommandElabM
| Exception.unsupportedSyntax => elabCommandUsing elabFns)
def elabCommandAux (stx : Syntax) : CommandElabM Unit :=
withIncRecDepth stx $ match stx with
withIncRecDepth stx $ withFreshMacroScope $ match stx with
| Syntax.node _ _ => do
s ← get;
let table := (commandElabAttribute.ext.getState s.env).table;