Unification des types + clause filtrage manquante + uniformisation locale

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

3 files changed, 14 insertions, 10 deletions

diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 5a32d2e423..3e8a3f597a 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -173,6 +173,7 @@ let string_of_hole_kind = function
   | CasesType -> "CasesType"
   | InternalHole -> "InternalHole"
   | TomatchTypeParameter _ -> "TomatchTypeParameter"
+  | GoalEvar -> "GoalEvar"
       
 let evars_of_term evc init c = 
   let rec evrec acc c =
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 72095e6c49..5497d98d18 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -20,11 +20,11 @@ open Inductiveops
 open Typeops
 open Evd
 
-let meta_type env mv =
+let meta_type evd mv =
   let ty =
-    try Evd.meta_ftype env mv
+    try Evd.meta_ftype evd mv
     with Not_found -> error ("unknown meta ?"^string_of_int mv) in
-  meta_instance env ty
+  meta_instance evd ty
 
 let vect_lift = Array.mapi lift
 let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 3245ec3fce..f23ce7e636 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -338,7 +338,7 @@ let unify_to_type env evd mod_delta c u =
   let sigma = evars_of evd in
   let c = refresh_universes c in
   let t = get_type_of_with_meta env sigma (metas_of evd) c in
-  let t = Tacred.hnf_constr env sigma (nf_betaiota t) in
+  let t = Tacred.hnf_constr env sigma (nf_betaiota (nf_meta evd t)) in
   let u = Tacred.hnf_constr env sigma u in
   try unify_0 env sigma Cumul mod_delta t u
   with e when precatchable_exception e -> ([],[])
@@ -410,12 +410,15 @@ let w_merge env with_types mod_delta metas evars evd =
     match metas with
     | (mv,c,(status,to_type))::metas ->
         let ((evd,c),(metas'',evars'')),eqns =
-	  if with_types & to_type = CoerceToType then
-            (* Some coercion may have to be inserted *)
-	    (unify_or_coerce_type env evd mod_delta mv c,[])
-	  else
-            (* No coercion needed: delay the unification of types *)
-	    ((evd,c),([],[])),(mv,c)::eqns in
+	  if with_types & to_type <> TypeProcessed then
+	    if to_type = CoerceToType then
+              (* Some coercion may have to be inserted *)
+	      (unify_or_coerce_type env evd mod_delta mv c,[])
+	    else
+              (* No coercion needed: delay the unification of types *)
+	      ((evd,c),([],[])),(mv,c)::eqns
+	  else 
+	    ((evd,c),([],[])),eqns in
     	if meta_defined evd mv then
 	  let {rebus=c'},(status',_) = meta_fvalue evd mv in
           let (take_left,st,(metas',evars')) =