From be8db31abc6839921e91540ab4b3300da9b64933 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 10 May 2019 11:49:50 +0200
Subject: mind_kelim is the highest allowed sort instead of a list

---
 vernac/auto_ind_decl.ml |  4 ++--
 vernac/himsg.ml         |  1 +
 vernac/indschemes.ml    | 11 ++++++-----
 3 files changed, 9 insertions(+), 7 deletions(-)

(limited to 'vernac')

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 528829f3a5..5aec5cac2c 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -331,8 +331,8 @@ let build_beq_scheme mode kn =
         eff := Safe_typing.concat_private eff' !eff
     done;
       (Array.init nb_ind (fun i ->
-      let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in
-	if not (Sorts.List.mem InSet kelim) then
+      let kelim = Inductive.elim_sort (mib,mib.mind_packets.(i)) in
+        if not (Sorts.family_leq InSet kelim) then
 	  raise (NonSingletonProp (kn,i));
         let fix = match mib.mind_finite with
         | CoFinite ->
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index b2382ce6fc..a1f7835cbe 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -219,6 +219,7 @@ let explain_elim_arity env sigma ind c pj okinds =
   let pc = pr_leconstr_env env sigma c in
   let msg = match okinds with
   | Some(sorts,kp,ki,explanation) ->
+      let sorts = Inductiveops.sorts_below sorts in
       let pki = Sorts.pr_sort_family ki in
       let pkp = Sorts.pr_sort_family kp in
       let explanation =	match explanation with
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 6ac259b1fe..de7d2fd49a 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -216,11 +216,11 @@ let declare_one_case_analysis_scheme ind =
     else if not (Inductiveops.has_dependent_elim mib) then
       case_scheme_kind_from_type
     else case_dep_scheme_kind_from_type in
-  let kelim = elim_sorts (mib,mip) in
+  let kelim = elim_sort (mib,mip) in
     (* in case the inductive has a type elimination, generates only one
        induction scheme, the other ones share the same code with the
        appropriate type *)
-  if Sorts.List.mem InType kelim then
+  if Sorts.family_leq InType kelim then
     ignore (define_individual_scheme dep UserAutomaticRequest None ind)
 
 (* Induction/recursion schemes *)
@@ -248,16 +248,17 @@ let declare_one_induction_scheme ind =
   let kind = inductive_sort_family mip in
   let from_prop = kind == InProp in
   let depelim = Inductiveops.has_dependent_elim mib in
-  let kelim = elim_sorts (mib,mip) in
+  let kelim = Inductiveops.sorts_below (elim_sort (mib,mip)) in
   let kelim = if Global.sprop_allowed () then kelim
     else List.filter (fun s -> s <> InSProp) kelim
   in
   let elims =
     List.map_filter (fun (sort,kind) ->
-      if Sorts.List.mem sort kelim then Some kind else None)
+        if List.mem_f Sorts.family_equal sort kelim then Some kind else None)
       (if from_prop then kinds_from_prop
        else if depelim then kinds_from_type
-       else nondep_kinds_from_type) in
+       else nondep_kinds_from_type)
+  in
   List.iter (fun kind -> ignore (define_individual_scheme kind UserAutomaticRequest None ind))
     elims
 
-- 
cgit v1.2.3