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

perf(library/type_context): small optimization

Browse source
This commit is contained in:
Leonardo de Moura 2016-02-02 15:36:53 -08:00
parent bc86e9f179
commit b508cf813c
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/library/type_context.cpp
View file

@ -743,8 +743,8 @@ bool type_context::is_def_eq_proof_irrel(expr const & e1, expr const & e2) {
if (!m_env.prop_proof_irrel())
return false;
expr e1_type = infer(e1);
expr e2_type = infer(e2);
if (is_prop(e1_type)) {
expr e2_type = infer(e2);
scope s(*this);
if (is_def_eq_core(e1_type, e2_type)) {
s.commit();