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
---
 doc/refman/Universes.tex | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index a08cd1475a..36518e6fae 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -201,7 +201,8 @@ universes and explicitly instantiate polymorphic definitions.
 In the monorphic case, this command declares a new global universe named
 {\ident}. It supports the polymorphic flag only in sections, meaning the
 universe quantification will be discharged on each section definition
-independently.
+independently. One cannot mix polymorphic and monomorphic declarations
+in the same section.
 
 \subsection{\tt Constraint {\ident} {\textit{ord}} {\ident}.
   \comindex{Constraint}
@@ -212,6 +213,7 @@ The order relation can be one of $<$, $\le$ or $=$. If consistent,
 the constraint is then enforced in the global environment. Like
 \texttt{Universe}, it can be used with the \texttt{Polymorphic} prefix
 in sections only to declare constraints discharged at section closing time.
+One cannot declare a global constraint on polymorphic universes.
 
 \begin{ErrMsgs}
 \item \errindex{Undeclared universe {\ident}}.
-- 
cgit v1.2.3