Removing [revert] tactic from the AST.

7 files changed, 7 insertions, 12 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index d7237f467..e2995cfab 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -154,7 +154,6 @@ type ('trm,'pat,'cst,'ref,'nam,'lev) gen_atomic_tactic_expr =
   | TacClearBody of 'nam list
   | TacMove of bool * 'nam * 'nam move_location
   | TacRename of ('nam *'nam) list
-  | TacRevert of 'nam list
 
   (* Trmuctors *)
   | TacSplit of evars_flag * 'trm bindings list
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 861ac5dfd..5ffabbcf5 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -644,7 +644,6 @@ GEXTEND Gram
       | IDENT "move"; hfrom = id_or_meta; hto = move_location ->
 	  TacAtom (!@loc, TacMove (true,hfrom,hto))
       | IDENT "rename"; l = LIST1 rename SEP "," -> TacAtom (!@loc, TacRename l)
-      | IDENT "revert"; l = LIST1 id_or_meta -> TacAtom (!@loc, TacRevert l)
 
       (* Constructors *)
       | "exists"; bll = opt_bindings -> TacAtom (!@loc, TacSplit (false,bll))
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index f3bec78e2..f8eb93956 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -791,8 +791,6 @@ and pr_atom1 = function
 	   (fun (i1,i2) ->
 	      pr_ident i1 ++ spc () ++ str "into" ++ spc () ++ pr_ident i2)
 	   l)
-  | TacRevert l ->
-      hov 1 (str "revert" ++ spc () ++ prlist_with_sep spc pr_ident l)
 
   (* Constructors *)
   | TacSplit (ev,l) -> hov 1 (str (with_evars ev "exists") ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l)
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index d429dc07e..a464b5e8d 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -180,6 +180,12 @@ TACTIC EXTEND intros_until
   [ "intros" "until" quantified_hypothesis(h) ] -> [ Tactics.intros_until h ]
 END
 
+(** Revert *)
+
+TACTIC EXTEND revert
+  [ "revert" ne_hyp_list(hl) ] -> [ Tactics.revert hl ]
+END
+
 (** Simple induction / destruct *)
 
 TACTIC EXTEND simple_induction
@@ -201,7 +207,7 @@ let initial_atomic () =
     let body = TacAtom (dloc, t) in
     Tacenv.register_ltac false (Id.of_string s) body
   in
-  let ans = List.iter iter
+  let () = List.iter iter
       [ "red", TacReduce(Red false,nocl);
         "hnf", TacReduce(Hnf,nocl);
         "simpl", TacReduce(Simpl None,nocl);
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index eac80a63a..fd5d23656 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -521,7 +521,6 @@ let rec intern_atomic lf ist x =
       TacRename (List.map (fun (id1,id2) ->
 			     intern_hyp ist id1,
 			     intern_hyp ist id2) l)
-  | TacRevert l -> TacRevert (List.map (intern_hyp ist) l)
 
   (* Constructors *)
   | TacSplit (ev,bll) -> TacSplit (ev,List.map (intern_bindings ist) bll)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 8c86db613..e69a307bd 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1944,11 +1944,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
 	  interp_fresh_ident ist env (snd id2)) l)
           gl
       end
-  | TacRevert l ->
-      Proofview.Goal.raw_enter begin fun gl ->
-        let env = Proofview.Goal.env gl in
-        Tactics.revert (interp_hyp_list ist env l)
-      end
 
   (* Constructors *)
   | TacSplit (ev,bll) ->
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index cdea2b47b..ab96fe674 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -173,7 +173,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacClearBody l as x -> x
   | TacMove (dep,id1,id2) as x -> x
   | TacRename l as x -> x
-  | TacRevert _ as x -> x
 
   (* Constructors *)
   | TacSplit (ev,bll) -> TacSplit (ev,List.map (subst_bindings subst) bll)