Merge PR #11367: Minor cleanup of indtypes/indtyping

Reviewed-by: ppedrot

2 files changed, 14 insertions, 17 deletions

diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index d9ccf81619..b19472dc99 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -197,16 +197,14 @@ let unbounded_from_below u cstrs =
    is u_k and is contributing. *)
 let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt concl =
   let check_level l =
-    if Univ.LSet.mem l (Univ.ContextSet.levels uctx) &&
-       unbounded_from_below l (Univ.ContextSet.constraints uctx) &&
-       not (Univ.LSet.mem l ctor_levels) then
-      Some l
-    else None
+    Univ.LSet.mem l (Univ.ContextSet.levels uctx) &&
+    unbounded_from_below l (Univ.ContextSet.constraints uctx) &&
+    not (Univ.LSet.mem l ctor_levels)
   in
   let univs = Univ.Universe.levels concl in
   let univs =
     if template_check then
-      Univ.LSet.filter (fun l -> Option.has_some (check_level l) || Univ.Level.is_prop l) univs
+      Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs
     else univs (* Doesn't check the universes can be generalized *)
   in
   let fold acc = function
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index ab915e2b8d..0d900c2ec9 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -487,18 +487,17 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite
     in
     (* Assigning VM tags to constructors *)
     let nconst, nblock = ref 0, ref 0 in
-    let transf num =
-      let arity = List.length (dest_subterms recarg).(num) in
-        if Int.equal arity 0 then
-          let p  = (!nconst, 0) in
-            incr nconst; p
-        else
-          let p = (!nblock + 1, arity) in
-            incr nblock; p
-              (* les tag des constructeur constant commence a 0,
-                 les tag des constructeur non constant a 1 (0 => accumulator) *)
+    let transf arity =
+      if Int.equal arity 0 then
+        let p  = (!nconst, 0) in
+        incr nconst; p
+      else
+        let p = (!nblock + 1, arity) in
+        incr nblock; p
+        (* les tag des constructeur constant commence a 0,
+           les tag des constructeur non constant a 1 (0 => accumulator) *)
     in
-    let rtbl = Array.init (List.length cnames) transf in
+    let rtbl = Array.map transf consnrealargs in
       (* Build the inductive packet *)
       { mind_typename = id;
         mind_arity = arity;