Moving the [split] tactic out of the AST.

5 files changed, 27 insertions, 5 deletions

diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 283cff73f8..a95d714435 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -118,3 +118,27 @@ END
 TACTIC EXTEND symmetry
   [ "symmetry" ] -> [ Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} ]
 END
+
+(** Split *)
+
+TACTIC EXTEND split
+  [ "split" ] -> [ Tactics.split_with_bindings false [NoBindings] ]
+END
+
+TACTIC EXTEND esplit
+  [ "esplit" ] -> [ Tactics.split_with_bindings true [NoBindings] ]
+END
+
+TACTIC EXTEND split_with
+  [ "split" "with" bindings(bl) ] -> [
+    let { Evd.sigma = sigma ; it = bl } = bl in
+    Tacticals.New.tclWITHHOLES false (Tactics.split_with_bindings false) sigma [bl]
+  ]
+END
+
+TACTIC EXTEND esplit_with
+  [ "esplit" "with" bindings(bl) ] -> [
+    let { Evd.sigma = sigma ; it = bl } = bl in
+    Tacticals.New.tclWITHHOLES true (Tactics.split_with_bindings true) sigma [bl]
+  ]
+END
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 9da5d44e06..5ce914a9c8 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -80,8 +80,6 @@ let initial_atomic =
         "cofix", TacCofix None;
         "trivial", TacTrivial (Off,[],None);
         "auto", TacAuto(Off,None,[],None);
-        "split", TacSplit(false,false,[NoBindings]);
-        "esplit", TacSplit(true,false,[NoBindings]);
         "constructor", TacAnyConstructor (false,None);
         "econstructor", TacAnyConstructor (true,None);
       ]
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 4d711af9ab..35952c9ddd 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -520,7 +520,7 @@ let rec intern_atomic lf ist x =
   | TacRevert l -> TacRevert (List.map (intern_hyp_or_metaid ist) l)
 
   (* Constructors *)
-  | TacSplit (ev,b,bll) -> TacSplit (ev,b,List.map (intern_bindings ist) bll)
+  | TacSplit (ev,bll) -> TacSplit (ev,List.map (intern_bindings ist) bll)
   | TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (intern_pure_tactic ist) t)
   | TacConstructor (ev,n,bl) -> TacConstructor (ev,intern_or_var ist n,intern_bindings ist bl)
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 9ca9aababa..1ca63b53ad 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1690,7 +1690,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
       end
 
   (* Constructors *)
-  | TacSplit (ev,_,bll) ->
+  | TacSplit (ev,bll) ->
       Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 6222455240..aa090b7159 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -178,7 +178,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacRevert _ as x -> x
 
   (* Constructors *)
-  | TacSplit (ev,b,bll) -> TacSplit (ev,b,List.map (subst_bindings subst) bll)
+  | TacSplit (ev,bll) -> TacSplit (ev,List.map (subst_bindings subst) bll)
   | TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (subst_tactic subst) t)
   | TacConstructor (ev,n,bl) -> TacConstructor (ev,n,subst_bindings subst bl)