From ee573583701c8e53e8b82978998a9df93170cd79 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 8 Mar 2018 15:11:34 +0100
Subject: Fix expected number of arguments for cumulative constructors.

We expected `nparams + nrealargs + consnrealargs` but the `nrealargs`
should not be there. This breaks cumulativity of constructors for any
inductive with indices (so records still work, explaining why the test
case in #6747 works).
---
 kernel/reduction.ml | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'kernel')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 4ecbec0edd..81fbd4f5ef 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -251,11 +251,8 @@ let convert_inductives cv_pb ind nargs u1 u2 (s, check) =
     cv_pb ind nargs u1 u2 s, check
 
 let constructor_cumulativity_arguments (mind, ind, ctor) =
-  let nparamsctxt =
-    mind.Declarations.mind_nparams +
-    mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
-    (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in
-  nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(ctor - 1)
+  mind.Declarations.mind_nparams +
+  mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(ctor - 1)
 
 let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u2 s =
   match mind.Declarations.mind_universes with
-- 
cgit v1.2.3