From baa8812294d48bf9d0e6e62a39440e9ffb2b93e2 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 31 Oct 2018 14:00:38 +0100
Subject: Fix #8876: expected number of arguments for cumulative constructors

ee573583701c8e53e8b82978998a9df93170cd79 ported to the checker.
---
 checker/reduction.ml         |  5 +----
 test-suite/coqchk/bug_8876.v | 19 +++++++++++++++++++
 2 files changed, 20 insertions(+), 4 deletions(-)
 create mode 100644 test-suite/coqchk/bug_8876.v

diff --git a/checker/reduction.ml b/checker/reduction.ml
index 58a3f4e410..1158152f63 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -192,10 +192,7 @@ let convert_constructors
   | Monomorphic_ind _ | Polymorphic_ind _ -> convert_universes univs u1 u2
   | Cumulative_ind cumi ->
     let num_cnstr_args =
-      let nparamsctxt =
-        mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs
-      in
-      nparamsctxt + mind.mind_packets.(ind).mind_consnrealargs.(cns - 1)
+      mind.mind_nparams + mind.mind_packets.(ind).mind_consnrealargs.(cns - 1)
     in
     if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
       convert_universes univs u1 u2
diff --git a/test-suite/coqchk/bug_8876.v b/test-suite/coqchk/bug_8876.v
new file mode 100644
index 0000000000..2d20511a04
--- /dev/null
+++ b/test-suite/coqchk/bug_8876.v
@@ -0,0 +1,19 @@
+(* -*- coq-prog-args: ("-noinit"); -*- *)
+Require Import Coq.Init.Notations.
+
+Notation "x -> y" := (forall _ : x, y).
+
+Inductive eq {A:Type} (a:A) : A -> Prop := eq_refl : eq a a.
+
+Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
+Set Printing Universes.
+
+(* 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