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

@@ -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
 

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