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

4 files changed, 16 insertions, 14 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index ad54fca23..51e88a7c0 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
-      [Proofview.V82.tactic (revert dephyps);
+      [new_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 9dd6c941e..eb9bbb5e3 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 (Tactics.revert [name]) (Tacmach.refine p))
+		  (tclTHEN (Proofview.V82.of_tactic (Tactics.new_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 0d2b3d5a1..e838dc52d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1699,8 +1699,9 @@ and interp_atomic ist tac =
           gl
       end
   | TacRevert l ->
-      Proofview.V82.tactic begin fun gl -> 
-        Tactics.revert (interp_hyp_list ist (pf_env gl) l) gl
+      Proofview.Goal.raw_enter begin fun gl ->
+        let env = Proofview.Goal.env gl in
+        Tactics.new_revert (interp_hyp_list ist env l)
       end
 
   (* Constructors *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index da33ecfd8..e9c65a97d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1914,6 +1914,13 @@ 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
@@ -2039,13 +2046,6 @@ 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,9 +2783,10 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
 	  in
 	    if List.is_empty vars then tac
 	    else Tacticals.New.tclTHEN tac
-              (Proofview.V82.tactic (fun gl -> tclFIRST [revert vars ;
-				   tclMAP (fun id ->
-				     tclTRY (generalize_dep ~with_let:true (mkVar id))) vars] gl))
+              (Tacticals.New.tclFIRST
+                [new_revert vars ;
+		 Proofview.V82.tactic (fun gl -> tclMAP (fun id ->
+				     tclTRY (generalize_dep ~with_let:true (mkVar id))) vars gl)])
   end
 
 let rec compare_upto_variables x y =