diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 43259170f..3954f8cfd 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -95,15 +95,16 @@ expr pretty_fn::purify(expr const & e) {
 }
 
 void pretty_fn::set_options(options const & o) {
-    m_indent     = get_pp_indent(o);
-    m_max_depth  = get_pp_max_depth(o);
-    m_max_steps  = get_pp_max_steps(o);
-    m_implict    = get_pp_implicit(o);
-    m_unicode    = get_pp_unicode(o);
-    m_coercion   = get_pp_coercion(o);
-    m_notation   = get_pp_notation(o);
-    m_universes  = get_pp_universes(o);
-    m_full_names = get_pp_full_names(o);
+    m_indent        = get_pp_indent(o);
+    m_max_depth     = get_pp_max_depth(o);
+    m_max_steps     = get_pp_max_steps(o);
+    m_implict       = get_pp_implicit(o);
+    m_unicode       = get_pp_unicode(o);
+    m_coercion      = get_pp_coercion(o);
+    m_notation      = get_pp_notation(o);
+    m_universes     = get_pp_universes(o);
+    m_full_names    = get_pp_full_names(o);
+    m_private_names = get_pp_private_names(o);
 }
 
 format pretty_fn::pp_level(level const & l) {
@@ -176,8 +177,10 @@ auto pretty_fn::pp_const(expr const & e) -> result {
             }
         }
     }
-    if (auto n1 = hidden_to_user_name(m_env, n))
-        n = *n1;
+    if (!m_private_names) {
+        if (auto n1 = hidden_to_user_name(m_env, n))
+            n = *n1;
+    }
     if (m_universes && !empty(const_levels(e))) {
         format r = compose(format(n), format(".{"));
         bool first = true;
diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h
index f7fb341f4..d42f2e934 100644
--- a/src/frontends/lean/pp.h
+++ b/src/frontends/lean/pp.h
@@ -38,6 +38,7 @@ private:
     bool               m_notation;
     bool               m_universes;
     bool               m_full_names;
+    bool               m_private_names;
 
     void set_options(options const & o);
 
diff --git a/src/frontends/lean/pp_options.cpp b/src/frontends/lean/pp_options.cpp
index 48d6906d3..8d3d395d7 100644
--- a/src/frontends/lean/pp_options.cpp
+++ b/src/frontends/lean/pp_options.cpp
@@ -34,6 +34,10 @@ Author: Leonardo de Moura
 #define LEAN_DEFAULT_PP_FULL_NAMES false
 #endif
 
+#ifndef LEAN_DEFAULT_PP_PRIVATE_NAMES
+#define LEAN_DEFAULT_PP_PRIVATE_NAMES false
+#endif
+
 namespace lean {
 static name g_pp_max_depth        {"pp", "max_depth"};
 static name g_pp_max_steps        {"pp", "max_steps"};
@@ -42,6 +46,7 @@ static name g_pp_implicit         {"pp", "implicit"};
 static name g_pp_coercion         {"pp", "coercion"};
 static name g_pp_universes        {"pp", "universes"};
 static name g_pp_full_names       {"pp", "full_names"};
+static name g_pp_private_names    {"pp", "private_names"};
 
 RegisterUnsignedOption(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH,
                        "(pretty printer) maximum expression depth, after that it will use ellipsis");
@@ -57,12 +62,15 @@ RegisterBoolOption(g_pp_universes,  LEAN_DEFAULT_PP_UNIVERSES,
                    "(pretty printer) display universes");
 RegisterBoolOption(g_pp_full_names,  LEAN_DEFAULT_PP_FULL_NAMES,
                    "(pretty printer) display fully qualified names");
+RegisterBoolOption(g_pp_private_names,  LEAN_DEFAULT_PP_PRIVATE_NAMES,
+                   "(pretty printer) display internal names assigned to private declarations");
 
-unsigned get_pp_max_depth(options const & opts)  { return opts.get_unsigned(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH); }
-unsigned get_pp_max_steps(options const & opts)  { return opts.get_unsigned(g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); }
-bool     get_pp_notation(options const & opts)   { return opts.get_bool(g_pp_notation, LEAN_DEFAULT_PP_NOTATION); }
-bool     get_pp_implicit(options const & opts)   { return opts.get_bool(g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT); }
-bool     get_pp_coercion(options const & opts)   { return opts.get_bool(g_pp_coercion, LEAN_DEFAULT_PP_COERCION); }
-bool     get_pp_universes(options const & opts)  { return opts.get_bool(g_pp_universes, LEAN_DEFAULT_PP_UNIVERSES); }
-bool     get_pp_full_names(options const & opts) { return opts.get_bool(g_pp_full_names, LEAN_DEFAULT_PP_FULL_NAMES); }
+unsigned get_pp_max_depth(options const & opts)     { return opts.get_unsigned(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH); }
+unsigned get_pp_max_steps(options const & opts)     { return opts.get_unsigned(g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); }
+bool     get_pp_notation(options const & opts)      { return opts.get_bool(g_pp_notation, LEAN_DEFAULT_PP_NOTATION); }
+bool     get_pp_implicit(options const & opts)      { return opts.get_bool(g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT); }
+bool     get_pp_coercion(options const & opts)      { return opts.get_bool(g_pp_coercion, LEAN_DEFAULT_PP_COERCION); }
+bool     get_pp_universes(options const & opts)     { return opts.get_bool(g_pp_universes, LEAN_DEFAULT_PP_UNIVERSES); }
+bool     get_pp_full_names(options const & opts)    { return opts.get_bool(g_pp_full_names, LEAN_DEFAULT_PP_FULL_NAMES); }
+bool     get_pp_private_names(options const & opts) { return opts.get_bool(g_pp_private_names, LEAN_DEFAULT_PP_PRIVATE_NAMES); }
 }
diff --git a/src/frontends/lean/pp_options.h b/src/frontends/lean/pp_options.h
index 03e0f496b..f0a0569b8 100644
--- a/src/frontends/lean/pp_options.h
+++ b/src/frontends/lean/pp_options.h
@@ -14,4 +14,5 @@ bool     get_pp_implicit(options const & opts);
 bool     get_pp_coercion(options const & opts);
 bool     get_pp_universes(options const & opts);
 bool     get_pp_full_names(options const & opts);
+bool     get_pp_private_names(options const & opts);
 }