Merge PR #7746: Many small cleanups removing unused arguments and functions

1 files changed, 2 insertions, 13 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 61b71df31..5d45c2c1a 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -120,16 +120,6 @@ let mind_check_names mie =
 
 (* Typing the arities and constructor types *)
 
-(* An inductive definition is a "unit" if it has only one constructor
-   and that all arguments expected by this constructor are
-   logical, this is the case for equality, conjunction of logical properties
-*)
-let is_unit constrsinfos =
-  match constrsinfos with  (* One info = One constructor *)
-   | [level] -> is_type0m_univ level
-   | [] -> (* type without constructors *) true
-   | _ -> false
-
 let infos_and_sort env t =
   let rec aux env t max =
     let t = whd_all env t in
@@ -174,10 +164,9 @@ let infer_constructor_packet env_ar_par params lc =
   let lc'' = Array.map (fun j -> Term.it_mkProd_or_LetIn j.utj_val params) jlc in
   (* compute the max of the sorts of the products of the constructors types *)
   let levels = List.map (infos_and_sort env_ar_par) lc in
-  let isunit = is_unit levels in
   let min = if Array.length jlc > 1 then Universe.type0 else Universe.type0m in
   let level = List.fold_left (fun max l -> Universe.sup max l) min levels in
-  (lc'', (isunit, level))
+  (lc'', level)
 
 (* If indices matter *)
 let cumulate_arity_large_levels env sign =
@@ -354,7 +343,7 @@ let typecheck_inductive env mie =
   (* Compute/check the sorts of the inductive types *)
 
   let inds =
-    Array.map (fun ((id,full_arity,sign,expltype,def_level,inf_level),cn,lc,(is_unit,clev))  ->
+    Array.map (fun ((id,full_arity,sign,expltype,def_level,inf_level),cn,lc,clev)  ->
       let infu = 
 	(** Inferred level, with parameters and constructors. *)
 	match inf_level with