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,