From feb4993f9c18ab4d0155c189d0a695e75d34e8f5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 15 Sep 2014 10:07:49 -0700 Subject: [PATCH] fix(frontends/lean/server): '[anonymous]' entry being displayed by FINDP This could happen when there is a declaration (e.g., nat) whose type is equal to an active namespace. --- src/frontends/lean/server.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp index 53346cde0..4a1065931 100644 --- a/src/frontends/lean/server.cpp +++ b/src/frontends/lean/server.cpp @@ -565,7 +565,7 @@ void server::display_decl(name const & d, environment const & env, options const // using namespace override resolution rule list const & ns_list = get_namespaces(env); for (name const & ns : ns_list) { - if (is_prefix_of(ns, d)) { + if (is_prefix_of(ns, d) && ns != d) { display_decl(d.replace_prefix(ns, name()), d, env, o); return; }