From dd325cfffc07dd4bc2d5c8d266001868f4e31b5d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 4 May 2021 16:46:41 -0700
Subject: [PATCH] fix: `getHeadInfo` ==> `getHeadInfo?`

The generated code was not producing compilation errors because we
have a coercion from `A` to `Option A`
---
 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 4076041fc9..45c31c00a5 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -76,7 +76,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
       getAntiquotTerm 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 (Option.getD (getHeadInfo? $(getAntiquotTerm stx)) info) $(quote val))
       | _                 => throwErrorAt stx "expected token"
     else if isAntiquotSuffixSplice stx && !isEscapedAntiquot stx then
       -- splices must occur in a `many` node