From 7dd8c2bf4747c94be6f18d7fdd0e3b593f560a2f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Mon, 29 Feb 2016 11:20:26 +0100
Subject: Moving the "clearbody" tactic to TACTIC EXTEND.

---
 tactics/coretactics.ml4 | 6 ++++++
 tactics/tacintern.ml    | 1 -
 tactics/tacinterp.ml    | 9 ---------
 tactics/tacsubst.ml     | 1 -
 4 files changed, 6 insertions(+), 11 deletions(-)

(limited to 'tactics')

diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index ab97dad70..b68aab621 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 bea8d3469..9775f103f 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 74121d3ab..b2f539fb9 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 0b8dbb6e3..50730eaea 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
 
-- 
cgit v1.2.3