From 44cafc5d7e5de836c096573f709f2465723240dc Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 6 Dec 2004 18:18:04 +0000
Subject: Suppression des cast après avoir utiliser l'information de type
 (Tacinv envoie à refine des métas castées avec des métas ?!)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6423 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/refine.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/tactics/refine.ml b/tactics/refine.ml
index bb80e361fc..7f69a9c95d 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -141,7 +141,7 @@ let rec compute_metamap env c = match kind_of_term c with
       *)
       TH (c,[],[None])
   | Cast (m,ty) when isMeta m -> 
-      TH (c,[destMeta m,ty],[None])
+      TH (m,[destMeta m,ty],[None])
 
   (* abstraction => il faut décomposer si le terme dessous n'est pas pur
    *    attention : dans ce cas il faut remplacer (Rel 1) par (Var x)
@@ -335,7 +335,8 @@ let rec tcc_aux subst (TH (c,mm,sgp) as th) gl =
             (function None -> tclIDTAC | Some th -> tcc_aux subst th) sgp)
 	  gl
 
-(* Et finalement la tactique refine elle-même : *)
+
+(* La coercion face au but était faite auparavant dans Tacinterp *)
 
 let coerce_to_goal (sigma,c) gl =
   let env = pf_env gl in
@@ -346,6 +347,8 @@ let coerce_to_goal (sigma,c) gl =
   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 env = pf_env gl in
-- 
cgit v1.2.3