From 1220aab80893b68c14adb64ba0b75811961ac04d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 30 Dec 2019 13:03:31 +0100
Subject: minor cleanup template_polymorphic_univs: check_levels returns bool

---
 kernel/indTyping.ml | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3


From e1da46b1141e1fc9ce04f2285fbb50fe3aab18b7 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 30 Dec 2019 16:57:27 +0100
Subject: cleanup: do not use recargs when computing the reloc table for ctors

This doesn't actually have anything to do with positivity AFAICT, we
just want the number of non-parameter arguments.
---
 kernel/indtypes.ml | 21 ++++++++++-----------
 1 file changed, 10 insertions(+), 11 deletions(-)

(limited to 'kernel')

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;
-- 
cgit v1.2.3