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).
---
 test-suite/success/cumulativity.v | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'test-suite')

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