New tactics : econstructor, eleft, eright, esplit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4929 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 29 insertions, 15 deletions

diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 0f4bc93a83..c37e41a012 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -33,6 +33,7 @@ let rec make_rawwit loc = function
   | RedExprArgType -> <:expr< Genarg.rawwit_red_expr >>
   | CastedOpenConstrArgType -> <:expr< Genarg.rawwit_casted_open_constr >>
   | ConstrWithBindingsArgType -> <:expr< Genarg.rawwit_constr_with_bindings >>
+  | WithBindingsArgType -> <:expr< Genarg.rawwit_with_bindings >>
   | List0ArgType t -> <:expr< Genarg.wit_list0 $make_rawwit loc t$ >>
   | List1ArgType t -> <:expr< Genarg.wit_list1 $make_rawwit loc t$ >>
   | OptArgType t -> <:expr< Genarg.wit_opt $make_rawwit loc t$ >>
@@ -56,6 +57,7 @@ let rec make_globwit loc = function
   | RedExprArgType -> <:expr< Genarg.globwit_red_expr >>
   | CastedOpenConstrArgType -> <:expr< Genarg.globwit_casted_open_constr >>
   | ConstrWithBindingsArgType -> <:expr< Genarg.globwit_constr_with_bindings >>
+  | WithBindingsArgType -> <:expr< Genarg.globwit_with_bindings >>
   | List0ArgType t -> <:expr< Genarg.wit_list0 $make_globwit loc t$ >>
   | List1ArgType t -> <:expr< Genarg.wit_list1 $make_globwit loc t$ >>
   | OptArgType t -> <:expr< Genarg.wit_opt $make_globwit loc t$ >>
@@ -79,6 +81,7 @@ let rec make_wit loc = function
   | RedExprArgType -> <:expr< Genarg.wit_red_expr >>
   | CastedOpenConstrArgType -> <:expr< Genarg.wit_casted_open_constr >>
   | ConstrWithBindingsArgType -> <:expr< Genarg.wit_constr_with_bindings >>
+  | WithBindingsArgType -> <:expr< Genarg.wit_with_bindings >>
   | List0ArgType t -> <:expr< Genarg.wit_list0 $make_wit loc t$ >>
   | List1ArgType t -> <:expr< Genarg.wit_list1 $make_wit loc t$ >>
   | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >>
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 9c450101b0..01b59dcf65 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -62,8 +62,8 @@ let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2)
 
 if !Options.v7 then
 GEXTEND Gram
-  GLOBAL: simple_tactic constrarg constr_with_bindings quantified_hypothesis
-    red_expr int_or_var castedopenconstr;
+  GLOBAL: simple_tactic constrarg with_bindings constr_with_bindings 
+  quantified_hypothesis red_expr int_or_var castedopenconstr;
 
   int_or_var:
     [ [ n = integer  -> Genarg.ArgArg n
@@ -161,9 +161,9 @@ GEXTEND Gram
 	  ImplicitBindings (c1 :: bl) ] ]
   ;
   constr_with_bindings:
-    [ [ c = constr; l = with_binding_list -> (c, l) ] ]
+    [ [ c = constr; l = with_bindings -> (c, l) ] ]
   ;
-  with_binding_list:
+  with_bindings:
     [ [ "with"; bl = binding_list -> bl | -> NoBindings ] ]
   ;
   unfold_occ:
@@ -343,12 +343,12 @@ GEXTEND Gram
 	  id2 = id_or_ltac_ref -> TacRename (id1,id2)
 
       (* Constructors *)
-      | IDENT "Left"; bl = with_binding_list -> TacLeft bl
-      | IDENT "Right"; bl = with_binding_list -> TacRight bl
-      | IDENT "Split"; bl = with_binding_list -> TacSplit (false,bl)
+      | IDENT "Left"; bl = with_bindings -> TacLeft bl
+      | IDENT "Right"; bl = with_bindings -> TacRight bl
+      | IDENT "Split"; bl = with_bindings -> TacSplit (false,bl)
       | IDENT "Exists"; bl = binding_list -> TacSplit (true,bl)
       | IDENT "Exists" -> TacSplit (true,NoBindings)
-      | IDENT "Constructor"; n = num_or_meta; l = with_binding_list ->
+      | IDENT "Constructor"; n = num_or_meta; l = with_bindings ->
 	  TacConstructor (n,l)
       | IDENT "Constructor"; t = OPT tactic -> TacAnyConstructor t
 
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 96805e87b0..8151a8c14f 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -128,7 +128,7 @@ let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2)
 if not !Options.v7 then
 GEXTEND Gram
   GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
-    red_expr int_or_var castedopenconstr;
+ with_bindings red_expr int_or_var castedopenconstr;
 
   int_or_var:
     [ [ n = integer  -> Genarg.ArgArg n
@@ -211,9 +211,9 @@ GEXTEND Gram
       | bl = LIST1 constr -> ImplicitBindings bl ] ]
   ;
   constr_with_bindings:
-    [ [ c = constr; l = with_binding_list -> (c, l) ] ]
+    [ [ c = constr; l = with_bindings -> (c, l) ] ]
   ;
-  with_binding_list:
+  with_bindings:
     [ [ "with"; bl = binding_list -> bl | -> NoBindings ] ]
   ;
   red_flag:
@@ -387,12 +387,12 @@ GEXTEND Gram
 	  TacRename (id1,id2)
 
       (* Constructors *)
-      | IDENT "left"; bl = with_binding_list -> TacLeft bl
-      | IDENT "right"; bl = with_binding_list -> TacRight bl
-      | IDENT "split"; bl = with_binding_list -> TacSplit (false,bl)
+      | IDENT "left"; bl = with_bindings -> TacLeft bl
+      | IDENT "right"; bl = with_bindings -> TacRight bl
+      | IDENT "split"; bl = with_bindings -> TacSplit (false,bl)
       | "exists"; bl = binding_list -> TacSplit (true,bl)
       | "exists" -> TacSplit (true,NoBindings)
-      | IDENT "constructor"; n = num_or_meta; l = with_binding_list ->
+      | IDENT "constructor"; n = num_or_meta; l = with_bindings ->
 	  TacConstructor (n,l)
       | IDENT "constructor"; t = OPT tactic -> TacAnyConstructor t
 
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 759030fbe5..32ab9894ed 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -369,6 +369,8 @@ module Tactic =
       make_gen_entry utactic rawwit_casted_open_constr "castedopenconstr"
     let constr_with_bindings =
       make_gen_entry utactic rawwit_constr_with_bindings "constr_with_bindings"
+    let with_bindings =
+      make_gen_entry utactic rawwit_with_bindings "with_bindings"
     let constrarg = make_gen_entry utactic rawwit_constr_may_eval "constrarg"
     let quantified_hypothesis =
       make_gen_entry utactic rawwit_quant_hyp "quantified_hypothesis"
@@ -410,6 +412,7 @@ let reset_all_grammars () =
   f Tactic.simple_tactic;
   f Tactic.castedopenconstr;
   f Tactic.constr_with_bindings;
+  f Tactic.with_bindings;
   f Tactic.constrarg;
   f Tactic.quantified_hypothesis;
   f Tactic.int_or_var;
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index a91a3592dd..cbf416acc8 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -154,6 +154,7 @@ module Tactic :
     open Rawterm
     val castedopenconstr : constr_expr Gram.Entry.e
     val constr_with_bindings : constr_expr with_bindings Gram.Entry.e
+    val with_bindings : constr_expr bindings Gram.Entry.e
     val constrarg : (constr_expr,reference) may_eval Gram.Entry.e
     val quantified_hypothesis : quantified_hypothesis Gram.Entry.e
     val int_or_var : int or_var Gram.Entry.e
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 12e57e85f9..d7b2cbe449 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -268,6 +268,8 @@ let rec pr_raw_generic prc prlc prtac prref x =
       pr_arg prc (out_gen rawwit_casted_open_constr x)
   | ConstrWithBindingsArgType -> 
       pr_arg (pr_with_bindings prc prlc) (out_gen rawwit_constr_with_bindings x)
+  | WithBindingsArgType -> 
+      pr_arg (pr_bindings prc prlc) (out_gen rawwit_with_bindings x)
   | List0ArgType _ -> 
       hov 0 (fold_list0 (fun x a -> pr_raw_generic prc prlc prtac prref x ++ a) x (mt()))
   | List1ArgType _ ->
@@ -311,6 +313,8 @@ let rec pr_glob_generic prc prlc prtac x =
       pr_arg prc (out_gen globwit_casted_open_constr x)
   | ConstrWithBindingsArgType -> 
       pr_arg (pr_with_bindings prc prlc) (out_gen globwit_constr_with_bindings x)
+  | WithBindingsArgType -> 
+      pr_arg (pr_bindings prc prlc) (out_gen globwit_with_bindings x)
   | List0ArgType _ -> 
       hov 0 (fold_list0 (fun x a -> pr_glob_generic prc prlc prtac x ++ a) x (mt()))
   | List1ArgType _ ->
@@ -353,6 +357,8 @@ let rec pr_generic prc prlc prtac x =
       pr_arg prc (snd (out_gen wit_casted_open_constr x))
   | ConstrWithBindingsArgType -> 
       pr_arg (pr_with_bindings prc prlc) (out_gen wit_constr_with_bindings x)
+  | WithBindingsArgType -> 
+      pr_arg (pr_bindings prc prlc) (out_gen wit_with_bindings x)
   | List0ArgType _ -> 
       hov 0 (fold_list0 (fun x a -> pr_generic prc prlc prtac x ++ a) x (mt()))
   | List1ArgType _ ->
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index decb60923d..06b1b8bf99 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -252,6 +252,7 @@ let rec mlexpr_of_argtype loc = function
   | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >>
   | Genarg.CastedOpenConstrArgType -> <:expr< Genarg.CastedOpenConstrArgType >>
   | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >>
+  | Genarg.WithBindingsArgType -> <:expr< Genarg.WithBindingsArgType >>
   | Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >>
   | Genarg.TacticArgType -> <:expr< Genarg.TacticArgType >>
   | Genarg.SortArgType -> <:expr< Genarg.SortArgType >>