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 ++-----
 test-suite/success/cumulativity.v | 9 +++++++++
 2 files changed, 11 insertions(+), 5 deletions(-)

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
diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
index dfa305dc6e..3d97f27b16 100644
--- a/test-suite/success/cumulativity.v
+++ b/test-suite/success/cumulativity.v
@@ -128,3 +128,12 @@ Definition foo2@{i} : bar@{i} := let x := mkfoo in x. (* must reduce *)
 (* Rigid universes however should not be unified unnecessarily. *)
 Definition foo3@{i j|} : foo@{i} := let x := mkfoo@{j} in x.
 Definition foo4@{i j|} : bar@{i} := let x := mkfoo@{j} in x.
+
+(* Constructors for an inductive with indices *)
+Module WithIndex.
+  Inductive foo@{i} : (Prop -> Prop) -> Prop := mkfoo: foo (fun x => x).
+
+  Monomorphic Universes i j.
+  Monomorphic Constraint i < j.
+  Definition bar : eq mkfoo@{i} mkfoo@{j} := eq_refl _.
+End WithIndex.
-- 
cgit v1.2.3