michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean/pp): option 'pp.private_names' should also affect private declarations defined in the current file

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-28 14:18:40 -08:00
parent d082fb7402
commit 0aa7e4a9f9
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/frontends/lean/pp.cpp
View file

@ -396,7 +396,8 @@ auto pretty_fn::pp_const(expr const & e) -> result {
name n = const_name(e); name n = const_name(e);
if (!m_full_names) { if (!m_full_names) {
if (auto it = is_aliased(n)) { if (auto it = is_aliased(n)) {
n = *it; if (!m_private_names || !hidden_to_user_name(m_env, n))
n = *it;
} else { } else {
for (name const & ns : get_namespaces(m_env)) { for (name const & ns : get_namespaces(m_env)) {
if (!ns.is_anonymous()) { if (!ns.is_anonymous()) {