From 03a71a241f8d05f6a86f3c8f3c2146c4db378f7b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 13 Jun 2016 18:42:01 +0200
Subject: Univs: more robust Universe/Constraint decls #4816

This fixes the declarations of constraints, universes
and assumptions:
- global constraints can refer to global universes only,
- polymorphic universes, constraints and assumptions can only be
  declared inside sections, when all the section's
  variables/universes are polymorphic as well.
- monomorphic assumptions may only be declared in section contexts
  which are not parameterized by polymorphic universes/assumptions.

Add fix for part 1 of bug #4816
---
 test-suite/bugs/closed/4816.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 test-suite/bugs/closed/4816.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4816.v b/test-suite/bugs/closed/4816.v
new file mode 100644
index 0000000000..86597c88fa
--- /dev/null
+++ b/test-suite/bugs/closed/4816.v
@@ -0,0 +1,17 @@
+Section foo.
+Polymorphic Universes A B.
+Fail Constraint A <= B.
+End foo.
+(* gives an anomaly Universe undefined *)
+
+Universes X Y.
+Section Foo.
+  Polymorphic Universes Z W.
+  Polymorphic Constraint W < Z.
+
+  Fail Definition bla := Type@{W}.
+  Polymorphic Definition bla := Type@{W}.
+  Section Bar.
+    Fail Constraint X <= Z.
+  End Bar.
+End Foo.
-- 
cgit v1.2.3