From 0272c30b4bebb5353ce89fb240fe990dc97df9de Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 1 Aug 2022 23:31:19 +0200 Subject: [PATCH] fix: token antiquotations should create synthetic positions synthetic means synthetic means synthetic --- src/Lean/Elab/Quotation.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean index b433ae1662..091118aab4 100644 --- a/src/Lean/Elab/Quotation.lean +++ b/src/Lean/Elab/Quotation.lean @@ -112,7 +112,7 @@ private partial def quoteSyntax : Syntax → TermElabM Term `(@TSyntax.raw $(quote <| ks.map (·.1)) $(getAntiquotTerm (getCanonicalAntiquot stx))) else if isTokenAntiquot stx && !isEscapedAntiquot stx then match stx[0] with - | Syntax.atom _ val => `(Syntax.atom (Option.getD (getHeadInfo? $(getAntiquotTerm stx)) info) $(quote val)) + | Syntax.atom _ val => `(Syntax.atom (SourceInfo.fromRef $(getAntiquotTerm stx)) $(quote val)) | _ => throwErrorAt stx "expected token" else if isAntiquotSuffixSplice stx && !isEscapedAntiquot (getCanonicalAntiquot (getAntiquotSuffixSpliceInner stx)) then -- splices must occur in a `many` node