Merge PR #925: Document Extraction TestCompile

2 files changed, 24 insertions, 6 deletions

diff --git a/CHANGES b/CHANGES
index 5a18da3c0..c9a8418cc 100644
--- a/CHANGES
+++ b/CHANGES
@@ -82,6 +82,8 @@ Standard Library
 Plugins
 
 - The mathematical proof language (also known as declarative mode) was removed.
+- A new command Extraction TestCompile has been introduced, not meant
+  for the general user but instead for Coq's test-suite.
 
 Dependencies
 
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index fa3d61b1c..8cb049d50 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}