Restauration type casted_open_constr pour tactique refine car l'unification n'est pas assez puissante pour retarder la coercion vers le but au dernier moment

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

7 files changed, 20 insertions, 10 deletions

diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 78128a99d8..061efa49e8 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 >>
-  | OpenConstrArgType -> <:expr< Genarg.rawwit_open_constr >>
+  | OpenConstrArgType b -> <:expr< Genarg.rawwit_open_constr_gen $mlexpr_of_bool b$ >>
   | 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 >>
-  | OpenConstrArgType -> <:expr< Genarg.globwit_open_constr >>
+  | OpenConstrArgType b -> <:expr< Genarg.globwit_open_constr_gen $mlexpr_of_bool b$ >>
   | 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 >>
-  | OpenConstrArgType -> <:expr< Genarg.wit_open_constr >>
+  | OpenConstrArgType b -> <:expr< Genarg.wit_open_constr_gen $mlexpr_of_bool b$ >>
   | 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 b4e562706f..8274092187 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 open_constr
+  quantified_hypothesis red_expr int_or_var open_constr casted_open_constr
   simple_intropattern;
 
   int_or_var:
@@ -99,6 +99,9 @@ GEXTEND Gram
   open_constr:
     [ [ c = constr -> ((),c) ] ]
   ;
+  casted_open_constr:
+    [ [ c = constr -> ((),c) ] ]
+  ;
   induction_arg:
     [ [ n = natural -> ElimOnAnonHyp n
       | c = constr -> induction_arg_of_constr c
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index d869c5522c..dfb90f610d 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -109,7 +109,8 @@ 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 open_constr simple_intropattern;
+  bindings red_expr int_or_var open_constr casted_open_constr 
+  simple_intropattern;
 
   int_or_var:
     [ [ n = integer  -> Genarg.ArgArg n
@@ -131,6 +132,9 @@ GEXTEND Gram
   open_constr:
     [ [ c = constr -> ((),c) ] ]
   ;
+  casted_open_constr:
+    [ [ c = constr -> ((),c) ] ]
+  ;
   induction_arg:
     [ [ n = natural -> ElimOnAnonHyp n
       | c = constr -> induction_arg_of_constr c
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index cc00806a5f..73e0b4cc87 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -372,7 +372,9 @@ module Tactic =
     (* Entries that can be refered via the string -> Gram.Entry.e table *)
     (* Typically for tactic user extensions *)
     let open_constr = 
-      make_gen_entry utactic rawwit_open_constr "open_constr"
+      make_gen_entry utactic (rawwit_open_constr_gen false) "open_constr"
+    let casted_open_constr =
+      make_gen_entry utactic (rawwit_open_constr_gen true) "casted_open_constr"
     let constr_with_bindings =
       make_gen_entry utactic rawwit_constr_with_bindings "constr_with_bindings"
     let bindings =
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 9c88106ee0..1d7b8345f3 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -157,6 +157,7 @@ module Tactic :
   sig
     open Rawterm
     val open_constr : open_constr_expr Gram.Entry.e
+    val casted_open_constr : 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 76c9847efd..c1f3790696 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -272,7 +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)
-  | OpenConstrArgType -> pr_arg prc (snd (out_gen rawwit_open_constr x))
+  | OpenConstrArgType b -> pr_arg prc (snd (out_gen (rawwit_open_constr_gen b) x))
   | ConstrWithBindingsArgType -> 
       pr_arg (pr_with_bindings prc prlc) (out_gen rawwit_constr_with_bindings x)
   | BindingsArgType -> 
@@ -319,7 +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)
-  | OpenConstrArgType -> pr_arg prc (snd (out_gen globwit_open_constr x))
+  | OpenConstrArgType b -> pr_arg prc (snd (out_gen (globwit_open_constr_gen b) x))
   | ConstrWithBindingsArgType -> 
       pr_arg (pr_with_bindings prc prlc) (out_gen globwit_constr_with_bindings x)
   | BindingsArgType -> 
@@ -365,7 +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)
-  | OpenConstrArgType -> pr_arg prc (snd (out_gen wit_open_constr x))
+  | OpenConstrArgType b -> pr_arg prc (snd (out_gen (wit_open_constr_gen b) 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 a4c58aec97..a7c4a12af6 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.OpenConstrArgType -> <:expr< Genarg.OpenConstrArgType >>
+  | Genarg.OpenConstrArgType b -> <:expr< Genarg.OpenConstrArgType $mlexpr_of_bool b$ >>
   | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >>
   | Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >>
   | Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >>