From 9615c025a2a09b69f2001d44a66a1fddef74e680 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 29 Sep 2016 15:51:18 +0200
Subject: Fix bug #4869, allow Prop, Set, and level names in constraints.

---
 test-suite/bugs/closed/4869.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 test-suite/bugs/closed/4869.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4869.v b/test-suite/bugs/closed/4869.v
new file mode 100644
index 0000000000..6d21b66fe9
--- /dev/null
+++ b/test-suite/bugs/closed/4869.v
@@ -0,0 +1,18 @@
+Universes i.
+
+Fail Constraint i < Set.
+Fail Constraint i <= Set.
+Fail Constraint i = Set.
+Constraint Set <= i.
+Constraint Set < i.
+Fail Constraint i < j. (* undeclared j *)
+Fail Constraint i < Type. (* anonymous *)
+
+Set Universe Polymorphism.
+
+Section Foo.
+  Universe j.
+  Constraint Set < j.
+
+  Definition foo := Type@{j}.
+End Foo.
\ No newline at end of file
-- 
cgit v1.2.3