From b24c085cb0f04fce1adf68668f1dab161ba642b8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 9 Feb 2014 09:26:51 -0800 Subject: [PATCH] feat(frontends/lean): avoid warning message Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser_cmds.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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);