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

fix(frontends/lean/server): '[anonymous]' entry being displayed by FINDP

Browse source 
This could happen when there is a declaration (e.g., nat) whose type is
equal to an active namespace.
This commit is contained in:
Leonardo de Moura 2014-09-15 10:07:49 -07:00
parent a803b8fd8d
commit feb4993f9c
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/server.cpp
View file

@ -565,7 +565,7 @@ void server::display_decl(name const & d, environment const & env, options const
// using namespace override resolution rule
list<name> 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;
}