From ebdda67812690a03f5fa8b6ed5b374df2a1d1176 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Mar 2015 19:23:41 -0700 Subject: [PATCH] fix(library/tactic/inversion_tactic.cpp): remove unnecessary hypothesis in HoTT mode partial solution for #468 --- src/library/tactic/inversion_tactic.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp index 64535eedf..0b793cdf1 100644 --- a/src/library/tactic/inversion_tactic.cpp +++ b/src/library/tactic/inversion_tactic.cpp @@ -742,7 +742,7 @@ class inversion_tac { if (const_name(lhs_fn) == const_name(rhs_fn)) { // injectivity transition expr new_type = binding_domain(whnf(infer_type(no_confusion))); - if (m_proof_irrel) + if (m_proof_irrel || !depends_on(g_type, hyps.back())) hyps.pop_back(); // remove processed equality expr new_mvar = mk_metavar(m_ngen.next(), Pi(hyps, new_type)); expr new_meta = mk_app(new_mvar, hyps); @@ -835,7 +835,7 @@ class inversion_tac { } } else if (is_local(lhs)) { // flip equation and reduce to previous case - if (m_proof_irrel) + if (m_proof_irrel || !depends_on(g_type, hyps.back())) hyps.pop_back(); // remove processed equality expr symm_eq = mk_eq(rhs, lhs).first; expr new_type = mk_arrow(symm_eq, g_type);