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

fix(library/unifier): bug in process_eq_constraint

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-30 18:22:05 -07:00
parent abe12b0631
commit ad12abcdb4
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

@ -575,8 +575,12 @@ struct unifier_fn {
// Update justification using the justification of the instantiated metavariables
justification new_jst = mk_composite1(mk_composite1(c.get_justification(), lhs_jst.second), rhs_jst.second);
if (!has_metavar(lhs) && !has_metavar(rhs)) {
set_conflict(new_jst);
return false; // trivial failure
if (!m_tc.is_def_eq(lhs, rhs, new_jst)) {
set_conflict(new_jst);
return false; // trivial failure
} else {
return true;
}
}
// Handle higher-order pattern matching.