diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 2059a1a40..3b64a2c09 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -124,7 +124,7 @@ Remark: Set (predicative) is encoded as Type(0) let sort_as_univ = function | Type u -> u -| Prop Null -> lower_univ +| Prop Null -> type0m_univ | Prop Pos -> type0_univ let cons_subst u su subst = @@ -179,10 +179,12 @@ let instantiate_universes env ctx ar argsorts = let ctx,subst = make_subst env (ctx,ar.poly_param_levels,args) in let level = subst_large_constraints subst ar.poly_level in ctx, - if is_type0_univ level then set_sort else Type level - (* Note: for singleton types, we keep a representative in Type so that - predicativity and subtyping in Set applies, even if the resulting type - is semantically equivalent to Prop (and indeed convertible to it) *) + (* Singleton type not containing types are interpretable in Prop *) + if is_type0m_univ level then prop_sort + (* Non singleton type not containing types are interpretable in Set *) + else if is_type0_univ level then set_sort + (* This is a Type with constraints *) + else Type level let type_of_inductive_knowing_parameters env mip paramtyps = match mip.mind_arity with @@ -206,7 +208,7 @@ let cumulate_constructor_univ u = function | Type u' -> sup u u' let max_inductive_sort = - Array.fold_left cumulate_constructor_univ lower_univ + Array.fold_left cumulate_constructor_univ type0m_univ (************************************************************************) (* Type of a constructor *) |