Moving the "exists" tactic to TACTIC EXTEND.

4 files changed, 23 insertions, 18 deletions

diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 55461ef7c5..2d5ce53075 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 84df21eb81..e69d3f61e0 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 81fbcc6db6..65fdecc29b 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 142a964454..ba9a74d05a 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) ->