feat(library/init/meta/tactic): 'revert' tactic returns the number of actually reverted hypothesis

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

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) {

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

tests/lean/rev_tac1.lean.expected.out

@@ -0,0 +1,5 @@
+3
+b : ℕ,
+H : b > 0
+⊢ ∀ a,
+    a > 0 → a > b → a = b → true