diff options
| author | Hugo Herbelin | 2014-09-13 10:44:40 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-09-13 11:20:28 +0200 |
| commit | 24d0027f0344bca7abce3b8fa8c2a1e42ecf1a00 (patch) | |
| tree | bdde5a56a8e3ca5b0a258ccb68a85caf498fdf56 /pretyping/evd.ml | |
| parent | 9a4e062c92ad88c894ebbd6e20ee9d1511f24a3f (diff) | |
Providing a -type-in-type option for collapsing the universe hierarchy.
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 813a212299..c4bf366ac7 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1193,7 +1193,7 @@ let set_eq_instances ?(flex=false) d u1 u2 = add_universe_constraints d (Universes.enforce_eq_instances_univs flex u1 u2 Universes.Constraints.empty) -let set_leq_sort evd s1 s2 = +let set_leq_sort env evd s1 s2 = let s1 = normalize_sort evd s1 and s2 = normalize_sort evd s2 in match is_eq_sort s1 s2 with @@ -1205,7 +1205,9 @@ let set_leq_sort evd s1 s2 = (* else if Univ.is_type0m_univ u2 then *) (* raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])) *) (* else *) + if not (type_in_type env) then add_universe_constraints evd (Universes.Constraints.singleton (u1,Universes.ULe,u2)) + else evd let check_eq evd s s' = Univ.check_eq evd.universes.uctx_universes s s' |