From bebdba1004552aaa740e4a5580476efea21f38e3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 23 May 2017 21:43:37 -0700 Subject: [PATCH] fix(library/init/meta/simp_tactic): make sure replace_target does not fail due to reducibility settings --- library/init/meta/simp_tactic.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean index 074aa4def5..0c6680fd6d 100644 --- a/library/init/meta/simp_tactic.lean +++ b/library/init/meta/simp_tactic.lean @@ -245,9 +245,12 @@ do e_type ← infer_type e >>= whnf, simplify_core cfg S `eq e meta def replace_target (new_target : expr) (pr : expr) : tactic unit := -do assert `htarget new_target, swap, - ht ← get_local `htarget, - mk_eq_mpr pr ht >>= exact +do t ← target, + assert `htarget new_target, swap, + ht ← get_local `htarget, + eq_type ← mk_app `eq [t, new_target], + locked_pr ← return $ expr.app (expr.app (expr.const ``id_locked [level.zero]) eq_type) pr, + mk_eq_mpr locked_pr ht >>= exact meta def simplify_goal (S : simp_lemmas) (cfg : simp_config := {}) : tactic unit := do t ← target,