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