From b1a59bb1cfa4fe17ede6e119d45f15488e522935 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 15 Jan 2020 17:47:08 +0100 Subject: [PATCH] refactor: simplify quoteSyntax --- src/Init/Lean/Elab/Quotation.lean | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/Init/Lean/Elab/Quotation.lean b/src/Init/Lean/Elab/Quotation.lean index 369ccc5a5c..e9d418a931 100644 --- a/src/Init/Lean/Elab/Quotation.lean +++ b/src/Init/Lean/Elab/Quotation.lean @@ -108,10 +108,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax let preresolved := resolveGlobalName env currNamespace openDecls val ++ preresolved; let val := quote val; -- `scp` is bound in stxQuot.expand - val ← `(addMacroScope $val scp); - let args := quote preresolved; - -- TODO: simplify quotations when we're no longer limited by name resolution in the old frontend - `(Syntax.ident none (String.toSubstring $(quote (toString rawVal))) $val $args) + `(Syntax.ident none (String.toSubstring $(quote (toString rawVal))) (addMacroScope $val scp) $(quote preresolved)) -- if antiquotation, insert contents as-is, else recurse | stx@(Syntax.node k args) => if isAntiquot stx then