From e1c024d4d9c8edc828b92f53cbdb028e44afa1fe Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Mon, 29 May 2017 11:49:32 -0400 Subject: [PATCH] fix(library/init/meta/simp_tactic): fix relabeling of hypotheses in simp_intro_aux --- library/init/meta/simp_tactic.lean | 4 ++-- tests/lean/simp_wildcard.lean | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean index 0c6680fd6d..20e15c64de 100644 --- a/library/init/meta/simp_tactic.lean +++ b/library/init/meta/simp_tactic.lean @@ -325,10 +325,10 @@ meta def simp_intro_aux (cfg : simp_config) (updt : bool) : simp_lemmas → bool h_d ← intro1_aux use_ns ns, h_new_d ← mk_eq_mp h_d_eq_new_d h_d, assertv_core h_d.local_pp_name new_d h_new_d, + clear h_d, h_new ← intro1, new_S ← if updt && is_equation new_d then S.add h_new else return S, - clear h_d, - simp_intro_aux new_S use_ns ns + simp_intro_aux new_S use_ns ns.tail } <|> -- failed to simplify... we just introduce and continue diff --git a/tests/lean/simp_wildcard.lean b/tests/lean/simp_wildcard.lean index 5e38ad714f..4dacae05b9 100644 --- a/tests/lean/simp_wildcard.lean +++ b/tests/lean/simp_wildcard.lean @@ -20,8 +20,8 @@ forall (A B C : Type) (list.map h $ list.map f b) = b' -> a' = list.map (g ∘ f) a ∧ b' = list.map (h ∘ f) b := begin - intros, + intros A B C a b a' b' f g h a₁ a₂, simp [simp_rule] at *, - rw [a_1_1, a_2_1], + rw [a₁, a₂], split; reflexivity end