diff options
| author | msozeau | 2011-04-16 10:32:16 +0000 |
|---|---|---|
| committer | msozeau | 2011-04-16 10:32:16 +0000 |
| commit | 0f78158fe1993b0e680d27b581bcaaad8fc009f7 (patch) | |
| tree | e1c63fcc80b2e49347129fb9077358040ef78bbe | |
| parent | e2257ae597fd213463dcc7d56e1eb6e6663c0ad3 (diff) | |
Fix unification of types of metavariables and error message for sort unification.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14020 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/unification.ml | 11 |
1 files changed, 2 insertions, 9 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 828825aa00..7d5d68fbb1 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -268,7 +268,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag then Evd.set_leq_sort sigma s1 s2 else Evd.set_eq_sort sigma s1 s2 in (sigma', metasubst, evarsubst) - with _ -> error_cannot_unify_local curenv sigma (m,n,cM)) + with _ -> error_cannot_unify curenv sigma (m,n)) | Lambda (na,t1,c1), Lambda (_,t2,c2) -> unirec_rec (push (na,t1) curenvnb) topconv true @@ -643,14 +643,7 @@ let unify_to_type env sigma flags c status u = let t = get_type_of env sigma c in let t = Tacred.hnf_constr env sigma (nf_betaiota sigma (nf_meta sigma t)) in let u = Tacred.hnf_constr env sigma u in - if status = IsSuperType then - unify_0 env sigma Cumul flags u t - else if status = IsSubType then - unify_0 env sigma Cumul flags t u - else - try unify_0 env sigma Cumul flags t u - with e when precatchable_exception e -> - unify_0 env sigma Cumul flags u t + unify_0 env sigma Cumul flags t u let unify_type env sigma flags mv status c = let mvty = Typing.meta_type sigma mv in |