diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index b196e189e9..4a23fdff46 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -108,7 +108,7 @@ meta_constant intron        : nat → tactic unit
 meta_constant rename        : name → name → tactic unit
 /- Clear the given local constant. The tactic fails if the given expression is not a local constant. -/
 meta_constant clear         : expr → tactic unit
-meta_constant revert_lst    : list expr → tactic unit
+meta_constant revert_lst    : list expr → tactic nat
 meta_constant whnf          : expr → tactic expr
 meta_constant unify_core    : transparency → expr → expr → tactic unit
 /- Infer the type of the given expression.
@@ -223,7 +223,7 @@ mk_app_core semireducible
 meta_definition mk_mapp : name → list (option expr) → tactic expr :=
 mk_mapp_core semireducible
 
-meta_definition revert (l : expr) : tactic unit :=
+meta_definition revert (l : expr) : tactic nat :=
 revert_lst [l]
 
 meta_definition clear_lst : list name → tactic unit
diff --git a/src/library/tactic/revert_tactic.cpp b/src/library/tactic/revert_tactic.cpp
index 132878dba7..8d252924ba 100644
--- a/src/library/tactic/revert_tactic.cpp
+++ b/src/library/tactic/revert_tactic.cpp
@@ -29,7 +29,8 @@ vm_obj revert(list<expr> const & ls, tactic_state const & s) {
             return mk_tactic_exception(sstream() << "revert tactic failed, unknown '" << local_pp_name(l) << "' hypothesis", s);
         }
     }
-    return mk_tactic_success(revert(locals, s));
+    tactic_state new_s = revert(locals, s);
+    return mk_tactic_success(mk_vm_nat(locals.size()), new_s);
 }
 
 vm_obj tactic_revert_lst(vm_obj const & ns, vm_obj const & s) {
diff --git a/tests/lean/rev_tac1.lean b/tests/lean/rev_tac1.lean
new file mode 100644
index 0000000000..90c69b97da
--- /dev/null
+++ b/tests/lean/rev_tac1.lean
@@ -0,0 +1,10 @@
+open tactic
+
+example (a b : nat) (H : a > 0) (H : a > b) (H : b > 0) : a = b → true :=
+by do
+  a ← get_local "a",
+  n ← revert a,
+  trace n,
+  trace_state,
+  intros,
+  constructor
diff --git a/tests/lean/rev_tac1.lean.expected.out b/tests/lean/rev_tac1.lean.expected.out
new file mode 100644
index 0000000000..db345dfb1a
--- /dev/null
+++ b/tests/lean/rev_tac1.lean.expected.out
@@ -0,0 +1,5 @@
+3
+b : ℕ,
+H : b > 0
+⊢ ∀ a,
+    a > 0 → a > b → a = b → true