fix(library/elaborator): add missing conflict justification
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
521fa1ddb8
commit
577ca128a1
1 changed files with 1 additions and 0 deletions
|
@ -1158,6 +1158,7 @@ class elaborator::imp {
|
|||
push_front(mk_eq_constraint(ctx, arg(a, i), arg(b, i), new_jst));
|
||||
return true;
|
||||
} else {
|
||||
m_conflict = justification(new unification_failure_justification(c));
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue