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

fix(kernel/level): bug in get_undef_global

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-12 14:34:24 -07:00
parent 89d6a1e691
commit a8a6bb1b7f
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/kernel/level.cpp
View file

@ -464,7 +464,7 @@ level replace_level_fn::apply(level const & l) {
optional<name> get_undef_param(level const & l, param_names const & ps) { optional<name> get_undef_param(level const & l, param_names const & ps) {
optional<name> r; optional<name> r;
for_each(l, [&](level const & l) { for_each(l, [&](level const & l) {
if (!has_param(l)) if (!has_param(l) || r)
return false; return false;
if (is_param(l) && std::find(ps.begin(), ps.end(), param_id(l)) == ps.end()) if (is_param(l) && std::find(ps.begin(), ps.end(), param_id(l)) == ps.end())
r = param_id(l); r = param_id(l);
@ -476,9 +476,9 @@ optional<name> get_undef_param(level const & l, param_names const & ps) {
optional<name> get_undef_global(level const & l, environment const & env) { optional<name> get_undef_global(level const & l, environment const & env) {
optional<name> r; optional<name> r;
for_each(l, [&](level const & l) { for_each(l, [&](level const & l) {
if (!has_global(l)) if (!has_global(l) || r)
return false; return false;
if (is_global(l) && env.is_global_level(global_id(l))) if (is_global(l) && !env.is_global_level(global_id(l)))
r = global_id(l); r = global_id(l);
return true; return true;
}); });