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

2 files changed, 22 insertions, 18 deletions

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 60a6972b8..631aee59d 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 488e8833c..3434299ab 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