diff --git a/src/frontends/lean/parser_cmds.cpp b/src/frontends/lean/parser_cmds.cpp index 3b0f2ad5a..20693da89 100644 --- a/src/frontends/lean/parser_cmds.cpp +++ b/src/frontends/lean/parser_cmds.cpp @@ -830,7 +830,7 @@ void parser_imp::parse_using() { if (it != m_using_decls.end()) diagnostic(m_io_state) << "warning: " << n << " will shadow " << it->second << endl; auto obj = m_env->find_object(n); - if (obj) + if (obj && n != obj->get_name()) diagnostic(m_io_state) << "warning: " << n << " will shadow " << obj->get_name() << endl; } m_using_decls.insert(n, p.second);