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

1 files changed, 17 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4816.v b/test-suite/bugs/closed/4816.v
new file mode 100644
index 000000000..86597c88f
--- /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.