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

fix(library/unifier): potentially changing flag from l_false ==> l_undef

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-23 10:59:53 -07:00
parent 301c395e59
commit 35481cb045
1 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/unifier.cpp
View file

@ -84,8 +84,12 @@ lbool occurs_context_check(substitution & s, expr const & e, expr const & m, buf
}
return false; // do not visit type
} else if (is_meta(e)) {
if (!context_check(e, locals) || s.occurs(m, e))
r = l_undef;
if (r == l_true) {
if (!context_check(e, locals))
r = l_undef;
if (s.occurs(m, e))
r = l_undef;
}
if (get_app_fn(e) == m)
r = l_false;
return false; // do not visit children