8 files changed, 64 insertions, 18 deletions
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index 8cb049d50e..499239b6f3 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -381,6 +381,9 @@ some specific {\tt Extract Constant} when primitive counterparts exist.
 
 \Example
 Typical examples are the following:
+\begin{coq_eval}
+Require Extraction.
+\end{coq_eval}
 \begin{coq_example}
 Extract Inductive unit => "unit" [ "()" ].
 Extract Inductive bool => "bool" [ "true" "false" ].
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 96fb1eb752..7a71d69086 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1425,6 +1425,9 @@ If there is an hypothesis $h:a=b$ in the local context, it can be used for
 rewriting not only in logical propositions but also in any type.
 % In that case, the term \verb!eq_rec! which was defined as an axiom, is
 % now a term of the calculus.
+\begin{coq_eval}
+Require Extraction.
+\end{coq_eval}
 \begin{coq_example}
 Print eq_rec.
 Extraction eq_rec.
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 71977d3e9d..ef12fe416a 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -37,7 +37,7 @@ Similarly, the notation ``\nelist{\entry}{}'' stands for a non
 empty sequence of expressions parsed by the ``{\entry}'' entry,
 without any separator between.
 
-At the end, the notation ``\sequence{\entry}{\tt sep}'' stands for a
+Finally, the notation ``\sequence{\entry}{\tt sep}'' stands for a
 possibly empty sequence of expressions parsed by the ``{\entry}'' entry,
 separated by the literal ``{\tt sep}''.
 
diff --git a/doc/refman/RefMan-int.tex b/doc/refman/RefMan-int.tex
index eca3efcdd6..2b9e4e6051 100644
--- a/doc/refman/RefMan-int.tex
+++ b/doc/refman/RefMan-int.tex
@@ -58,7 +58,7 @@ Chapter~\ref{Addoc-coqide}.
 
 \section*{How to read this book}
 
-This is a Reference Manual, not a User Manual, then it is not made for a
+This is a Reference Manual, not a User Manual, so it is not made for a
 continuous reading. However, it has some structure that is explained
 below.
 
diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex
index d3719bed46..23a1c9b029 100644
--- a/doc/refman/RefMan-sch.tex
+++ b/doc/refman/RefMan-sch.tex
@@ -227,6 +227,7 @@ We define the function \texttt{div2} as follows:
 
 \begin{coq_eval}
 Reset Initial.
+Require Import FunInd.
 \end{coq_eval}
 
 \begin{coq_example*}
diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex
index 9f4ddc8044..cb8f916f13 100644
--- a/doc/refman/RefMan-tacex.tex
+++ b/doc/refman/RefMan-tacex.tex
@@ -849,7 +849,7 @@ Ltac DSimplif trm :=
 Ltac Length trm :=
   match trm with
   | (_ * ?B) => let succ := Length B in constr:(S succ)
-  | _ => constr:1
+  | _ => constr:(1)
   end.
 Ltac assoc := repeat rewrite <- Ass.
 \end{coq_example}
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index 2c9602a229..6c79284389 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -156,9 +156,9 @@ compatibility constraints.
 \begin{cscexample}[Rewriting]
 Continuing the previous examples, suppose that the user must prove
 \texttt{set\_eq int (union int (union int S1 S2) S2) (f S1 S2)} under the
-hypothesis \texttt{H: set\_eq int S2 (nil int)}. It is possible to
+hypothesis \texttt{H: set\_eq int S2 (@nil int)}. It is possible to
 use the \texttt{rewrite} tactic to replace the first two occurrences of
-\texttt{S2} with \texttt{nil int} in the goal since the context
+\texttt{S2} with \texttt{@nil int} in the goal since the context
 \texttt{set\_eq int (union int (union int S1 nil) nil) (f S1 S2)}, being
 a composition of morphisms instances, is a morphism. However the tactic
 will fail replacing the third occurrence of \texttt{S2} unless \texttt{f}
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index 2bb1301c79..cd36d1d320 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -134,12 +134,14 @@ 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. Consider the examples below.
+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*}
 Polymorphic Cumulative Inductive list {A : Type} :=
 | nil : list
@@ -158,24 +160,61 @@ 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:
+The following is an example of a record with non-trivial subtyping relation:
 \begin{coq_example*}
-Polymorphic NonCumulative Inductive list' {A : Type} :=
-| nil' : list'
-| cons' : A -> list' -> list'.
+Polymorphic Cumulative Record packType := {pk : Type}.
 \end{coq_example*}
 \begin{coq_example}
-Print list'.
+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 uses the \texttt{Cumulative} or
+\texttt{NonCumulative} prefix in a monomorphic context.
+Notice that this is not the case for the option \texttt{Set Polymorphic Inductive Cumulativity}.
+That is, this option, when set, makes all subsequent \emph{polymorphic}
+inductive declarations cumulative (unless, of course the \texttt{NonCumulative} prefix is used)
+but has no effect on \emph{monomorphic} inductive declarations.
+Consider the following examples.
+\begin{coq_example}
+Monomorphic Cumulative Inductive Unit := unit.
+\end{coq_example}
+\begin{coq_example}
+Monomorphic NonCumulative Inductive Unit := unit.
 \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}.
+Set Polymorphic Inductive Cumulativity.
+Inductive Unit := unit.
 \end{coq_example*}
 \begin{coq_example}
-Print packType.
+Print Unit.
 \end{coq_example}
-Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are convertible if and only if \texttt{i $=$ j}.
 
+\subsection*{An example of a proof using cumulativity}
+
+\begin{coq_example}
+Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
+
+Inductive eq@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := eq_refl : eq x x.
+
+Definition funext_type@{a b e} (A : Type@{a}) (B : A -> Type@{b})
+  := forall f g : (forall a, B a),
+    (forall x, eq@{e} (f x) (g x))
+    -> eq@{e} f g.
+
+Section down.
+  Universes a b e e'.
+  Constraint e' < e.
+  Lemma funext_down {A B}
+    (H : @funext_type@{a b e} A B) : @funext_type@{a b e'} A B.
+  Proof.
+    exact H.
+  Defined.
+\end{coq_example}
 
 \asection{Global and local universes}