From ef83c37973a92cda00236a9237a26e3d886b586c Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Fri, 18 Aug 2017 09:24:04 +0200 Subject: [PATCH] fix(library/init/meta/simp_tactic): dsimp_target: instantiate_mvars --- library/init/meta/simp_tactic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean index 1146a75a56..66f179a10a 100644 --- a/library/init/meta/simp_tactic.lean +++ b/library/init/meta/simp_tactic.lean @@ -121,7 +121,7 @@ meta def get_simp_lemmas_or_default : option simp_lemmas → tactic simp_lemmas | (some s) := return s meta def dsimp_target (s : option simp_lemmas := none) (u : list name := []) (cfg : dsimp_config := {}) : tactic unit := -do s ← get_simp_lemmas_or_default s, t ← target, s.dsimplify u t cfg >>= unsafe_change +do s ← get_simp_lemmas_or_default s, t ← target >>= instantiate_mvars, s.dsimplify u t cfg >>= unsafe_change meta def dsimp_hyp (h : expr) (s : option simp_lemmas := none) (u : list name := []) (cfg : dsimp_config := {}) : tactic unit := do s ← get_simp_lemmas_or_default s, revert_and_transform (λ e, s.dsimplify u e cfg) h