Improve documentation of cumulativity

1 files changed, 22 insertions, 1 deletions

diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index 2bb1301c79..79b9e4df52 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -139,7 +139,9 @@ producing global universe constraints, one can use the
 Inductive types, coinductive types, variants and records can be
 declared cumulative using the \texttt{Cumulative}. Alternatively,
 there is an option \texttt{Set Inductive Cumulativity} which when set,
-makes all subsequent inductive definitions cumulative. Consider the examples below.
+makes all subsequent inductive definitions cumulative.  When set
+inductive types and the like can be enforced to be
+\emph{non-cumulative} using the \texttt{NonCumulative} prefix. Consider the examples below.
 \begin{coq_example*}
 Polymorphic Cumulative Inductive list {A : Type} :=
 | nil : list
@@ -176,6 +178,25 @@ Print packType.
 \end{coq_example}
 Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are convertible if and only if \texttt{i $=$ j}.
 
+Cumulative inductive types, coninductive types, variants and records
+only make sense when they are universe polymorphic. Therefore, an
+error is issued whenever the user inputs such monomorphic and
+cumulative type. Notice that this also implies that when the option
+\texttt{Set Inductive Cumulativity} is set any subsequent inductive
+declaration should be polymorphic, e.g., by setting \texttt{Set
+  Universe Polymorphism}, unless it is specifically made
+\emph{non-cumulative} using the \texttt{NonCumulative} prefix.
+
+\begin{coq_example}
+Fail Monomorphic Cumulative Inductive Unit := unit.
+\end{coq_example}
+\begin{coq_example}
+Set Inductive Cumulativity.
+Fail Inductive Unit := unit.
+\end{coq_example}
+\begin{coq_example}
+NonCumulative Inductive Unit := unit.
+\end{coq_example}
 
 \asection{Global and local universes}