From 747262e49817a12744567fb35a90c02712e26ec2 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 19 Mar 2026 10:16:48 +0100
Subject: [PATCH] fix: respect `pp.privateNames` in `#print` signature (#12979)

This PR makes `#print` show the full internal private name (including
module prefix) in the declaration signature when `pp.privateNames` is
set to true. Previously, `pp.privateNames` only affected names in the
body but the signature always stripped the private prefix.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
---
 src/Lean/Elab/Print.lean     |  2 +-
 tests/elab/printPrivate.lean | 48 ++++++++++++++++++++++++++++++++++++
 2 files changed, 49 insertions(+), 1 deletion(-)
 create mode 100644 tests/elab/printPrivate.lean

diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean
index a5eaad4606..de72a3a601 100644
--- a/src/Lean/Elab/Print.lean
+++ b/src/Lean/Elab/Print.lean
@@ -50,7 +50,7 @@ private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type
   let id' ← match privateToUserName? id with
     | some id' =>
       m := m ++ "private "
-      pure id'
+      if getPPPrivateNames (← getOptions) then pure id else pure id'
     | none =>
       pure id
 
diff --git a/tests/elab/printPrivate.lean b/tests/elab/printPrivate.lean
new file mode 100644
index 0000000000..f3bd583764
--- /dev/null
+++ b/tests/elab/printPrivate.lean
@@ -0,0 +1,48 @@
+module
+
+-- Test that `pp.privateNames` affects the name in the output of `#print`, `#print sig`, and `#check`.
+
+private def foo : Nat := 42
+
+-- Without pp.privateNames, commands show the user name
+/--
+info: private def foo : Nat :=
+42
+-/
+#guard_msgs in
+#print foo
+
+/--
+info: private def foo : Nat
+-/
+#guard_msgs in
+#print sig foo
+
+/--
+info: foo : Nat
+-/
+#guard_msgs in
+#check @foo
+
+-- With pp.privateNames, commands should show the full private name
+set_option pp.privateNames true in
+/--
+info: private def _private.elab.printPrivate.0.foo : Nat :=
+42
+-/
+#guard_msgs in
+#print foo
+
+set_option pp.privateNames true in
+/--
+info: private def _private.elab.printPrivate.0.foo : Nat
+-/
+#guard_msgs in
+#print sig foo
+
+set_option pp.privateNames true in
+/--
+info: _private.elab.printPrivate.0.foo : Nat
+-/
+#guard_msgs in
+#check @foo