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

1 files changed, 0 insertions, 13 deletions

diff --git a/tactics/refine.ml b/tactics/refine.ml
index 169e51467..db4c52020 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 *)