Update documentation of cumulativity

1 files changed, 20 insertions, 25 deletions

diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index e097de59b3..667fd66984 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -134,12 +134,12 @@ producing global universe constraints, one can use the
 \asection{{\tt Cumulative, NonCumulative}}
 \comindex{Cumulative}
 \comindex{NonCumulative}
-\optindex{Inductive Cumulativity}
+\optindex{Polymorphic Inductive Cumulativity}
 
-Inductive types, coinductive types, variants and records can be
+Polymorphic 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.  When set,
+there is an option \texttt{Set Polymorphic Inductive Cumulativity} which when set,
+makes all subsequent \emph{polymorphic} 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*}
@@ -160,15 +160,6 @@ This also means that any two instances of \texttt{list} are convertible:
 $\WTEGCONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ whenever $\WTEGCONV{A}{B}$ and
 furthermore their corresponding (when fully applied to convertible arguments) constructors.
 See Chapter~\ref{Cic} for more details on convertibility and subtyping.
-Also notice the subtyping constraints for the \emph{non-cumulative} version of list:
-\begin{coq_example*}
-Polymorphic NonCumulative Inductive list' {A : Type} :=
-| nil' : list'
-| cons' : A -> list' -> list'.
-\end{coq_example*}
-\begin{coq_example}
-Print list'.
-\end{coq_example}
 The following is an example of a record with non-trivial subtyping relation:
 \begin{coq_example*}
 Polymorphic Cumulative Record packType := {pk : Type}.
@@ -176,33 +167,37 @@ Polymorphic Cumulative Record packType := {pk : Type}.
 \begin{coq_example}
 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}.
+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 a 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.
-
+error is issued whenever the user uses the \texttt{Cumulative} or
+\texttt{NonCumulative} prefix in a monomorphic contexts.
+Notice that this is not the case for the option \texttt{Set Polymorphic Inductive Cumulativity}.
+That is, this optiotion, when set, makes all subsequent \emph{polymorphic}
+inductive declarations cumulative (unless, of course if the \texttt{NonCumulative} prefix is used)
+but has no effect on \emph{monomorphic} inductive declarations.
+Consider the following examples.
 \begin{coq_example}
 Fail Monomorphic Cumulative Inductive Unit := unit.
 \end{coq_example}
 \begin{coq_example}
-Set Inductive Cumulativity.
-Fail Inductive Unit := unit.
+Fail Monomorphic NonCumulative Inductive Unit := unit.
 \end{coq_example}
+\begin{coq_example*}
+Set Polymorphic Inductive Cumulativity.
+Inductive Unit := unit.
+\end{coq_example*}
 \begin{coq_example}
-NonCumulative Inductive Unit := unit.
+Print Unit.
 \end{coq_example}
 
 \subsection*{An example of a proof using cumulativity}
 
 \begin{coq_example}
 Set Universe Polymorphism.
-Set Inductive Cumulativity.
+Set Polymorphic Inductive Cumulativity.
 
 Inductive eq@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := eq_refl : eq x x.