Revert "Avoid "revert" to retype-check the goal, and move it to a "new" tactic."

(made push command with wrong local ref; leaving control to Matthieu
on new revert)

This reverts commit b797ba85b7b0f82d66af5629ccf6f75d90dda99a.

4 files changed, 14 insertions, 16 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 51e88a7c03..ad54fca233 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1627,7 +1627,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
   let need_rewrite = not (List.is_empty dephyps) || depconcl in
   tclTHENLIST
     ((if need_rewrite then
-      [new_revert dephyps;
+      [Proofview.V82.tactic (revert dephyps);
        general_rewrite dir AllOccurrences true dep_proof_ok (mkVar hyp);
        (tclMAP intro_using dephyps)]
       else
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index eb9bbb5e3c..9dd6c941ee 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1421,7 +1421,7 @@ let cl_rewrite_clause_tac ?abs strat meta clause gl =
 	      let name = next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
 		tclTHENLAST
 		  (Tacmach.internal_cut false name newt)
-		  (tclTHEN (Proofview.V82.of_tactic (Tactics.new_revert [name])) (Tacmach.refine p))
+		  (tclTHEN (Tactics.revert [name]) (Tacmach.refine p))
 	  | None, None -> change_in_concl None newt
 	in tclTHEN (evartac undef) tac
   in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e838dc52d1..0d2b3d5a1f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1699,9 +1699,8 @@ and interp_atomic ist tac =
           gl
       end
   | TacRevert l ->
-      Proofview.Goal.raw_enter begin fun gl ->
-        let env = Proofview.Goal.env gl in
-        Tactics.new_revert (interp_hyp_list ist env l)
+      Proofview.V82.tactic begin fun gl -> 
+        Tactics.revert (interp_hyp_list ist (pf_env gl) l) gl
       end
 
   (* Constructors *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e9c65a97dc..da33ecfd88 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1914,13 +1914,6 @@ let bring_hyps hyps =
       end
     end
 
-let new_revert hyps = 
-  Proofview.Goal.raw_enter begin fun gl ->
-    let gl = Proofview.Goal.assume gl in
-    let ctx = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) hyps in
-      (bring_hyps ctx) <*> (Proofview.V82.tactic (clear hyps))
-  end
-
 (* Compute a name for a generalization *)
 
 let generalized_name c t ids cl = function
@@ -2046,6 +2039,13 @@ let revert hyps gl =
     hyps
   in tclTHEN (generalize_gen_let lconstr) (clear hyps) gl
 
+let new_revert hyps = 
+  Proofview.Goal.raw_enter begin fun gl ->
+    let gl = Proofview.Goal.assume gl in
+    let ctx = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) hyps in
+      (bring_hyps ctx) <*> (Proofview.V82.tactic (clear hyps))
+  end
+
 (* Faudra-t-il une version avec plusieurs args de generalize_dep ?
 Cela peut-être troublant de faire "Generalize Dependent H n" dans
 "n:nat; H:n=n |- P(n)" et d'échouer parce que H a disparu après la
@@ -2783,10 +2783,9 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
 	  in
 	    if List.is_empty vars then tac
 	    else Tacticals.New.tclTHEN tac
-              (Tacticals.New.tclFIRST
-                [new_revert vars ;
-		 Proofview.V82.tactic (fun gl -> tclMAP (fun id ->
-				     tclTRY (generalize_dep ~with_let:true (mkVar id))) vars gl)])
+              (Proofview.V82.tactic (fun gl -> tclFIRST [revert vars ;
+				   tclMAP (fun id ->
+				     tclTRY (generalize_dep ~with_let:true (mkVar id))) vars] gl))
   end
 
 let rec compare_upto_variables x y =