diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index d14a212de0..66cd4cba9e 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -226,7 +226,10 @@ let type_of_inductive_knowing_parameters env ?(polyprop=true) mip args = (* The max of an array of universes *) let cumulate_constructor_univ u = let open Sorts in function - | Prop -> u + | SProp | Prop -> + (* SProp is non cumulative but allowed in constructors of any + inductive (except non-sprop primitive records) *) + u | Set -> Universe.sup Universe.type0 u | Type u' -> Universe.sup u u' @@ -301,11 +304,7 @@ let build_dependent_inductive ind (_,mip) params = exception LocalArity of (Sorts.family * Sorts.family * arity_error) option let check_allowed_sort ksort specif = - let open Sorts in - let eq_ksort s = match ksort, s with - | InProp, InProp | InSet, InSet | InType, InType -> true - | _ -> false in - if not (CList.exists eq_ksort (elim_sorts specif)) then + if not (CList.exists (Sorts.family_equal ksort) (elim_sorts specif)) then let s = inductive_sort_family (snd specif) in raise (LocalArity (Some(ksort,s,error_elim_explain ksort s))) |