diff --git a/doc/changes.md b/doc/changes.md
index 86a963eb35..f27583bf7e 100644
--- a/doc/changes.md
+++ b/doc/changes.md
@@ -100,6 +100,8 @@ master branch (aka work in progress branch)
 * `subst` and `subst_vars` now support heterogeneous equalities that are actually homogeneous
    (i.e., `@heq α a β b` where `α` and `β` are definitionally equal).
 
+* Add interactive `subst_vars` tactic.
+
 *Changes*
 
 * Replace `inout` modifier in type class declarations with `out_param` modifier.
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 0ce99b63f6..31fed53dbe 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -1297,6 +1297,12 @@ Given hypothesis `h : x = t` or `h : t = x`, where `x` is a local constant, `sub
 meta def subst (q : parse texpr) : tactic unit :=
 i_to_expr q >>= tactic.subst >> try (tactic.reflexivity reducible)
 
+/--
+Apply `subst` to all hypotheses of the form `h : x = t` or `h : t = x`.
+-/
+meta def subst_vars : tactic unit :=
+tactic.subst_vars
+
 /--
 `clear h₁ ... hₙ` tries to clear each hypothesis `hᵢ` from the local context.
 -/
diff --git a/tests/lean/run/subst_heq.lean b/tests/lean/run/subst_heq.lean
index 5a9b437a6d..c32b5a3489 100644
--- a/tests/lean/run/subst_heq.lean
+++ b/tests/lean/run/subst_heq.lean
@@ -2,3 +2,8 @@ example (a b : nat) (h : a == b) : a + 1 = b + 1 :=
 begin
   subst h
 end
+
+example (a b : nat) (h : a == b) : a + 1 = b + 1 :=
+begin
+  subst_vars
+end