From 1ba55e5cdadb3d99d5d9b784bd3a8a3dcf30a437 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Fri, 9 Dec 2016 15:52:09 -0500 Subject: [PATCH] feat(library/init/meta/interactive): allow metavariable in change tactic --- library/init/meta/interactive.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index db630888cf..319f8272d9 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -107,7 +107,7 @@ meta def assumption : tactic unit := tactic.assumption meta def change (q : qexpr0) : tactic unit := -to_expr_strict q >>= tactic.change +to_expr q >>= tactic.change meta def exact (q : qexpr0) : tactic unit := do tgt : expr ← target,