suppression warning et calcule type dans replace_by_meta dans tous les cas

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

1 files changed, 10 insertions, 4 deletions

diff --git a/tactics/refine.ml b/tactics/refine.ml
index a63cfe975..8ec991c0f 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -94,12 +94,13 @@ let replace_by_meta env = function
 	    mkNamedProd id c1 (snd (destCast c2))
 	| IsLambda (Anonymous,c1,c2) when isCast c2 ->
 	    mkArrow c1 (snd (destCast c2))
-	| (IsApp _ | IsMutCase _) ->
-	    (** let j = ise_resolve true empty_evd mm (gLOB sign) c in **)
+	| _ -> (* (IsApp _ | IsMutCase _) -> *)
 	    Retyping.get_type_of_with_meta env Evd.empty mm c
+	(*
 	| IsFix ((_,j),(v,_,_)) ->
 	    v.(j) (* en pleine confiance ! *)
 	| _ -> invalid_arg "Tcc.replace_by_meta (TO DO)" 
+        *)
       in
       mkCast (m,ty),[n,ty],[Some th]
 
@@ -124,13 +125,18 @@ let fresh env n =
 let rec compute_metamap env c = match kind_of_term c with
   (* le terme est directement une preuve *)
   | (IsConst _ | IsEvar _ | IsMutInd _ | IsMutConstruct _ |
-    IsSort _ | IsVar _ | IsRel _) -> TH (c,[],[])
+    IsSort _ | IsVar _ | IsRel _) -> 
+      TH (c,[],[])
 
   (* le terme est une mv => un but *)
   | IsMeta n ->
+      (* 
       Pp.warning (Printf.sprintf ("compute_metamap: MV(%d) sans type !\n") n);
+      let ty = Retyping.get_type_of_with_meta env Evd.empty lmeta c in 
+      *)
       TH (c,[],[None])
-  | IsCast (m,ty) when isMeta m -> TH (c,[destMeta m,ty],[None])
+  | IsCast (m,ty) when isMeta m -> 
+      TH (c,[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)