mind_kelim is the highest allowed sort instead of a list

5 files changed, 17 insertions, 12 deletions

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 7615a17514..1c488a6974 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -84,7 +84,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
 
   let () = if Option.is_empty projs then check_privacy_block mib in
   let () = 
-    if not (Sorts.List.mem kind (elim_sorts specif)) then
+    if not (Sorts.family_leq kind (elim_sort specif)) then
       raise
 	(RecursionSchemeError
            (env, NotAllowedCaseAnalysis (false, fst (UnivGen.fresh_sort_in_family kind), pind)))
@@ -557,8 +557,8 @@ let weaken_sort_scheme env evd set sort npars term ty =
 let check_arities env listdepkind =
   let _ = List.fold_left
     (fun ln (((_,ni as mind),u),mibi,mipi,dep,kind) ->
-       let kelim = elim_sorts (mibi,mipi) in
-       if not (Sorts.List.mem kind kelim) then raise
+       let kelim = elim_sort (mibi,mipi) in
+       if not (Sorts.family_leq kind kelim) then raise
 	 (RecursionSchemeError
           (env, NotAllowedCaseAnalysis (true, fst (UnivGen.fresh_sort_in_family kind),(mind,u))))
        else if Int.List.mem ni ln then raise
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index b1c98da2c7..12a7859b88 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -255,10 +255,13 @@ let inductive_has_local_defs env ind =
   let l2 = mib.mind_nparams + mip.mind_nrealargs in
   not (Int.equal l1 l2)
 
-let allowed_sorts env (kn,i as ind) =
+let top_allowed_sort env (kn,i as ind) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   mip.mind_kelim
 
+let sorts_below top =
+  List.filter (fun s -> Sorts.family_leq s top) Sorts.[InSProp;InProp;InSet;InType]
+
 let has_dependent_elim mib =
   match mib.mind_record with
   | PrimRecord _ -> mib.mind_finite == BiFinite
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index cfc650938e..aacbecf6c7 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -141,7 +141,9 @@ val constructor_nrealdecls_env : env -> constructor -> int
 val constructor_has_local_defs : env -> constructor -> bool
 val inductive_has_local_defs : env -> inductive -> bool
 
-val allowed_sorts : env -> inductive -> Sorts.family list
+val sorts_below : Sorts.family -> Sorts.family list
+
+val top_allowed_sort : env -> inductive -> Sorts.family
 
 (** (Co)Inductive records with primitive projections do not have eta-conversion,
     hence no dependent elimination. *)
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index a9e2b0ea8f..25e56602a5 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -107,7 +107,7 @@ val error_ill_typed_rec_body :
 val error_elim_arity :
   ?loc:Loc.t -> env -> Evd.evar_map ->
       pinductive -> constr ->
-      unsafe_judgment -> (Sorts.family list * Sorts.family * Sorts.family * arity_error) option -> 'b
+      unsafe_judgment -> (Sorts.family * Sorts.family * Sorts.family * arity_error) option -> 'b
 
 val error_not_a_type :
   ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index be71f44a5e..00c52e7665 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -117,12 +117,12 @@ let check_branch_types env sigma (ind,u) cj (lfj,explft) =
     sigma lfj explft
 
 let max_sort l =
-  if Sorts.List.mem InType l then InType else
-  if Sorts.List.mem InSet l then InSet else InProp
+  if List.mem_f Sorts.family_equal InType l then InType else
+  if List.mem_f Sorts.family_equal InSet l then InSet else InProp
 
 let is_correct_arity env sigma c pj ind specif params =
   let arsign = make_arity_signature env sigma true (make_ind_family (ind,params)) in
-  let allowed_sorts = elim_sorts specif in
+  let allowed_sorts = sorts_below (elim_sort specif) in
   let error () = Pretype_errors.error_elim_arity env sigma ind c pj None in
   let rec srec env sigma pt ar =
     let pt' = whd_all env sigma pt in
@@ -135,7 +135,7 @@ let is_correct_arity env sigma c pj ind specif params =
       end
     | Sort s, [] ->
         let s = ESorts.kind sigma s in
-        if not (Sorts.List.mem (Sorts.family s) allowed_sorts)
+        if not (List.mem_f Sorts.family_equal (Sorts.family s) allowed_sorts)
         then error ()
         else sigma, s
     | Evar (ev,_), [] ->
@@ -199,13 +199,13 @@ let check_type_fixpoint ?loc env sigma lna lar vdefj =
 (* FIXME: might depend on the level of actual parameters!*)
 let check_allowed_sort env sigma ind c p =
   let specif = lookup_mind_specif env (fst ind) in
-  let sorts = elim_sorts specif in
+  let sorts = elim_sort specif in
   let pj = Retyping.get_judgment_of env sigma p in
   let _, s = splay_prod env sigma pj.uj_type in
   let ksort = match EConstr.kind sigma s with
   | Sort s -> Sorts.family (ESorts.kind sigma s)
   | _ -> error_elim_arity env sigma ind c pj None in
-  if not (List.exists ((==) ksort) sorts) then
+  if not (Sorts.family_leq ksort sorts) then
     let s = inductive_sort_family (snd specif) in
     error_elim_arity env sigma ind c pj
       (Some(sorts,ksort,s,Type_errors.error_elim_explain ksort s))