From fbe0b2645eab84012aec50e76d94e15a3fefe664 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Fri, 7 Jul 2017 14:09:31 +0200
Subject: Issue error on monomorphic cumulative inductives

---
 test-suite/success/cumulativity.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
index ebf817cfc5..604da2108e 100644
--- a/test-suite/success/cumulativity.v
+++ b/test-suite/success/cumulativity.v
@@ -1,3 +1,9 @@
+Polymorphic Cumulative Inductive T1 := t1 : T1.
+Fail Monomorphic Cumulative Inductive T2 := t2 : T2.
+
+Polymorphic Cumulative Record R1 := { r1 : T1 }.
+Fail Monomorphic Cumulative Inductive R2 := {r2 : T1}.
+
 Set Universe Polymorphism.
 Set Inductive Cumulativity.
 Set Printing Universes.
-- 
cgit v1.2.3