Moving the "clear" tactic to TACTIC EXTEND.

4 files changed, 10 insertions, 13 deletions

diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 27efc06cca..ab97dad706 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -206,6 +206,16 @@ TACTIC EXTEND cofix
 | [ "cofix" ident(id) ] -> [ Proofview.V82.tactic (Tactics.cofix (Some id)) ]
 END
 
+(* Clear *)
+
+TACTIC EXTEND clear
+  [ "clear" hyp_list(ids) ] -> [
+    if List.is_empty ids then Tactics.keep []
+    else Proofview.V82.tactic (Tactics.clear ids)
+  ]
+| [ "clear" "-" ne_hyp_list(ids) ] -> [ Tactics.keep 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 e7545597cc..bea8d3469b 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 *)
-  | TacClear (b,l) -> TacClear (b,List.map (intern_hyp ist) l)
   | TacClearBody l -> TacClearBody (List.map (intern_hyp ist) l)
   | TacMove (id1,id2) ->
     TacMove (intern_hyp ist id1,intern_move_location ist id2)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 2a741ee367..74121d3abe 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1881,17 +1881,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
         (TacDoubleInduction (h1,h2))
         (Elim.h_double_induction h1 h2)
   (* Context management *)
-  | TacClear (b,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
-        if b then name_atomic ~env (TacClear (b, l)) (Tactics.keep l)
-        else
-          (* spiwack: until the tactic is in the monad *)
-          let tac = Proofview.V82.tactic (fun gl -> Tactics.clear l gl) in
-          Proofview.Trace.name_tactic (fun () -> Pp.str"<clear>") tac
-      end }
   | TacClearBody l ->
       Proofview.Goal.enter { enter = begin fun gl ->
         let env = pf_env gl in
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index faf068bfd5..0b8dbb6e3a 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 *)
-  | TacClear _ as x -> x
   | TacClearBody l as x -> x
   | TacMove (id1,id2) as x -> x
   | TacRename l as x -> x