Déplacement de la coercion vis à vis du but au niveau de Refine

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

1 files changed, 1 insertions, 10 deletions

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index fd8efc5f91..4a68cbe9fc 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -158,17 +158,8 @@ END
 
 open Refine
 
-let coerce_to_goal tac (sigma,c) gl =
-  let env = Tacmach.pf_env gl in
-  let evars = Evd.create_evar_defs sigma in
-  let j = Retyping.get_judgment_of env sigma c in
-  let ccl = Tacmach.pf_concl gl in
-  let (evars,j) = Coercion.inh_conv_coerce_to Util.dummy_loc env evars j ccl in
-  let sigma = Evd.evars_of evars in
-  tac (sigma,Reductionops.nf_evar sigma j.Environ.uj_val) gl
-
 TACTIC EXTEND Refine
-  [ "Refine" openconstr(c) ] -> [ coerce_to_goal refine c ]
+  [ "Refine" openconstr(c) ] -> [ refine c ]
 END
 
 let refine_tac = h_refine