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

13 files changed, 62 insertions, 47 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 6758576370..78f4984c38 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -887,7 +887,7 @@ and xlate_tac =
 		   | _ -> assert false)
 	    | _ -> assert false)
     | TacExtend (_, "refine", [c]) ->
-       CT_refine (xlate_formula (snd (out_gen rawwit_open_constr c)))
+       CT_refine (xlate_formula (snd (out_gen rawwit_casted_open_constr c)))
     | TacExtend (_,"absurd",[c]) ->
        CT_absurd (xlate_formula (out_gen rawwit_constr c))
     | TacExtend (_,"contradiction",[opt_c]) ->
@@ -1237,11 +1237,11 @@ and coerce_genarg_to_TARG x =
   | TacticArgType ->
       let t = xlate_tactic (out_gen rawwit_tactic x) in
       CT_coerce_TACTIC_COM_to_TARG t
-  | OpenConstrArgType -> 
+  | OpenConstrArgType b -> 
       CT_coerce_SCOMMENT_CONTENT_to_TARG
       	(CT_coerce_FORMULA_to_SCOMMENT_CONTENT(xlate_formula
-						 (snd (out_gen
-						    rawwit_open_constr x))))
+					 (snd (out_gen
+					    (rawwit_open_constr_gen b) x))))
   | ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings"
   | BindingsArgType -> xlate_error "TODO: generic with bindings"
   | RedExprArgType -> xlate_error "TODO: generic red expr"
@@ -1331,7 +1331,7 @@ let coerce_genarg_to_VARG x =
   | TacticArgType ->
       let t = xlate_tactic (out_gen rawwit_tactic x) in
       CT_coerce_TACTIC_OPT_to_VARG (CT_coerce_TACTIC_COM_to_TACTIC_OPT t)
-  | OpenConstrArgType -> xlate_error "TODO: generic open constr"
+  | OpenConstrArgType _ -> xlate_error "TODO: generic open constr"
   | ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings"
   | BindingsArgType -> xlate_error "TODO: generic with bindings"
   | RedExprArgType -> xlate_error "TODO: red expr as generic argument"
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 3483695ecf..2b01a20344 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -34,7 +34,7 @@ type argument_type =
   | ConstrMayEvalArgType
   | QuantHypArgType
   | TacticArgType
-  | OpenConstrArgType
+  | OpenConstrArgType of bool
   | ConstrWithBindingsArgType
   | BindingsArgType
   | RedExprArgType
@@ -144,9 +144,17 @@ let rawwit_tactic = TacticArgType
 let globwit_tactic = TacticArgType
 let wit_tactic = TacticArgType
 
-let rawwit_open_constr = OpenConstrArgType
-let globwit_open_constr = OpenConstrArgType
-let wit_open_constr = OpenConstrArgType
+let rawwit_open_constr_gen b = OpenConstrArgType b
+let globwit_open_constr_gen b = OpenConstrArgType b 
+let wit_open_constr_gen b = OpenConstrArgType b
+
+let rawwit_open_constr = rawwit_open_constr_gen false
+let globwit_open_constr = globwit_open_constr_gen false
+let wit_open_constr = wit_open_constr_gen false
+
+let rawwit_casted_open_constr = rawwit_open_constr_gen true
+let globwit_casted_open_constr = globwit_open_constr_gen true
+let wit_casted_open_constr = wit_open_constr_gen true
 
 let rawwit_constr_with_bindings = ConstrWithBindingsArgType
 let globwit_constr_with_bindings = ConstrWithBindingsArgType
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 7f01cd6ace..af02a9ebe6 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -132,10 +132,18 @@ val rawwit_constr_may_eval : ((constr_expr,reference) may_eval,constr_expr,'ta)
 val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) may_eval,rawconstr_and_expr,'ta) abstract_argument_type
 val wit_constr_may_eval : (constr,constr,'ta) abstract_argument_type
 
+val rawwit_open_constr_gen : bool -> (open_constr_expr,constr_expr,'ta) abstract_argument_type
+val globwit_open_constr_gen : bool -> (open_rawconstr,rawconstr_and_expr,'ta) abstract_argument_type
+val wit_open_constr_gen : bool -> (open_constr,constr,'ta) abstract_argument_type
+
 val rawwit_open_constr : (open_constr_expr,constr_expr,'ta) abstract_argument_type
 val globwit_open_constr : (open_rawconstr,rawconstr_and_expr,'ta) abstract_argument_type
 val wit_open_constr : (open_constr,constr,'ta) abstract_argument_type
 
+val rawwit_casted_open_constr : (open_constr_expr,constr_expr,'ta) abstract_argument_type
+val globwit_casted_open_constr : (open_rawconstr,rawconstr_and_expr,'ta) abstract_argument_type
+val wit_casted_open_constr : (open_constr,constr,'ta) abstract_argument_type
+
 val rawwit_constr_with_bindings : (constr_expr with_bindings,constr_expr,'ta) abstract_argument_type
 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
@@ -227,7 +235,7 @@ type argument_type =
   | ConstrMayEvalArgType
   | QuantHypArgType
   | TacticArgType
-  | OpenConstrArgType
+  | OpenConstrArgType of bool
   | ConstrWithBindingsArgType
   | BindingsArgType
   | RedExprArgType
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 >>
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index b1ba9db486..edf99f175d 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -159,7 +159,7 @@ END
 open Refine
 
 TACTIC EXTEND Refine
-  [ "Refine" open_constr(c) ] -> [ refine c ]
+  [ "Refine" casted_open_constr(c) ] -> [ refine c ]
 END
 
 let refine_tac = h_refine
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 169e51467c..db4c52020b 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -333,23 +333,10 @@ let rec tcc_aux subst (TH (c,mm,sgp) as th) gl =
             (function None -> tclIDTAC | Some th -> tcc_aux subst th) sgp)
 	  gl
 
-
-(* La coercion face au but était faite auparavant dans Tacinterp *)
-
-let coerce_to_goal (sigma,c) gl =
-  let env = pf_env gl in
-  let evars = Evd.create_evar_defs sigma in
-  let j = Retyping.get_judgment_of env sigma c in
-  let ccl = pf_concl gl in
-  let (evars,j) = Coercion.inh_conv_coerce_to dummy_loc env evars j ccl in
-  let sigma = Evd.evars_of evars in
-  (sigma,Reductionops.nf_evar sigma j.Environ.uj_val)
-
 (* Et finalement la tactique refine elle-même : *)
 
 let refine oc gl =
   let sigma = project gl in
-  let oc = coerce_to_goal oc gl in
   let (_gmm,c) = Evarutil.exist_to_meta sigma oc in
   (* Relies on Cast's put on Meta's by exist_to_meta, because it is otherwise 
      complicated to update gmm when passing through a binder *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a53724b643..33d375dffe 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -885,9 +885,9 @@ and intern_genarg ist x =
       in_gen globwit_red_expr (intern_redexp ist (out_gen rawwit_red_expr x))
   | TacticArgType ->
       in_gen globwit_tactic (intern_tactic ist (out_gen rawwit_tactic x))
-  | OpenConstrArgType ->
-      in_gen globwit_open_constr 
-        ((),intern_constr ist (snd (out_gen rawwit_open_constr x)))
+  | OpenConstrArgType b ->
+      in_gen (globwit_open_constr_gen b)
+        ((),intern_constr ist (snd (out_gen (rawwit_open_constr_gen b) x)))
   | ConstrWithBindingsArgType ->
       in_gen globwit_constr_with_bindings
         (intern_constr_with_bindings ist (out_gen rawwit_constr_with_bindings x))
@@ -1195,18 +1195,19 @@ let interp_constr ist sigma env c =
   interp_casted_constr None ist sigma env c
 
 (* Interprets an open constr expression *)
-let pf_interp_openconstr ist gl (c,ce) =
+let pf_interp_open_constr casted ist gl (c,ce) =
   let sigma = project gl in
   let env = pf_env gl in
   let (ltacvars,l) = constr_list ist env in
   let typs = retype_list sigma env ltacvars in
+  let ocl = if casted then Some (pf_concl gl) else None in
   match ce with
   | None ->
-      Pretyping.understand_gen_tcc sigma env typs None c
+      Pretyping.understand_gen_tcc sigma env typs ocl c
     (* If at toplevel (ce<>None), the error can be due to an incorrect
        context at globalization time: we retype with the now known
        intros/lettac/inversion hypothesis names *)
-  | Some c -> interp_openconstr_gen sigma env (ltacvars,l) c None
+  | Some c -> interp_openconstr_gen sigma env (ltacvars,l) c ocl
 
 (* Interprets a constr expression *)
 let pf_interp_constr ist gl =
@@ -1585,9 +1586,10 @@ and interp_genarg ist goal x =
   | RedExprArgType ->
       in_gen wit_red_expr (pf_redexp_interp ist goal (out_gen globwit_red_expr x))
   | TacticArgType -> in_gen wit_tactic (out_gen globwit_tactic x)
-  | OpenConstrArgType ->
-      in_gen wit_open_constr 
-        (pf_interp_openconstr ist goal (snd (out_gen globwit_open_constr x)))
+  | OpenConstrArgType casted ->
+      in_gen (wit_open_constr_gen casted) 
+        (pf_interp_open_constr casted ist goal 
+          (snd (out_gen (globwit_open_constr_gen casted) x)))
   | ConstrWithBindingsArgType ->
       in_gen wit_constr_with_bindings
         (interp_constr_with_bindings ist goal (out_gen globwit_constr_with_bindings x))
@@ -1800,7 +1802,7 @@ and interp_atomic ist gl = function
 	val_interp ist gl (out_gen globwit_tactic x)
     | StringArgType | BoolArgType
     | QuantHypArgType | RedExprArgType 
-    | OpenConstrArgType | ConstrWithBindingsArgType | BindingsArgType 
+    | OpenConstrArgType _ | ConstrWithBindingsArgType | BindingsArgType 
     | ExtraArgType _ | List0ArgType _ | List1ArgType _ | OptArgType _ | PairArgType _ 
 	-> error "This generic type is not supported in alias"
     in
@@ -2087,9 +2089,9 @@ and subst_genarg subst (x:glob_generic_argument) =
       in_gen globwit_red_expr (subst_redexp subst (out_gen globwit_red_expr x))
   | TacticArgType ->
       in_gen globwit_tactic (subst_tactic subst (out_gen globwit_tactic x))
-  | OpenConstrArgType ->
-      in_gen globwit_open_constr 
-        ((),subst_rawconstr subst (snd (out_gen globwit_open_constr x)))
+  | OpenConstrArgType b ->
+      in_gen (globwit_open_constr_gen b)
+        ((),subst_rawconstr subst (snd (out_gen (globwit_open_constr_gen b) x)))
   | ConstrWithBindingsArgType ->
       in_gen globwit_constr_with_bindings
         (subst_raw_with_bindings subst (out_gen globwit_constr_with_bindings x))