From 979e48bfe1a16b0cbc6671a78297d496b730bf99 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Thu, 8 May 2014 18:36:34 +0200
Subject: Upgrade Matthieu's new_revert as the "revert" (a "unit tactic").

---
 tactics/equality.ml  |  2 +-
 tactics/rewrite.ml   |  2 +-
 tactics/tacinterp.ml |  5 +++--
 tactics/tactics.ml   | 28 +++++++++++-----------------
 tactics/tactics.mli  |  3 +--
 5 files changed, 17 insertions(+), 23 deletions(-)

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index d342d8482..623733ec7 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);
+      [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 56194ed5d..abf1c47d8 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1445,7 +1445,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.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 1b770d214..4c0f10342 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1658,8 +1658,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.revert (interp_hyp_list ist env l)
       end
 
   (* Constructors *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8fe0a6893..ba721bc89 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1914,6 +1914,13 @@ let bring_hyps hyps =
       end
     end
 
+let 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
@@ -2032,20 +2039,6 @@ let generalize l =
 let new_generalize l =
   new_generalize_gen_let (List.map (fun c -> ((AllOccurrences,c,None),Anonymous)) l)
 
-let revert hyps gl =
-  let lconstr = List.map (fun id ->
-    let (_, b, _) = pf_get_hyp gl id in
-    ((AllOccurrences, mkVar id, b), Anonymous))
-    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 +2776,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
+                [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 =
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 411cc38f4..4153f6e75 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -165,8 +165,7 @@ val specialize    : constr with_bindings -> tactic
 val move_hyp      : bool -> Id.t -> Id.t move_location -> tactic
 val rename_hyp    : (Id.t * Id.t) list -> tactic
 
-val revert        : Id.t list -> tactic
-val new_revert    : Id.t list -> unit Proofview.tactic
+val revert        : Id.t list -> unit Proofview.tactic
 
 (** {6 Resolution tactics. } *)
 
-- 
cgit v1.2.3