diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-13 14:56:06 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-13 14:56:06 +0000 |
| commit | 6366dec0a76dbaf100907b2d4cd4da84a2ba7fef (patch) | |
| tree | 397f7ce5c437dd3a0b0d537c0d45b4fc7efb97ae | |
| parent | a07e31a2693bde01d3dca59364693096d550561a (diff) | |
Made unification patch 12268 even more ad hoc (if evars remain in a
term, its type is not the smallest one - actually, we would have to
reduce the term too but it would be more costly).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12274 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/evarutil.ml | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index cd2dc5d20..451860477 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1134,14 +1134,16 @@ let solve_refl conv_algo env evd evk argsv1 argsv2 = (* Util *) let check_instance_type conv_algo env evd ev1 t2 = - let typ2 = Retyping.get_type_of env evd (refresh_universes t2) in - let typ1 = existential_type evd ev1 in - match kind_of_term (whd_evar evd typ2) with - | Evar _ -> - (* No firm constraints: don't want to commit to an equal - solution while only subtyping is requested *) - evd - | _ -> + let t2 = nf_evar evd t2 in + if has_undefined_evars_or_sorts evd t2 then + (* May contain larger constraints than needed: don't want to + commit to an equal solution while only subtyping is requested *) + evd + else + let typ2 = Retyping.get_type_of env evd (refresh_universes t2) in + if isEvar typ2 then (* Don't want to commit too early too *) evd + else + let typ1 = existential_type evd ev1 in let evd,b = conv_algo env evd Reduction.CUMUL typ2 typ1 in if b then evd else user_err_loc (fst (evar_source (fst ev1) evd),"", |