Fix a bunch of bugs related to setoid_rewrite, unification and evars:

- Really unify with types of metas when they contain metas
_or_ evars (why not always?) (fixes bug #2027).
- Better handling of evars in rewrite lemmas when using setoid_rewrite
through rewrite (reported by Ralf Hinze).
- Use retyping with metas when possible (check?) and improve an
obscure error message in retyping.


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

2 files changed, 4 insertions, 4 deletions

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 532c258fa1..2460c7642a 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -49,7 +49,7 @@ let retype sigma metamap =
     match kind_of_term cstr with
     | Meta n ->
           (try strip_outer_cast (List.assoc n metamap)
-           with Not_found -> anomaly "type_of: this is not a well-typed term")
+           with Not_found -> anomaly ("type_of: unknown meta " ^ string_of_int n))
     | Rel n ->
         let (_,_,ty) = lookup_rel n env in
         lift n ty
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e072af3629..6c7ca8af2c 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -481,7 +481,7 @@ let w_coerce_to_type env evd c cty mvty =
     try_to_coerce env evd c cty tycon
 
 let w_coerce env evd mv c =
-  let cty = get_type_of env (evars_of evd) c in
+  let cty = get_type_of_with_meta env (evars_of evd) (metas_of evd) c in
   let mvty = Typing.meta_type evd mv in
   w_coerce_to_type env evd c cty mvty
 
@@ -496,7 +496,7 @@ let unify_to_type env evd flags c u =
 
 let unify_type env evd flags mv c =
   let mvty = Typing.meta_type evd mv in
-  if occur_meta mvty then
+  if occur_meta_or_existential mvty then
     unify_to_type env evd flags c mvty
   else ([],[])
 
@@ -589,7 +589,7 @@ let w_merge env with_types flags (metas,evars) evd =
     let (evd', c) = applyHead sp_env evd nargs hdc in
     let (mc,ec) =
       unify_0 sp_env (evars_of evd') Cumul flags
-        (Retyping.get_type_of sp_env (evars_of evd') c) ev.evar_concl in
+        (Retyping.get_type_of_with_meta sp_env (evars_of evd') (metas_of evd') c) ev.evar_concl in
     let evd'' = w_merge_rec evd' mc ec [] in
     if (evars_of evd') == (evars_of evd'')
     then Evd.evar_define sp c evd''