Moving left & right tactics out of the AST.

5 files changed, 49 insertions, 22 deletions

diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index f033ef5ca..bff5c13d3 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 2a6589d21..6dc11510d 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 3b1cdecfb..9f911564a 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 12547e704..734d5b894 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 1b15fa8e1..bea77a0b0 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)