Moving left & right tactics out of the AST.

9 files changed, 49 insertions, 34 deletions

diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index e152cdd7f4..a52fdeb62c 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -385,10 +385,6 @@ let rec mlexpr_of_atomic_tactic = function
               $mlexpr_of_move_location mlexpr_of_hyp id2$ >>
 
   (* Constructors *)
-  | Tacexpr.TacLeft (ev,l) ->
-      <:expr< Tacexpr.TacLeft $mlexpr_of_bool ev$ $mlexpr_of_binding_kind l$>>
-  | Tacexpr.TacRight (ev,l) ->
-      <:expr< Tacexpr.TacRight $mlexpr_of_bool ev$ $mlexpr_of_binding_kind l$>>
   | Tacexpr.TacSplit (ev,b,l) ->
       <:expr< Tacexpr.TacSplit
         ($mlexpr_of_bool ev$,$mlexpr_of_bool b$,$mlexpr_of_list mlexpr_of_binding_kind l$)>>
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 223ece63be..4b78b55fd5 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -144,8 +144,6 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
   | TacRevert of 'nam list
 
   (* Trmuctors *)
-  | TacLeft of evars_flag * 'trm bindings
-  | TacRight of evars_flag * 'trm bindings
   | TacSplit of evars_flag * split_flag * 'trm bindings list
   | TacAnyConstructor of evars_flag *
       ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr option
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 3e80c99f5a..5f9f6e472d 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -634,10 +634,6 @@ GEXTEND Gram
       | IDENT "revert"; l = LIST1 id_or_meta -> TacRevert l
 
       (* Constructors *)
-      | IDENT "left";   bl = with_bindings -> TacLeft  (false,bl)
-      | IDENT "eleft";  bl = with_bindings -> TacLeft  (true,bl)
-      | IDENT "right";  bl = with_bindings -> TacRight (false,bl)
-      | IDENT "eright"; bl = with_bindings -> TacRight (true,bl)
       | IDENT "split";  bl = with_bindings -> TacSplit (false,false,[bl])
       | IDENT "esplit"; bl = with_bindings -> TacSplit (true,false,[bl])
       | "exists"; bll = LIST1 opt_bindings SEP "," -> TacSplit (false,true,bll)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index a5b07c4770..587a8db41b 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -766,8 +766,6 @@ and pr_atom1 = function
       hov 1 (str "revert" ++ spc () ++ prlist_with_sep spc pr_ident l)
 
   (* Constructors *)
-  | TacLeft (ev,l) -> hov 1 (str (with_evars ev "left") ++ pr_bindings l)
-  | TacRight (ev,l) -> hov 1 (str (with_evars ev "right") ++ pr_bindings l)
   | TacSplit (ev,false,l) -> hov 1 (str (with_evars ev "split") ++ prlist_with_sep pr_comma pr_bindings l)
   | TacSplit (ev,true,l) -> hov 1 (str (with_evars ev "exists") ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l)
   | TacAnyConstructor (ev,Some t) ->
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index f033ef5caf..bff5c13d3f 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -11,6 +11,7 @@
 open Util
 open Names
 open Tacexpr
+open Misctypes
 open Tacinterp
 
 DECLARE PLUGIN "coretactics"
@@ -54,3 +55,51 @@ END
 TACTIC EXTEND transitivity
   [ "transitivity" constr(c) ] -> [ Tactics.intros_transitivity (Some c) ]
 END
+
+(** Left *)
+
+TACTIC EXTEND left
+  [ "left" ] -> [ Tactics.left_with_bindings false NoBindings ]
+END
+
+TACTIC EXTEND eleft
+  [ "eleft" ] -> [ Tactics.left_with_bindings true NoBindings ]
+END
+
+TACTIC EXTEND left_with
+  [ "left" "with" bindings(bl) ] -> [
+    let { Evd.sigma = sigma ; it = bl } = bl in
+    Tacticals.New.tclWITHHOLES false (Tactics.left_with_bindings false) sigma bl
+  ]
+END
+
+TACTIC EXTEND eleft_with
+  [ "eleft" "with" bindings(bl) ] -> [
+    let { Evd.sigma = sigma ; it = bl } = bl in
+    Tacticals.New.tclWITHHOLES true (Tactics.left_with_bindings true) sigma bl
+  ]
+END
+
+(** Right *)
+
+TACTIC EXTEND right
+  [ "right" ] -> [ Tactics.right_with_bindings false NoBindings ]
+END
+
+TACTIC EXTEND eright
+  [ "eright" ] -> [ Tactics.right_with_bindings true NoBindings ]
+END
+
+TACTIC EXTEND right_with
+  [ "right" "with" bindings(bl) ] -> [
+    let { Evd.sigma = sigma ; it = bl } = bl in
+    Tacticals.New.tclWITHHOLES false (Tactics.right_with_bindings false) sigma bl
+  ]
+END
+
+TACTIC EXTEND eright_with
+  [ "eright" "with" bindings(bl) ] -> [
+    let { Evd.sigma = sigma ; it = bl } = bl in
+    Tacticals.New.tclWITHHOLES true (Tactics.right_with_bindings true) sigma bl
+  ]
+END
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 2a6589d21f..6dc11510d4 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -80,10 +80,6 @@ let initial_atomic =
         "cofix", TacCofix None;
         "trivial", TacTrivial (Off,[],None);
         "auto", TacAuto(Off,None,[],None);
-        "left", TacLeft(false,NoBindings);
-        "eleft", TacLeft(true,NoBindings);
-        "right", TacRight(false,NoBindings);
-        "eright", TacRight(true,NoBindings);
         "split", TacSplit(false,false,[NoBindings]);
         "esplit", TacSplit(true,false,[NoBindings]);
         "constructor", TacAnyConstructor (false,None);
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 3b1cdecfb6..9f911564a3 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -524,8 +524,6 @@ let rec intern_atomic lf ist x =
   | TacRevert l -> TacRevert (List.map (intern_hyp_or_metaid ist) l)
 
   (* Constructors *)
-  | TacLeft (ev,bl) -> TacLeft (ev,intern_bindings ist bl)
-  | TacRight (ev,bl) -> TacRight (ev,intern_bindings ist bl)
   | TacSplit (ev,b,bll) -> TacSplit (ev,b,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 12547e704d..734d5b8949 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1677,20 +1677,6 @@ and interp_atomic ist tac =
       end
 
   (* Constructors *)
-  | TacLeft (ev,bl) ->
-      Proofview.Goal.raw_enter begin fun gl ->
-        let env = Proofview.Goal.env gl in
-        let sigma = Proofview.Goal.sigma gl in
-        let sigma, bl = interp_bindings ist env sigma bl in
-        Tacticals.New.tclWITHHOLES ev (Tactics.left_with_bindings ev) sigma bl
-      end
-  | TacRight (ev,bl) ->
-      Proofview.Goal.raw_enter begin fun gl ->
-        let env = Proofview.Goal.env gl in
-        let sigma = Proofview.Goal.sigma gl in
-        let sigma, bl = interp_bindings ist env sigma bl in
-        Tacticals.New.tclWITHHOLES ev (Tactics.right_with_bindings ev) sigma bl
-      end
   | TacSplit (ev,_,bll) ->
       Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 1b15fa8e18..bea77a0b06 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -181,8 +181,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacRevert _ as x -> x
 
   (* Constructors *)
-  | TacLeft (ev,bl) -> TacLeft (ev,subst_bindings subst bl)
-  | TacRight (ev,bl) -> TacRight (ev,subst_bindings subst bl)
   | TacSplit (ev,b,bll) -> TacSplit (ev,b,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)