Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tactiques d'appliquer une éventuelle coercion vers le but

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

7 files changed, 17 insertions, 20 deletions

diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index df48f5d8d..78128a99d 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -33,7 +33,7 @@ let rec make_rawwit loc = function
   | QuantHypArgType -> <:expr< Genarg.rawwit_quant_hyp >>
   | TacticArgType -> <:expr< Genarg.rawwit_tactic >>
   | RedExprArgType -> <:expr< Genarg.rawwit_red_expr >>
-  | CastedOpenConstrArgType -> <:expr< Genarg.rawwit_casted_open_constr >>
+  | OpenConstrArgType -> <:expr< Genarg.rawwit_open_constr >>
   | ConstrWithBindingsArgType -> <:expr< Genarg.rawwit_constr_with_bindings >>
   | BindingsArgType -> <:expr< Genarg.rawwit_bindings >>
   | List0ArgType t -> <:expr< Genarg.wit_list0 $make_rawwit loc t$ >>
@@ -59,7 +59,7 @@ let rec make_globwit loc = function
   | ConstrMayEvalArgType -> <:expr< Genarg.globwit_constr_may_eval >>
   | TacticArgType -> <:expr< Genarg.globwit_tactic >>
   | RedExprArgType -> <:expr< Genarg.globwit_red_expr >>
-  | CastedOpenConstrArgType -> <:expr< Genarg.globwit_casted_open_constr >>
+  | OpenConstrArgType -> <:expr< Genarg.globwit_open_constr >>
   | ConstrWithBindingsArgType -> <:expr< Genarg.globwit_constr_with_bindings >>
   | BindingsArgType -> <:expr< Genarg.globwit_bindings >>
   | List0ArgType t -> <:expr< Genarg.wit_list0 $make_globwit loc t$ >>
@@ -85,7 +85,7 @@ let rec make_wit loc = function
   | ConstrMayEvalArgType -> <:expr< Genarg.wit_constr_may_eval >>
   | TacticArgType -> <:expr< Genarg.wit_tactic >>
   | RedExprArgType -> <:expr< Genarg.wit_red_expr >>
-  | CastedOpenConstrArgType -> <:expr< Genarg.wit_casted_open_constr >>
+  | OpenConstrArgType -> <:expr< Genarg.wit_open_constr >>
   | ConstrWithBindingsArgType -> <:expr< Genarg.wit_constr_with_bindings >>
   | BindingsArgType -> <:expr< Genarg.wit_bindings >>
   | List0ArgType t -> <:expr< Genarg.wit_list0 $make_wit loc t$ >>
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 5ba7d591e..97f5d46a9 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -42,7 +42,7 @@ let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2)
 if !Options.v7 then
 GEXTEND Gram
   GLOBAL: simple_tactic constrarg bindings constr_with_bindings 
-  quantified_hypothesis red_expr int_or_var castedopenconstr
+  quantified_hypothesis red_expr int_or_var openconstr
   simple_intropattern;
 
   int_or_var:
@@ -96,8 +96,8 @@ GEXTEND Gram
       | IDENT "Check"; c = constr -> ConstrTypeOf c
       | c = constr -> ConstrTerm c ] ]
   ;
-  castedopenconstr:
-    [ [ c = constr -> c ] ]
+  openconstr:
+    [ [ c = constr -> ((),c) ] ]
   ;
   induction_arg:
     [ [ n = natural -> ElimOnAnonHyp n
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 8930c8dca..70729ce13 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -109,7 +109,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
-  bindings red_expr int_or_var castedopenconstr simple_intropattern;
+  bindings red_expr int_or_var openconstr simple_intropattern;
 
   int_or_var:
     [ [ n = integer  -> Genarg.ArgArg n
@@ -128,8 +128,8 @@ GEXTEND Gram
       |	id = METAIDENT -> MetaId (loc,id)
       ] ]
   ;
-  castedopenconstr:
-    [ [ c = constr -> c ] ]
+  openconstr:
+    [ [ c = constr -> ((),c) ] ]
   ;
   induction_arg:
     [ [ n = natural -> ElimOnAnonHyp n
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 081d7aeec..496b6594d 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -371,8 +371,8 @@ module Tactic =
 
     (* Entries that can be refered via the string -> Gram.Entry.e table *)
     (* Typically for tactic user extensions *)
-    let castedopenconstr = 
-      make_gen_entry utactic rawwit_casted_open_constr "castedopenconstr"
+    let openconstr = 
+      make_gen_entry utactic rawwit_open_constr "openconstr"
     let constr_with_bindings =
       make_gen_entry utactic rawwit_constr_with_bindings "constr_with_bindings"
     let bindings =
@@ -418,7 +418,7 @@ let reset_all_grammars () =
   f Constr.ident; f Constr.global; f Constr.sort; f Constr.pattern;
   f Module.module_expr; f Module.module_type;
   f Tactic.simple_tactic;
-  f Tactic.castedopenconstr;
+  f Tactic.openconstr;
   f Tactic.constr_with_bindings;
   f Tactic.bindings;
   f Tactic.constrarg;
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index c2f1c0240..76c23ad20 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -156,7 +156,7 @@ module Module :
 module Tactic :
   sig
     open Rawterm
-    val castedopenconstr : constr_expr Gram.Entry.e
+    val openconstr : open_constr_expr Gram.Entry.e
     val constr_with_bindings : constr_expr with_bindings Gram.Entry.e
     val bindings : constr_expr bindings Gram.Entry.e
     val constrarg : (constr_expr,reference) may_eval Gram.Entry.e
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 3057e41a4..76c9847ef 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -272,8 +272,7 @@ let rec pr_raw_generic prc prlc prtac prref x =
       pr_arg (pr_red_expr 
         (prc,prref)) (out_gen rawwit_red_expr x)
   | TacticArgType -> pr_arg prtac (out_gen rawwit_tactic x)
-  | CastedOpenConstrArgType ->
-      pr_arg prc (out_gen rawwit_casted_open_constr x)
+  | OpenConstrArgType -> pr_arg prc (snd (out_gen rawwit_open_constr x))
   | ConstrWithBindingsArgType -> 
       pr_arg (pr_with_bindings prc prlc) (out_gen rawwit_constr_with_bindings x)
   | BindingsArgType -> 
@@ -320,8 +319,7 @@ let rec pr_glob_generic prc prlc prtac x =
       pr_arg (pr_red_expr 
         (prc,pr_or_var (pr_and_short_name pr_evaluable_reference))) (out_gen globwit_red_expr x)
   | TacticArgType -> pr_arg prtac (out_gen globwit_tactic x)
-  | CastedOpenConstrArgType ->
-      pr_arg prc (out_gen globwit_casted_open_constr x)
+  | OpenConstrArgType -> pr_arg prc (snd (out_gen globwit_open_constr x))
   | ConstrWithBindingsArgType -> 
       pr_arg (pr_with_bindings prc prlc) (out_gen globwit_constr_with_bindings x)
   | BindingsArgType -> 
@@ -367,8 +365,7 @@ let rec pr_generic prc prlc prtac x =
   | RedExprArgType ->
       pr_arg (pr_red_expr (prc,pr_evaluable_reference)) (out_gen wit_red_expr x)
   | TacticArgType -> pr_arg prtac (out_gen wit_tactic x)
-  | CastedOpenConstrArgType ->
-      pr_arg prc (snd (out_gen wit_casted_open_constr x))
+  | OpenConstrArgType -> pr_arg prc (snd (out_gen wit_open_constr x))
   | ConstrWithBindingsArgType -> 
       pr_arg (pr_with_bindings prc prlc) (out_gen wit_constr_with_bindings x)
   | BindingsArgType -> 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index e1bb51dd7..a4c58aec9 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -272,7 +272,7 @@ let rec mlexpr_of_argtype loc = function
   | Genarg.HypArgType -> <:expr< Genarg.HypArgType >>
   | Genarg.StringArgType -> <:expr< Genarg.StringArgType >>
   | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >>
-  | Genarg.CastedOpenConstrArgType -> <:expr< Genarg.CastedOpenConstrArgType >>
+  | Genarg.OpenConstrArgType -> <:expr< Genarg.OpenConstrArgType >>
   | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >>
   | Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >>
   | Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >>