Moving the "exists" tactic to TACTIC EXTEND.

7 files changed, 23 insertions, 34 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 3f1d0fd76..dae960e0e 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -163,9 +163,6 @@ type 'a gen_atomic_tactic_expr =
   | TacMove of 'nam * 'nam move_location
   | TacRename of ('nam *'nam) list
 
-  (* Trmuctors *)
-  | TacSplit of evars_flag * 'trm bindings list
-
   (* Conversion *)
   | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr
   | TacChange of 'pat option * 'dtrm * 'nam clause_expr
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 4587e321f..e50eca25b 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -621,11 +621,6 @@ GEXTEND Gram
 	  TacAtom (!@loc, TacMove (hfrom,hto))
       | IDENT "rename"; l = LIST1 rename SEP "," -> TacAtom (!@loc, TacRename l)
 
-      (* Constructors *)
-      | "exists"; bll = opt_bindings -> TacAtom (!@loc, TacSplit (false,bll))
-      | IDENT "eexists"; bll = opt_bindings ->
-	  TacAtom (!@loc, TacSplit (true,bll))
-
       (* Equality and inversion *)
       | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ",";
 	  cl = clause_dft_concl; t=opt_by_tactic -> TacAtom (!@loc, TacRewrite (false,l,cl,t))
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 689ac6e4e..2c57cb811 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -725,7 +725,6 @@ module Make
 
         (* some shortcuts *)
         let _pr_bindings = pr_bindings pr.pr_constr pr.pr_lconstr in
-        let pr_ex_bindings = pr_bindings_gen true pr.pr_constr pr.pr_lconstr in
         let pr_with_bindings = pr_with_bindings pr.pr_constr pr.pr_lconstr in
         let pr_with_bindings_arg_full = pr_with_bindings_arg in
         let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in
@@ -909,13 +908,6 @@ module Make
                 l
             )
 
-          (* Constructors *)
-          | TacSplit (ev,l) ->
-            hov 1 (
-              primitive (with_evars ev "exists")
-              ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l
-            )
-
           (* Conversion *)
           | TacReduce (r,h) ->
             hov 1 (
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 55461ef7c..2d5ce5307 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -15,6 +15,7 @@ open Misctypes
 open Genredexpr
 
 open Proofview.Notations
+open Sigma.Notations
 
 DECLARE PLUGIN "coretactics"
 
@@ -145,6 +146,14 @@ END
 
 (** Split *)
 
+let rec delayed_list = function
+| [] -> { Tacexpr.delayed = fun _ sigma -> Sigma.here [] sigma }
+| x :: l ->
+  { Tacexpr.delayed = fun env sigma ->
+    let Sigma (x, sigma, p) = x.Tacexpr.delayed env sigma in
+    let Sigma (l, sigma, q) = (delayed_list l).Tacexpr.delayed env sigma in
+    Sigma (x :: l, sigma, p +> q) }
+
 TACTIC EXTEND split
   [ "split" ] -> [ Tactics.split_with_bindings false [NoBindings] ]
 END
@@ -165,6 +174,20 @@ TACTIC EXTEND esplit_with
   ]
 END
 
+TACTIC EXTEND exists
+  [ "exists" ] -> [ Tactics.split_with_bindings false [NoBindings] ]
+| [ "exists" ne_bindings_list_sep(bll, ",") ] -> [
+    Tacticals.New.tclDELAYEDWITHHOLES false (delayed_list bll) (fun bll -> Tactics.split_with_bindings false bll)
+  ]
+END
+
+TACTIC EXTEND eexists
+  [ "eexists" ] -> [ Tactics.split_with_bindings true [NoBindings] ]
+| [ "eexists" ne_bindings_list_sep(bll, ",") ] -> [
+    Tacticals.New.tclDELAYEDWITHHOLES true (delayed_list bll) (fun bll -> Tactics.split_with_bindings true bll)
+  ]
+END
+
 (** Intro *)
 
 TACTIC EXTEND intros_until
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 84df21eb8..e69d3f61e 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -531,9 +531,6 @@ let rec intern_atomic lf ist x =
 			     intern_hyp ist id1,
 			     intern_hyp ist id2) l)
 
-  (* Constructors *)
-  | TacSplit (ev,bll) -> TacSplit (ev,List.map (intern_bindings ist) bll)
-
   (* Conversion *)
   | TacReduce (r,cl) ->
       dump_glob_red_expr r;
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 81fbcc6db..65fdecc29 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1894,18 +1894,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
           (Tactics.rename_hyp l)
       end }
 
-  (* Constructors *)
-  | TacSplit (ev,bll) ->
-      Proofview.Goal.enter { enter = begin fun gl ->
-        let env = Proofview.Goal.env gl in
-        let sigma = project gl in
-        let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in
-        let named_tac =
-          let tac = Tactics.split_with_bindings ev bll in
-          name_atomic ~env (TacSplit (ev, bll)) tac
-        in
-        Tacticals.New.tclWITHHOLES ev named_tac sigma
-      end }
   (* Conversion *)
   | TacReduce (r,cl) ->
       (* spiwack: until the tactic is in the monad *)
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 142a96445..ba9a74d05 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -169,9 +169,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacMove (id1,id2) as x -> x
   | TacRename l as x -> x
 
-  (* Constructors *)
-  | TacSplit (ev,bll) -> TacSplit (ev,List.map (subst_bindings subst) bll)
-
   (* Conversion *)
   | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl)
   | TacChange (op,c,cl) ->