Move cumulativity inference to the kernel.

This is not quite pretty, but it is needed by the section mechanism to rebuild
an inductive when closing a section. Hopefully this can be moved back at some
point.

4 files changed, 6 insertions, 7 deletions

diff --git a/pretyping/inferCumulativity.ml b/kernel/inferCumulativity.ml
index ed069eace0..8b5b254f45 100644
--- a/pretyping/inferCumulativity.ml
+++ b/kernel/inferCumulativity.ml
@@ -77,7 +77,7 @@ let infer_sort cv_pb variances s =
   | CUMUL ->
     LSet.fold infer_level_leq (Universe.levels (Sorts.univ_of_sort s)) variances
 
-let infer_table_key infos variances c =
+let infer_table_key _infos variances c =
   let open Names in
   match c with
   | ConstKey (_, u) ->
@@ -152,7 +152,7 @@ and infer_stack infos variances (stk:CClosure.stack) =
       | Zfix (fx,a) ->
         let variances = infer_fterm CONV infos variances fx [] in
         infer_stack infos variances a
-      | ZcaseT (ci,p,br,e) ->
+      | ZcaseT (_, p, br, e) ->
         let variances = infer_fterm CONV infos variances (mk_clos e p) [] in
         infer_vect infos variances (Array.map (mk_clos e) br)
       | Zshift _ -> variances
@@ -195,7 +195,7 @@ let infer_inductive_core env params entries uctx =
     Array.fold_left (fun variances u -> LMap.add u IrrelevantI variances)
       LMap.empty uarray
   in
-  let env, params = Typeops.check_context env params in
+  let env, _ = Typeops.check_context env params in
   let variances = List.fold_left (fun variances entry ->
       let variances = infer_arity_constructor true
           env variances entry.mind_entry_arity
@@ -213,9 +213,8 @@ let infer_inductive_core env params entries uctx =
 
 let infer_inductive env mie =
   let open Entries in
-  let { mind_entry_params = params;
-        mind_entry_inds = entries; } = mie
-  in
+  let params = mie.mind_entry_params in
+  let entries = mie.mind_entry_inds in
   let variances =
     match mie.mind_entry_variance with
     | None -> None
diff --git a/pretyping/inferCumulativity.mli b/kernel/inferCumulativity.mli
index a234e334d1..a234e334d1 100644
--- a/pretyping/inferCumulativity.mli
+++ b/kernel/inferCumulativity.mli
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 59c1d5890f..66bac15e9a 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -43,6 +43,7 @@ Inductive
 Typeops
 IndTyping
 Indtypes
+InferCumulativity
 Cooking
 Term_typing
 Subtyping
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 0ca39f0404..7e140f4399 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -4,7 +4,6 @@ Locusops
 Pretype_errors
 Reductionops
 Inductiveops
-InferCumulativity
 Arguments_renaming
 Retyping
 Vnorm