6 files changed, 99 insertions, 41 deletions
diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex
index 7ffe252253..1609e4a041 100644
--- a/doc/refman/AsyncProofs.tex
+++ b/doc/refman/AsyncProofs.tex
@@ -6,7 +6,7 @@
 
 This chapter explains how proofs can be asynchronously processed by Coq.
 This feature improves the reactivity of the system when used in interactive
-mode via CoqIDE.  In addition to that, it allows Coq to take advantage of
+mode via CoqIDE. In addition, it allows Coq to take advantage of
 parallel hardware when used as a batch compiler by decoupling the checking
 of statements and definitions from the construction and checking of proofs
 objects.
@@ -22,7 +22,12 @@ For example, in interactive mode, some errors coming from the kernel of Coq
 are signaled late.  The type of errors belonging to this category
 are universe inconsistencies.
 
-Last, at the time of writing, only opaque proofs (ending with \texttt{Qed} or \texttt{Admitted}) can be processed asynchronously.
+At the time of writing, only opaque proofs (ending with \texttt{Qed} or \texttt{Admitted}) can be processed asynchronously.
+
+Finally, asynchronous processing is disabled when running CoqIDE in Windows. The
+current implementation of the feature is not stable on Windows. It can be
+enabled, as described below at \ref{interactivecaveats}, though doing so is not
+recommended.
 
 \section{Proof annotations}
 
@@ -46,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
@@ -81,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}
 
@@ -112,6 +117,7 @@ the kernel to check all the proof objects, one has to click the button
 with the gears. Only then are all the universe constraints checked.
 
 \subsubsection{Caveats}
+\label{interactivecaveats}
 
 The number of worker processes can be increased by passing CoqIDE the
 \texttt{-async-proofs-j $n$} flag.  Note that the memory consumption
@@ -120,7 +126,8 @@ the master process. Also note that increasing the number of workers may
 reduce the reactivity of the master process to user commands.
 
 To disable this feature, one can pass the \texttt{-async-proofs off} flag to
-CoqIDE.
+CoqIDE. Conversely, on Windows, where the feature is disabled by default,
+pass the \texttt{-async-proofs on} flag to enable it.
 
 Proofs that are known to take little time to process are not delegated to a
 worker process.  The threshold can be configure with \texttt{-async-proofs-delegation-threshold}.  Default is 0.03 seconds.
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index a8889be814..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}
 
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-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/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}