From 12aa5cc461e58afe5465c053ff067387ab95b01f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 13 Mar 2021 17:24:27 -0800 Subject: [PATCH] chore: avoid `!` in keywords --- src/Lean/Elab/Quotation.lean | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean index e51a6430de..03373130b4 100644 --- a/src/Lean/Elab/Quotation.lean +++ b/src/Lean/Elab/Quotation.lean @@ -156,24 +156,24 @@ def stxQuot.expand (stx : Syntax) : TermElabM Syntax := do implementation is "self-stabilizing". It was in fact originally compiled by an unhygienic prototype implementation. -/ -macro "elabStxQuot!" kind:ident : command => +macro "elab_stx_quot" kind:ident : command => `(@[builtinTermElab $kind:ident] def elabQuot : TermElab := adaptExpander stxQuot.expand) -- -elabStxQuot! Parser.Level.quot -elabStxQuot! Parser.Term.quot -elabStxQuot! Parser.Term.funBinder.quot -elabStxQuot! Parser.Term.bracketedBinder.quot -elabStxQuot! Parser.Term.matchDiscr.quot -elabStxQuot! Parser.Tactic.quot -elabStxQuot! Parser.Tactic.quotSeq -elabStxQuot! Parser.Term.stx.quot -elabStxQuot! Parser.Term.prec.quot -elabStxQuot! Parser.Term.attr.quot -elabStxQuot! Parser.Term.prio.quot -elabStxQuot! Parser.Term.doElem.quot -elabStxQuot! Parser.Term.dynamicQuot +elab_stx_quot Parser.Level.quot +elab_stx_quot Parser.Term.quot +elab_stx_quot Parser.Term.funBinder.quot +elab_stx_quot Parser.Term.bracketedBinder.quot +elab_stx_quot Parser.Term.matchDiscr.quot +elab_stx_quot Parser.Tactic.quot +elab_stx_quot Parser.Tactic.quotSeq +elab_stx_quot Parser.Term.stx.quot +elab_stx_quot Parser.Term.prec.quot +elab_stx_quot Parser.Term.attr.quot +elab_stx_quot Parser.Term.prio.quot +elab_stx_quot Parser.Term.doElem.quot +elab_stx_quot Parser.Term.dynamicQuot /- match -/