diff options
| author | Hugo Herbelin | 2015-07-10 01:13:59 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-07-10 19:18:41 +0200 |
| commit | 9c732a5c878bac2592cb397aca3d17cfefdcd023 (patch) | |
| tree | 7defb39c88bdf0d163ca323955d11f1a50d2367d /kernel/typeops.ml | |
| parent | 591e7e484d544e958595a0fb784336ae050a9c74 (diff) | |
Option -type-in-type: added support in checker and making it contaminating
in vo files (this was not done yet in 24d0027f0 and 090fffa57b).
Reused field "engagement" to carry information about both
impredicativity of set and type in type.
For the record: maybe some further checks to do around the sort of the
inductive types in coqchk?
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 48dbacf1a4..fe82d85d5d 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -252,14 +252,12 @@ let sort_of_product env domsort rangsort = | (Prop _, Prop Pos) -> rangsort (* Product rule (Type,Set,?) *) | (Type u1, Prop Pos) -> - begin match engagement env with - | Some ImpredicativeSet -> + if is_impredicative_set env then (* Rule is (Type,Set,Set) in the Set-impredicative calculus *) rangsort - | _ -> + else (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *) Type (Universe.sup Universe.type0 u1) - end (* Product rule (Prop,Type_i,Type_i) *) | (Prop Pos, Type u2) -> Type (Universe.sup Universe.type0 u2) (* Product rule (Prop,Type_i,Type_i) *) |