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

fix(library/unifier): missing set_conflict

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-20 16:01:06 -07:00
parent 9588336c15
commit fa342c8ea7
1 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/library/unifier.cpp
View file

@ -829,15 +829,18 @@ struct unifier_fn {
return Continue; return Continue;
bool contains = occurs_meta(lhs, rhs); bool contains = occurs_meta(lhs, rhs);
if (contains) { if (contains) {
if (is_succ(rhs)) if (is_succ(rhs)) {
set_conflict(j);
return Failed; return Failed;
else } else {
return Continue; return Continue;
}
} }
lean_assert(!m_subst.is_assigned(lhs)); lean_assert(!m_subst.is_assigned(lhs));
if (assign(lhs, rhs, j)) { if (assign(lhs, rhs, j)) {
return Solved; return Solved;
} else { } else {
set_conflict(j);
return Failed; return Failed;
} }
} }