From b74db2d90261d40c2a6c46d9cbaef2aba6e9bb6f Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 25 Oct 2021 13:11:07 +0200 Subject: [PATCH] feat: update macros for extra info field --- src/Lean/Elab/Binders.lean | 2 +- src/Lean/Elab/Quotation.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean index dfada60b7e..688bb7aff2 100644 --- a/src/Lean/Elab/Binders.lean +++ b/src/Lean/Elab/Binders.lean @@ -55,7 +55,7 @@ partial def quoteAutoTactic : Syntax → TermElabM Syntax else let quotedArg ← quoteAutoTactic arg quotedArgs ← `(Array.push $quotedArgs $quotedArg) - `(Syntax.node $(quote k) $quotedArgs) + `(Syntax.node SourceInfo.none $(quote k) $quotedArgs) | Syntax.atom info val => `(mkAtom $(quote val)) | Syntax.missing => throwError "invalid auto tactic, tactic is missing" diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean index 34716cc4dd..3728d34e95 100644 --- a/src/Lean/Elab/Quotation.lean +++ b/src/Lean/Elab/Quotation.lean @@ -145,7 +145,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax else do let arg ← quoteSyntax arg args := args.push arg - `(Syntax.node $(quote k) $(args.build)) + `(Syntax.node SourceInfo.none $(quote k) $(args.build)) | Syntax.atom _ val => `(Syntax.atom info $(quote val)) | Syntax.missing => throwUnsupportedSyntax