4 files changed, 46 insertions, 27 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 fa3d61b1cd..8cb049d50e 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}).