Extraction: document Separate Extraction and KeepSingleton

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15746 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 29 insertions, 2 deletions

diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index ee289ee7e..1ec25f9f1 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -22,8 +22,9 @@ an explicit toplevel for the language (formerly called \textsc{Fml}).
 \asection{Generating ML code}
 \comindex{Extraction}
 \comindex{Recursive Extraction}
-\comindex{Extraction Module}
-\comindex{Recursive Extraction Module}
+\comindex{Separate Extraction}
+\comindex{Extraction Library}
+\comindex{Recursive Extraction Library}
 
 The next two commands are meant to be used for rapid preview of
 extraction. They both display extracted term(s) inside \Coq.
@@ -60,6 +61,19 @@ one monolithic file or one file per \Coq\ library.
 \item {\tt Recursive Extraction Library} \ident. ~\par
   Extraction of the \Coq\ library {\tt\ident.v} and all other modules 
   {\tt\ident.v} depends on. 
+
+\item {\tt Separate Extraction}
+      \qualid$_1$ \dots\ \qualid$_n$. ~\par
+  Recursive extraction of all the globals (or modules) \qualid$_1$ \dots\
+  \qualid$_n$ and all their dependencies, just as {\tt
+    Extraction "{\em file}"}, but instead of producing one monolithic
+  file, this command splits the produced code in separate ML files, one per
+  corresponding Coq {\tt .v} file. This command is hence quite similar
+  to {\tt Recursive Extraction Library}, except that only the needed
+  parts of Coq libraries are extracted instead of the whole. The
+  naming convention in case of name clash is the same one as
+  {\tt Extraction Library} : identifiers are here renamed
+  using prefixes \verb!coq_!  or \verb!Coq_!.
 \end{description}
 
 The list of globals \qualid$_i$ does not need to be
@@ -112,6 +126,19 @@ Default is Set. This control all optimizations made on the ML terms
 Cases, etc). Put this option to Unset if you want a ML term as close as 
 possible to the Coq term.
 
+\item \comindex{Set Extraction KeepSingleton}
+{\tt Set Extraction KeepSingleton.}
+
+\item \comindex{Unset Extraction KeepSingleton}
+{\tt Unset Extraction KeepSingleton.}
+
+Default is Unset. Normaly, when the extraction of an inductive type
+produces a singleton type (i.e. a type with only one constructor, and
+only one argument to this constructor), the inductive structure is
+removed and this type is seen as an alias to the inner type.
+The typical example is {\tt sig}. This option allows to disable this
+optimization when one wishes to preserve the inductive structure of types.
+
 \item \comindex{Set Extraction AutoInline}
 {\tt Set Extraction AutoInline.}