From cd729660edf551493e6770ef6c66c77a4fc5babb Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 19 Aug 2025 11:07:48 +0200 Subject: [PATCH] chore: allow quoting private names from inside public scope (#9985) --- src/Lean/Elab/BuiltinTerm.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean index d98296d30d..1e6e11cc4e 100644 --- a/src/Lean/Elab/BuiltinTerm.lean +++ b/src/Lean/Elab/BuiltinTerm.lean @@ -238,7 +238,8 @@ def elabScientificLit : TermElab := fun stx expectedType? => do | none => throwIllFormedSyntax @[builtin_term_elab doubleQuotedName] def elabDoubleQuotedName : TermElab := fun stx _ => - return toExpr (← realizeGlobalConstNoOverloadWithInfo stx[2]) + -- Always allow quoting private names. + return toExpr (← withoutExporting <| realizeGlobalConstNoOverloadWithInfo stx[2]) @[builtin_term_elab declName] def elabDeclName : TermElab := adaptExpander fun _ => do let some declName ← getDeclName?