Moving the "clearbody" tactic to TACTIC EXTEND.

7 files changed, 6 insertions, 18 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 10c616627a..d936748f2d 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -161,7 +161,6 @@ type 'a gen_atomic_tactic_expr =
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
 
   (* Context management *)
-  | TacClearBody of 'nam list
   | TacMove of 'nam * 'nam move_location
   | TacRename of ('nam *'nam) list
 
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index ad5f78b46d..04ee02f944 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -618,7 +618,6 @@ GEXTEND Gram
 	  TacAtom (!@loc, TacInductionDestruct(false,true,icl))
 
       (* Context management *)
-      | IDENT "clearbody"; l = LIST1 id_or_meta -> TacAtom (!@loc, TacClearBody l)
       | IDENT "move"; hfrom = id_or_meta; hto = move_location ->
 	  TacAtom (!@loc, TacMove (hfrom,hto))
       | IDENT "rename"; l = LIST1 rename SEP "," -> TacAtom (!@loc, TacRename l)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index c61b80c834..b1d6fb0c0f 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -898,11 +898,6 @@ module Make
             )
 
           (* Context management *)
-          | TacClearBody l ->
-            hov 1 (
-              primitive "clearbody" ++ spc ()
-              ++ prlist_with_sep spc pr.pr_name l
-            )
           | TacMove (id1,id2) ->
             hov 1 (
               primitive "move"
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index ab97dad706..b68aab621e 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -216,6 +216,12 @@ TACTIC EXTEND clear
 | [ "clear" "-" ne_hyp_list(ids) ] -> [ Tactics.keep ids ]
 END
 
+(* Clearbody *)
+
+TACTIC EXTEND clearbody
+  [ "clearbody" ne_hyp_list(ids) ] -> [ Tactics.clear_body ids ]
+END
+
 (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
 
 open Tacexpr
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index bea8d3469b..9775f103f8 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -525,7 +525,6 @@ let rec intern_atomic lf ist x =
       let h2 = intern_quantified_hypothesis ist h2 in
       TacDoubleInduction (h1,h2)
   (* Context management *)
-  | TacClearBody l -> TacClearBody (List.map (intern_hyp ist) l)
   | TacMove (id1,id2) ->
     TacMove (intern_hyp ist id1,intern_move_location ist id2)
   | TacRename l ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 74121d3abe..b2f539fb97 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1881,15 +1881,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
         (TacDoubleInduction (h1,h2))
         (Elim.h_double_induction h1 h2)
   (* Context management *)
-  | TacClearBody l ->
-      Proofview.Goal.enter { enter = begin fun gl ->
-        let env = pf_env gl in
-        let sigma = project gl in
-        let l = interp_hyp_list ist env sigma l in
-        name_atomic ~env
-          (TacClearBody l)
-          (Tactics.clear_body l)
-      end }
   | TacMove (id1,id2) ->
       Proofview.Goal.enter { enter = begin fun gl ->
         Proofview.V82.tactic (Tactics.move_hyp (interp_hyp ist (pf_env gl) (project gl) id1)
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 0b8dbb6e3a..50730eaea1 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -167,7 +167,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacDoubleInduction (h1,h2) as x -> x
 
   (* Context management *)
-  | TacClearBody l as x -> x
   | TacMove (id1,id2) as x -> x
   | TacRename l as x -> x