9 files changed, 97 insertions, 39 deletions
diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex
index b93ca29577..1609e4a041 100644
--- a/doc/refman/AsyncProofs.tex
+++ b/doc/refman/AsyncProofs.tex
@@ -51,6 +51,12 @@ proof does not begin with \texttt{Proof using}, the system records in an
 auxiliary file, produced along with the \texttt{.vo} file, the list of
 section variables used.
 
+\subsubsection{Automatic suggestion of proof annotations}
+
+The command \texttt{Set Suggest Proof Using} makes Coq suggest, when a
+\texttt{Qed} command is processed, a correct proof annotation. It is up
+to the user to modify the proof script accordingly.
+
 \section{Proof blocks and error resilience}
 
 Coq 8.6 introduces a mechanism for error resiliency: in interactive mode Coq
@@ -86,13 +92,7 @@ CoqIDE one of the following options:
 \texttt{-async-proofs-tactic-error-resilience off},
 \texttt{-async-proofs-tactic-error-resilience all},
 \texttt{-async-proofs-tactic-error-resilience $blocktype_1$,..., $blocktype_n$}.
-Valid proof block types are: ``curly'', ``par'', ``indent'', ``bullet''. 
-
-\subsubsection{Automatic suggestion of proof annotations}
-
-The command \texttt{Set Suggest Proof Using} makes Coq suggest, when a
-\texttt{Qed} command is processed, a correct proof annotation. It is up
-to the user to modify the proof script accordingly.
+Valid proof block types are: ``curly'', ``par'', ``indent'', ``bullet''.
 
 \section{Interactive mode}
 
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index fa3d61b1cd..499239b6f3 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -21,9 +21,14 @@ be used (abusively) to refer to any of the three.
 
 Before using any of the commands or options described in this chapter,
 the extraction framework should first be loaded explicitly
-via {\tt Require Extraction}. Note that in earlier versions of Coq, these
-commands and options were directly available without any preliminary
-{\tt Require}.
+via {\tt Require Extraction}, or via the more robust
+{\tt From Coq Require Extraction}.
+Note that in earlier versions of Coq, these commands and options were
+directly available without any preliminary {\tt Require}.
+
+\begin{coq_example}
+Require Extraction.
+\end{coq_example}
 
 \asection{Generating ML code}
 \comindex{Extraction}
@@ -82,9 +87,20 @@ one monolithic file or one file per \Coq\ library.
   using prefixes \verb!coq_!  or \verb!Coq_!.
 \end{description}
 
-\noindent The list of globals \qualid$_i$ does not need to be
-exhaustive: it is automatically completed into a complete and minimal
-environment. 
+\noindent The following command is meant to help automatic testing of
+  the extraction, see for instance the {\tt test-suite} directory
+  in the \Coq\ sources.
+
+\begin{description}
+\item {\tt Extraction TestCompile} \qualid$_1$ \dots\ \qualid$_n$. ~\par
+  All the globals (or modules) \qualid$_1$ \dots\ \qualid$_n$ and all
+  their dependencies are extracted to a temporary Ocaml file, just as in
+  {\tt Extraction "{\em file}"}. Then this temporary file and its
+  signature are compiled with the same Ocaml compiler used to built
+  \Coq. This command succeeds only if the extraction and the Ocaml
+  compilation succeed (and it fails if the current target language
+  of the extraction is not Ocaml).
+\end{description}
 
 \asection{Extraction options}
 
@@ -365,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-int.tex b/doc/refman/RefMan-int.tex
index fbeccb664d..eca3efcdd6 100644
--- a/doc/refman/RefMan-int.tex
+++ b/doc/refman/RefMan-int.tex
@@ -100,6 +100,11 @@ corresponds to the Chapter~\ref{Addoc-syntax}.
   presented.
   Finally, Chapter~\ref{Addoc-coqide} describes the \Coq{} integrated
   development environment. 
+
+\item The fifth part documents a number of advanced features, including
+  coercions, canonical structures, typeclasses, program extraction, and
+  specialized solvers and tactics.  See the table of contents for a complete
+  list.
 \end{itemize}
 
 At the end of the document, after the global index, the user can find
@@ -120,15 +125,6 @@ documents:
   user can read also the tutorial on recursive types (document {\tt
     RecTutorial.ps}).
 
-\item[Addendum] The fifth part (the Addendum) of the Reference Manual
-  is distributed as a separate document. It contains more
-  detailed documentation and examples about some specific aspects of the
-  system that may interest only certain users. It shares the indexes,
-  the page numbers and
-  the bibliography with the Reference Manual. If you see in one of the
-  indexes a page number that is outside the Reference Manual, it refers
-  to the Addendum. 
-
 \item[Installation] A text file INSTALL that comes with the sources
   explains how to install \Coq{}.
 
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 3daaac88b1..bf48057cdf 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -656,7 +656,7 @@ dynamically.
 searched into the current {\ocaml} loadpath (see the command {\tt
 Add ML Path} in the Section~\ref{loadpath}).  Loading of {\ocaml}
 files is only possible under the bytecode version of {\tt coqtop}
-(i.e. {\tt coqtop} called with options {\tt -byte}, see chapter 
+(i.e. {\tt coqtop.byte}, see chapter 
 \ref{Addoc-coqc}), or when {\Coq} has been compiled with a version of
 {\ocaml} that supports native {\tt Dynlink} ($\ge$ 3.11).
 
@@ -739,7 +739,7 @@ the command {\tt Declare ML Module} in the Section~\ref{compiled}).
 \subsection[\tt Print ML Path {\str}.]{\tt Print ML Path {\str}.\comindex{Print ML Path}}
 This command displays the current {\ocaml} loadpath.
 This command makes sense only under the bytecode version of {\tt
-coqtop}, i.e. using option {\tt -byte} (see the
+coqtop}, i.e. {\tt coqtop.byte} (see the
 command {\tt Declare ML Module} in the section
 \ref{compiled}).
 
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-tac.tex b/doc/refman/RefMan-tac.tex
index a23c432322..b13ae9b7b3 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4113,7 +4113,7 @@ is to set the cut expression to $c | e$, the initial cut expression
 being \texttt{emp}.
 
 
-\item \texttt{Mode} {\tt (+ | ! | -)}$^*$ {\qualid}
+\item \texttt{Mode} {\qualid} {\tt (+ | ! | -)}$^*$
 \label{HintMode}
 \comindex{Hint Mode}
 
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/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}