From 3195a800f40d8eca413bf336759ace7e19042e02 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 21 Jun 2017 16:53:35 -0700 Subject: [PATCH] feat(library/tactic/simp_lemmas): use proof for refl lemmas at simp_lemma_rewrite too I forgot to do it at 9fcb3ae4b55bcff --- src/library/tactic/simp_lemmas.cpp | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/library/tactic/simp_lemmas.cpp b/src/library/tactic/simp_lemmas.cpp index e80907462e..a84f266d47 100644 --- a/src/library/tactic/simp_lemmas.cpp +++ b/src/library/tactic/simp_lemmas.cpp @@ -1395,12 +1395,9 @@ static simp_result simp_lemma_rewrite(type_context & ctx, simp_lemma const & sl, return simp_result(e); } } - if (sl.is_refl()) { - return simp_result(new_rhs); - } else { - expr pf = ctx.instantiate_mvars(sl.get_proof()); - return simp_result(new_rhs, pf); - } + + expr pf = ctx.instantiate_mvars(sl.get_proof()); + return simp_result(new_rhs, pf); } vm_obj simp_lemmas_rewrite_core(transparency_mode const & m, simp_lemmas const & sls, vm_obj const & prove_fn,