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

3 files changed, 16 insertions, 27 deletions

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))