From faedfbe651f9310d74ac63d0145d90a0ae973687 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 21 Mar 2022 17:43:53 +0100
Subject: [PATCH] fix: antiquotation splices early in bootstrapping

---
 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 0a742be120..8927554d00 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -140,7 +140,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
               `(mkSepArray $arr (mkAtom $(getSepFromSplice arg)))
             else pure arr
           let arr ← bindLets arr
-          args := args.append arr
+          args := args.append (appendName := appendName) arr
         else do
           let arg ← quoteSyntax arg
           args := args.push arg