Updated version 8.9.0 from 'upstream/8.9.0'

with Debian dir 81a4f85bc45e59aa1eadb4797f0eb0b8039efb63

1 files changed, 19 insertions, 0 deletions

diff --git a/test-suite/coqchk/bug_8876.v b/test-suite/coqchk/bug_8876.v
new file mode 100644
index 00000000..2d20511a
--- /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.