max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/class): is_anonymous_inst_name: ignore macro scopes

Browse source
This commit is contained in:
Sebastian Ullrich 2019-01-20 21:43:35 +01:00
parent 7001eee350
commit 280dc4e8d8
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/class.cpp
View file

@ -260,8 +260,10 @@ name mk_anonymous_inst_name(unsigned idx) {
}
bool is_anonymous_inst_name(name const & n) {
if (!n.is_atomic() || !n.is_string()) return false;
return strncmp(n.get_string().data(),
// remove mangled macro scopes
auto n2 = n.get_root();
if (!n2.is_string()) return false;
return strncmp(n2.get_string().data(),
g_anonymous_inst_name_prefix->get_string().data(),
strlen(g_anonymous_inst_name_prefix->get_string().data())) == 0;
}