9 files changed, 73 insertions, 27 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}
 
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index 8337b1c48f..77ce8574f2 100644
--- a/doc/tutorial/Tutorial.tex
+++ b/doc/tutorial/Tutorial.tex
@@ -241,7 +241,7 @@ Variables A B C : Prop.
 \end{coq_example}
 
 We shall consider simple implications, such as $A\ra B$, read as 
-``$A$ implies $B$''. Remark that we overload the arrow symbol, which
+``$A$ implies $B$''. Note that we overload the arrow symbol, which
 has been used above as the functionality type constructor, and which
 may be used as well as propositional connective:
 \begin{coq_example}
@@ -289,7 +289,7 @@ apply H.
 We are now in the situation where we have two judgments as conjectures
 that remain to be proved. Only the first is listed in full, for the
 others the system displays only the corresponding subgoal, without its
-local hypotheses list. Remark that \verb:apply: has kept the local
+local hypotheses list. Note that \verb:apply: has kept the local
 hypotheses of its father judgment, which are still available for
 the judgments it generated.
 
@@ -654,7 +654,7 @@ Hypothesis R_transitive :
     forall x y z : D, R x y -> R y z -> R x z.
 \end{coq_example}
 
-Remark the syntax \verb+forall x : D,+ which stands for universal quantification
+Note the syntax \verb+forall x : D,+ which stands for universal quantification
 $\forall x : D$.
 
 \subsection{Existential quantification}
@@ -664,10 +664,10 @@ We now state our lemma, and enter proof mode.
 Lemma refl_if : forall x : D, (exists y, R x y) -> R x x.
 \end{coq_example}
 
-Remark that the hypotheses which are local to the currently opened sections
+The hypotheses that are local to the currently opened sections
 are listed as local hypotheses to the current goals.
-The rationale is that these hypotheses are going to be discharged, as we
-shall see, when we shall close the corresponding sections.
+That is because these hypotheses are going to be discharged, as
+we shall see, when we shall close the corresponding sections.
 
 Note the functional syntax for existential quantification. The existential
 quantifier is built from the operator \verb:ex:, which expects a 
@@ -687,7 +687,7 @@ verifies \verb:P:. Let us see how this works on this simple example.
 intros x x_Rlinked.
 \end{coq_example}
 
-Remark that \verb:intros: treats universal quantification in the same way
+Note that \verb:intros: treats universal quantification in the same way
 as the premises of implications. Renaming of bound variables occurs
 when it is needed; for instance, had we started with \verb:intro y:,
 we would have obtained the goal:
@@ -859,7 +859,7 @@ Check weird.
 Check drinker.
 \end{coq_example}
 
-Remark how the three theorems are completely generic in the most general 
+Note how the three theorems are completely generic in the most general 
 fashion;
 the domain \verb:D: is discharged in all of them, \verb:R: is discharged in
 \verb:refl_if: only, \verb:P: is discharged only in \verb:weird: and
@@ -867,7 +867,7 @@ the domain \verb:D: is discharged in all of them, \verb:R: is discharged in
 Finally, the excluded middle hypothesis is discharged only in 
 \verb:drinker:.
 
-Note that the name \verb:d: has vanished as well from
+Note, too, that the name \verb:d: has vanished from
 the statements of \verb:weird: and \verb:drinker:, 
 since \Coq's pretty-printer replaces
 systematically a quantification such as \texttt{forall d : D, E},