From 0aa7e4a9f9f68d0d8748265f5e15841523641044 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 28 Dec 2014 14:18:40 -0800
Subject: [PATCH] fix(frontends/lean/pp): option 'pp.private_names' should also
 affect private declarations defined in the current file

---
 src/frontends/lean/pp.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index b8a65afe9..97d252243 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -396,7 +396,8 @@ auto pretty_fn::pp_const(expr const & e) -> result {
     name n = const_name(e);
     if (!m_full_names) {
         if (auto it = is_aliased(n)) {
-            n = *it;
+            if (!m_private_names || !hidden_to_user_name(m_env, n))
+                n = *it;
         } else {
             for (name const & ns : get_namespaces(m_env)) {
                 if (!ns.is_anonymous()) {