Nouvelle tactique EExists

Changement des exports pour tactic EXTEND : with_bindings devient bindings qui prend plus le with, il faut le mettre à la main dans la règle.


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

13 files changed, 71 insertions, 51 deletions

diff --git a/CHANGES b/CHANGES
index a9a8698d98..e094fd2a81 100644
--- a/CHANGES
+++ b/CHANGES
@@ -190,6 +190,7 @@ Tactics
 - Field now works on types in Set
 - Auto with reals now try to replace le by ge (Rge_le is no longer an
   immediate hint), resulting in shorter proofs
+- Some new tactics : EConstructor, ELeft, Eright, ESplit, EExists
 
 Extraction (See details in contrib/extraction/CHANGES)
 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index e2460d332d..1739240e0f 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1102,7 +1102,7 @@ and coerce_genarg_to_TARG x =
 						 (out_gen
 						    rawwit_casted_open_constr x)))
   | ConstrWithBindingsArgType -> xlate_error "TODO: constr with bindings"
-  | WithBindingsArgType -> xlate_error "TODO: with bindings"
+  | BindingsArgType -> xlate_error "TODO: with bindings"
   | RedExprArgType -> xlate_error "TODO: red expr as generic argument"
   | List0ArgType l -> xlate_error "TODO: lists of generic arguments"
   | List1ArgType l -> xlate_error "TODO: non empty lists of generic arguments"
@@ -1184,7 +1184,7 @@ let coerce_genarg_to_VARG x =
       CT_coerce_TACTIC_OPT_to_VARG (CT_coerce_TACTIC_COM_to_TACTIC_OPT t)
   | CastedOpenConstrArgType -> xlate_error "TODO: open constr"
   | ConstrWithBindingsArgType -> xlate_error "TODO: constr with bindings"
-  | WithBindingsArgType -> xlate_error "TODO: with bindings"
+  | BindingsArgType -> xlate_error "TODO: with bindings"
   | RedExprArgType -> xlate_error "TODO: red expr as generic argument"
   | List0ArgType l -> xlate_error "TODO: lists of generic arguments"
   | List1ArgType l -> xlate_error "TODO: non empty lists of generic arguments"
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 0ed7b97f47..80248f7e5e 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -32,7 +32,7 @@ type argument_type =
   | TacticArgType
   | CastedOpenConstrArgType
   | ConstrWithBindingsArgType
-  | WithBindingsArgType
+  | BindingsArgType
   | RedExprArgType
   | List0ArgType of argument_type
   | List1ArgType of argument_type
@@ -121,9 +121,9 @@ let rawwit_constr_with_bindings = ConstrWithBindingsArgType
 let globwit_constr_with_bindings = ConstrWithBindingsArgType
 let wit_constr_with_bindings = ConstrWithBindingsArgType
 
-let rawwit_with_bindings = WithBindingsArgType
-let globwit_with_bindings = WithBindingsArgType
-let wit_with_bindings = WithBindingsArgType
+let rawwit_bindings = BindingsArgType
+let globwit_bindings = BindingsArgType
+let wit_bindings = BindingsArgType
 
 let rawwit_red_expr = RedExprArgType
 let globwit_red_expr = RedExprArgType
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 2418646d9b..23e1b5377d 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -60,7 +60,7 @@ ConstrMayEvalArgType           constr_expr may_eval     constr
 QuantHypArgType                quantified_hypothesis    quantified_hypothesis
 TacticArgType                  raw_tactic_expr          tactic
 CastedOpenConstrArgType        constr_expr              open_constr
-ConstrWithBindingsArgType      constr_expr with_bindings constr with_bindings
+ConstrBindingsArgType      constr_expr with_bindings constr with_bindings
 List0ArgType of argument_type
 List1ArgType of argument_type
 OptArgType of argument_type
@@ -121,9 +121,9 @@ val rawwit_constr_with_bindings : (constr_expr with_bindings,constr_expr,'ta) ab
 val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,rawconstr_and_expr,'ta) abstract_argument_type
 val wit_constr_with_bindings : (constr with_bindings,constr,'ta) abstract_argument_type
 
-val rawwit_with_bindings : (constr_expr bindings,constr_expr,'ta) abstract_argument_type
-val globwit_with_bindings : (rawconstr_and_expr bindings,rawconstr_and_expr,'ta) abstract_argument_type
-val wit_with_bindings : (constr bindings,constr,'ta) abstract_argument_type
+val rawwit_bindings : (constr_expr bindings,constr_expr,'ta) abstract_argument_type
+val globwit_bindings : (rawconstr_and_expr bindings,rawconstr_and_expr,'ta) abstract_argument_type
+val wit_bindings : (constr bindings,constr,'ta) abstract_argument_type
 
 val rawwit_red_expr : ((constr_expr,reference) red_expr_gen,constr_expr,'ta) abstract_argument_type
 val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,rawconstr_and_expr,'ta) abstract_argument_type
@@ -208,7 +208,7 @@ type argument_type =
   | TacticArgType
   | CastedOpenConstrArgType
   | ConstrWithBindingsArgType
-  | WithBindingsArgType
+  | BindingsArgType
   | RedExprArgType
   | List0ArgType of argument_type
   | List1ArgType of argument_type
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index c37e41a012..44a54a0cff 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -33,7 +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 >>
+  | BindingsArgType -> <:expr< Genarg.rawwit_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$ >>
@@ -57,7 +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 >>
+  | BindingsArgType -> <:expr< Genarg.globwit_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$ >>
@@ -81,7 +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 >>
+  | BindingsArgType -> <:expr< Genarg.wit_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 2416b14bd5..cf10f0c45d 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -62,7 +62,7 @@ let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2)
 
 if !Options.v7 then
 GEXTEND Gram
-  GLOBAL: simple_tactic constrarg with_bindings constr_with_bindings 
+  GLOBAL: simple_tactic constrarg bindings constr_with_bindings 
   quantified_hypothesis red_expr int_or_var castedopenconstr;
 
   int_or_var:
@@ -151,7 +151,7 @@ GEXTEND Gram
     [ [ id = base_ident; ":="; c = constr -> (loc, NamedHyp id, c)
       | n = natural; ":="; c = constr -> (loc, AnonHyp n, c) ] ]
   ;
-  binding_list:
+  bindings:
     [ [ c1 = constr; ":="; c2 = constr; bl = LIST0 simple_binding ->
           ExplicitBindings
             ((join_to_constr loc c2,NamedHyp (coerce_to_id c1), c2) :: bl)
@@ -164,7 +164,7 @@ GEXTEND Gram
     [ [ c = constr; l = with_bindings -> (c, l) ] ]
   ;
   with_bindings:
-    [ [ "with"; bl = binding_list -> bl | -> NoBindings ] ]
+    [ [ "with"; bl = bindings -> bl | -> NoBindings ] ]
   ;
   unfold_occ:
     [ [ nl = LIST0 integer; c = global_or_ltac_ref -> (nl,c) ] ]
@@ -346,7 +346,7 @@ GEXTEND Gram
       | 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"; bl = bindings -> TacSplit (true,bl)
       | IDENT "Exists" -> TacSplit (true,NoBindings)
       | IDENT "Constructor"; n = num_or_meta; l = with_bindings ->
 	  TacConstructor (n,l)
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 9ee0041804..8b5f9139de 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
- with_bindings red_expr int_or_var castedopenconstr;
+  bindings red_expr int_or_var castedopenconstr;
 
   int_or_var:
     [ [ n = integer  -> Genarg.ArgArg n
@@ -205,7 +205,7 @@ GEXTEND Gram
     [ [ "("; id = base_ident; ":="; c = lconstr; ")" -> (loc, NamedHyp id, c)
       | "("; n = natural; ":="; c = lconstr; ")" -> (loc, AnonHyp n, c) ] ]
   ;
-  binding_list:
+  bindings:
     [ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding ->
           ExplicitBindings bl
       | bl = LIST1 constr -> ImplicitBindings bl ] ]
@@ -214,7 +214,7 @@ GEXTEND Gram
     [ [ c = constr; l = with_bindings -> (c, l) ] ]
   ;
   with_bindings:
-    [ [ "with"; bl = binding_list -> bl | -> NoBindings ] ]
+    [ [ "with"; bl = bindings -> bl | -> NoBindings ] ]
   ;
   red_flag:
     [ [ IDENT "beta" -> FBeta
@@ -390,7 +390,7 @@ GEXTEND Gram
       | 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"; bl = bindings -> TacSplit (true,bl)
       | "exists" -> TacSplit (true,NoBindings)
       | IDENT "constructor"; n = num_or_meta; l = with_bindings ->
 	  TacConstructor (n,l)
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index b9ec4cfc2e..7cbda15980 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -371,8 +371,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 bindings =
+      make_gen_entry utactic rawwit_bindings "bindings"
     let constrarg = make_gen_entry utactic rawwit_constr_may_eval "constrarg"
     let quantified_hypothesis =
       make_gen_entry utactic rawwit_quant_hyp "quantified_hypothesis"
@@ -414,7 +414,7 @@ let reset_all_grammars () =
   f Tactic.simple_tactic;
   f Tactic.castedopenconstr;
   f Tactic.constr_with_bindings;
-  f Tactic.with_bindings;
+  f Tactic.bindings;
   f Tactic.constrarg;
   f Tactic.quantified_hypothesis;
   f Tactic.int_or_var;
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 0541d1cf73..1ad4bbfd8f 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -155,7 +155,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 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 8a97eb2d0f..8f313f1f37 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -114,6 +114,20 @@ let pr_bindings prc prlc = function
         l
   | NoBindings -> mt ()
 
+let pr_bindings_no_with prc prlc = function
+  | ImplicitBindings l ->
+      brk (1,1) ++
+      prlist_with_sep spc prc l
+  | ExplicitBindings l ->
+      brk (1,1) ++ 
+        prlist_with_sep spc
+          (fun b -> if Options.do_translate () or not !Options.v7 then
+	    str"(" ++ pr_binding prlc b ++ str")" 
+	   else
+	    pr_binding prc b)
+        l
+  | NoBindings -> mt ()
+
 let pr_with_bindings prc prlc (c,bl) =
   if Options.do_translate () then
     (* translator calls pr_with_bindings on rawconstr: we cast it! *)
@@ -268,8 +282,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)
+  | BindingsArgType -> 
+      pr_arg (pr_bindings_no_with prc prlc) (out_gen rawwit_bindings x)
   | List0ArgType _ -> 
       hov 0 (fold_list0 (fun x a -> pr_raw_generic prc prlc prtac prref x ++ a) x (mt()))
   | List1ArgType _ ->
@@ -313,8 +327,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)
+  | BindingsArgType -> 
+      pr_arg (pr_bindings_no_with prc prlc) (out_gen globwit_bindings x)
   | List0ArgType _ -> 
       hov 0 (fold_list0 (fun x a -> pr_glob_generic prc prlc prtac x ++ a) x (mt()))
   | List1ArgType _ ->
@@ -357,8 +371,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)
+  | BindingsArgType -> 
+      pr_arg (pr_bindings_no_with prc prlc) (out_gen wit_bindings x)
   | List0ArgType _ -> 
       hov 0 (fold_list0 (fun x a -> pr_generic prc prlc prtac x ++ a) x (mt()))
   | List1ArgType _ ->
@@ -398,6 +412,7 @@ let pr_extend_gen prgen s l =
 let make_pr_tac (pr_tac,pr_tac0,pr_constr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend) =
 
 let pr_bindings = pr_bindings pr_constr pr_constr in
+let pr_bindings_no_with = pr_bindings_no_with pr_constr pr_constr in
 let pr_with_bindings = pr_with_bindings pr_constr pr_constr in
 let pr_eliminator cb = str "using" ++ pr_arg (pr_with_bindings) cb in
 let pr_constrarg c = spc () ++ pr_constr c in
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 84efdbcac1..e4f90ffa81 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -255,7 +255,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.BindingsArgType -> <:expr< Genarg.BindingsArgType >>
   | Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >>
   | Genarg.TacticArgType -> <:expr< Genarg.TacticArgType >>
   | Genarg.SortArgType -> <:expr< Genarg.SortArgType >>
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 60a6972b81..631aee59dc 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -111,27 +111,31 @@ let e_split = e_constructor_tac (Some 1) 1
   [ "econstructor" integer(n) with_bindings(c) ] -> [ e_constructor_tac None n c ]
 END*)
 TACTIC EXTEND econstructor
-  [ "EConstructor" integer(n) with_bindings(c) ] -> [ e_constructor_tac None n c ]
+  [ "EConstructor" integer(n) "with" bindings(c) ] -> [ e_constructor_tac None n c ]
+  | [ "EConstructor" integer(n) ] -> [ e_constructor_tac None n NoBindings ]
   | [ "EConstructor" tactic_opt(t) ] -> [ e_any_constructor (option_app Tacinterp.eval_tactic t) ] 
-END
+      END
 
 TACTIC EXTEND eleft
-  [ "ELeft" with_bindings(l) ] -> [e_left l]
+  [ "ELeft" "with" bindings(l) ] -> [e_left l]
+  | [ "ELeft"] -> [e_left NoBindings]
 END
 
 TACTIC EXTEND eright
-  [ "ERight" with_bindings(l) ] -> [e_right l]
+  [ "ERight" "with" bindings(l) ] -> [e_right l]
+  | [ "ERight" ] -> [e_right NoBindings]
 END
 
 TACTIC EXTEND esplit
-  [ "ESplit" with_bindings(l) ] -> [e_split l]
+  [ "ESplit" "with" bindings(l) ] -> [e_split l]
+  | [ "ESplit"] -> [e_split NoBindings]
 END
 
-(*
+
 TACTIC EXTEND eexists
-  [ "EExists" with_bindings(l) ] -> [e_split l]
+  [ "EExists" bindings(l) ] -> [e_split l]
 END
-*)
+
 
 (************************************************************************)
 (*   PROLOG tactic                                                      *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 488e8833cc..3434299ab0 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -821,9 +821,9 @@ and intern_genarg ist x =
   | ConstrWithBindingsArgType ->
       in_gen globwit_constr_with_bindings
         (intern_constr_with_bindings ist (out_gen rawwit_constr_with_bindings x))
-  | WithBindingsArgType ->
-      in_gen globwit_with_bindings
-        (intern_bindings ist (out_gen rawwit_with_bindings x))
+  | BindingsArgType ->
+      in_gen globwit_bindings
+        (intern_bindings ist (out_gen rawwit_bindings x))
   | List0ArgType _ -> app_list0 (intern_genarg ist) x
   | List1ArgType _ -> app_list1 (intern_genarg ist) x
   | OptArgType _ -> app_opt (intern_genarg ist) x
@@ -1533,9 +1533,9 @@ and interp_genarg ist goal x =
   | ConstrWithBindingsArgType ->
       in_gen wit_constr_with_bindings
         (interp_constr_with_bindings ist goal (out_gen globwit_constr_with_bindings x))
-  | WithBindingsArgType ->
-      in_gen wit_with_bindings
-        (interp_bindings ist goal (out_gen globwit_with_bindings x))
+  | BindingsArgType ->
+      in_gen wit_bindings
+        (interp_bindings ist goal (out_gen globwit_bindings x))
   | List0ArgType _ -> app_list0 (interp_genarg ist goal) x
   | List1ArgType _ -> app_list1 (interp_genarg ist goal) x
   | OptArgType _ -> app_opt (interp_genarg ist goal) x
@@ -1728,7 +1728,7 @@ and interp_atomic ist gl = function
     | QuantHypArgType | RedExprArgType 
     | TacticArgType -> 
 	val_interp ist gl (out_gen globwit_tactic x)
-    | CastedOpenConstrArgType | ConstrWithBindingsArgType | WithBindingsArgType 
+    | CastedOpenConstrArgType | ConstrWithBindingsArgType | BindingsArgType 
     | ExtraArgType _ | List0ArgType _ | List1ArgType _ | OptArgType _ | PairArgType _ 
 	-> error "This generic type is not supported in alias"
     in
@@ -2017,9 +2017,9 @@ and subst_genarg subst (x:glob_generic_argument) =
   | ConstrWithBindingsArgType ->
       in_gen globwit_constr_with_bindings
         (subst_raw_with_bindings subst (out_gen globwit_constr_with_bindings x))
-  | WithBindingsArgType ->
-      in_gen globwit_with_bindings
-        (subst_bindings subst (out_gen globwit_with_bindings x))
+  | BindingsArgType ->
+      in_gen globwit_bindings
+        (subst_bindings subst (out_gen globwit_bindings x))
   | List0ArgType _ -> app_list0 (subst_genarg subst) x
   | List1ArgType _ -> app_list1 (subst_genarg subst) x
   | OptArgType _ -> app_opt (subst_genarg subst) x