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 /pretyping | |
| 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 'pretyping')
| -rw-r--r-- | pretyping/nativenorm.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index b4b6b8aab8..2432b8d291 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -150,14 +150,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 (sup u1 type0_univ) - end (* Product rule (Prop,Type_i,Type_i) *) | (Prop Pos, Type u2) -> Type (sup type0_univ u2) (* Product rule (Prop,Type_i,Type_i) *) |