From 2f783e7beaabe671e306925fdf4e1f3aac06e659 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 6 Dec 2004 15:18:50 +0000
Subject: 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
---
 tactics/extratactics.ml4 | 11 +----------
 1 file changed, 1 insertion(+), 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
-- 
cgit v1.2.3