From 0c668a31feedf8a57caec5d67ae6b410030b326d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Jul 2014 10:58:13 -0700 Subject: [PATCH] fix(frontends/lean/pp): display private 'internal' names in a human readable way Signed-off-by: Leonardo de Moura --- src/frontends/lean/pp.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index bd8260bce..43259170f 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "library/coercion.h" #include "library/expr_pair.h" #include "library/placeholder.h" +#include "library/private.h" #include "frontends/lean/pp.h" #include "frontends/lean/pp_options.h" #include "frontends/lean/token_table.h" @@ -175,6 +176,8 @@ auto pretty_fn::pp_const(expr const & e) -> result { } } } + 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;