diff options
| author | Gaëtan Gilbert | 2017-10-12 13:55:08 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-14 13:27:38 +0100 |
| commit | a0e16c9e5c3f88a8b72935dd4877f13388640f69 (patch) | |
| tree | b177cc86b2742893adf0b181e53c03b8897b48cc /kernel/typeops.ml | |
| parent | 6c447d7a7190857b03bb2992f443f1b818618a94 (diff) | |
Make Sorts.t private
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 227a164549..6d12ce3020 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -275,13 +275,13 @@ let sort_of_product env domsort rangsort = rangsort else (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *) - Type (Universe.sup Universe.type0 u1) + Sorts.sort_of_univ (Universe.sup Universe.type0 u1) (* Product rule (Prop,Type_i,Type_i) *) - | (Set, Type u2) -> Type (Universe.sup Universe.type0 u2) + | (Set, Type u2) -> Sorts.sort_of_univ (Universe.sup Universe.type0 u2) (* Product rule (Prop,Type_i,Type_i) *) | (Prop, Type _) -> rangsort (* Product rule (Type_i,Type_i,Type_i) *) - | (Type u1, Type u2) -> Type (Universe.sup u1 u2) + | (Type u1, Type u2) -> Sorts.sort_of_univ (Universe.sup u1 u2) (* [judge_of_product env name (typ1,s1) (typ2,s2)] implements the rule |