From e072a73b3240763d90e720045ca5571f7bc55b18 Mon Sep 17 00:00:00 2001 From: msozeau Date: Mon, 12 Jan 2009 21:52:48 +0000 Subject: 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 --- pretyping/unification.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'pretyping/unification.ml') diff --git a/pretyping/unification.ml b/pretyping/unification.ml index e072af362..6c7ca8af2 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'' -- cgit v1.2.3