Moving the "clear" tactic to TACTIC EXTEND.

9 files changed, 20 insertions, 29 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 33a96150c..10c616627 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 *)
-  | TacClear of bool * 'nam list
   | 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 6c3918be3..ad5f78b46 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -618,10 +618,6 @@ GEXTEND Gram
 	  TacAtom (!@loc, TacInductionDestruct(false,true,icl))
 
       (* Context management *)
-      | IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacAtom (!@loc, TacClear (true, l))
-      | IDENT "clear"; l = LIST0 id_or_meta ->
-        let is_empty = match l with [] -> true | _ -> false in
-        TacAtom (!@loc, TacClear (is_empty, l))
       | 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))
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 05c3b3bf4..c61b80c83 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -793,7 +793,6 @@ module Make
         let rec pr_atom0 a = tag_atom a (match a with
           | TacIntroPattern [] -> primitive "intros"
           | TacIntroMove (None,MoveLast) -> primitive "intro"
-          | TacClear (true,[]) -> primitive "clear"
           | t -> str "(" ++ pr_atom1 t ++ str ")"
         )
 
@@ -899,14 +898,6 @@ module Make
             )
 
           (* Context management *)
-          | TacClear (true,[]) as t ->
-            pr_atom0 t
-          | TacClear (keep,l) ->
-            hov 1 (
-              primitive "clear" ++ spc ()
-              ++ (if keep then str "- " else mt ())
-              ++ prlist_with_sep spc pr.pr_name l
-            )
           | TacClearBody l ->
             hov 1 (
               primitive "clearbody" ++ spc ()
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 27efc06cc..ab97dad70 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 e7545597c..bea8d3469 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 2a741ee36..74121d3ab 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 faf068bfd..0b8dbb6e3 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
diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v
index 9125ab16d..25060debe 100644
--- a/test-suite/bugs/closed/3612.v
+++ b/test-suite/bugs/closed/3612.v
@@ -35,6 +35,9 @@ Axiom path_path_sigma : forall {A : Type} (P : A -> Type) (u v : sigT P)
            (r : p..1 = q..1)
            (s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2),
 p = q.
+
+Declare ML Module "coretactics".
+
 Goal forall (A : Type) (B : forall _ : A, Type) (x : @sigT A (fun x : A => B x))
             (xx : @paths (@sigT A (fun x0 : A => B x0)) x x),
        @paths (@paths (@sigT A (fun x0 : A => B x0)) x x) xx
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a6a1546ae..38832b422 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -884,8 +884,13 @@ let vernac_set_used_variables e =
         (str "Unknown variable: " ++ pr_id id))
     l;
   let _, to_clear = set_used_variables l in
-  vernac_solve
-    SelectAll None Tacexpr.(TacAtom (Loc.ghost,TacClear(false,to_clear))) false
+  (** FIXME: too fragile *)
+  let open Tacexpr in
+  let tac = { mltac_plugin = "coretactics"; mltac_tactic = "clear" } in
+  let tac = { mltac_name = tac; mltac_index = 0 } in
+  let arg = Genarg.in_gen (Genarg.rawwit (Genarg.wit_list Constrarg.wit_var)) to_clear in
+  let tac = if List.is_empty to_clear then TacId [] else TacML (Loc.ghost, tac, [TacGeneric arg]) in
+  vernac_solve SelectAll None tac false
 
 
 (*****************************)