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