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

perf(kernel/justification): avoid redundant justification objects

Browse source
This commit is contained in:
Leonardo de Moura 2015-03-25 19:09:01 -07:00
parent e019ab5500
commit d69f829337
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/justification.cpp
View file

@ -296,7 +296,7 @@ justification mk_composite(justification const & j1, justification const & j2, o
return justification(new (get_ext_composite_allocator().allocate()) ext_composite_cell(j1, j2, fn, s));
}
justification mk_composite1(justification const & j1, justification const & j2) {
if (j1.is_none())
if (j1.is_none() || j1.raw() == j2.raw())
return j2;
if (j2.is_none())
return j1;