Fix typos in the Extraction part of the reference manual.

In particular, fix the name of all the user contributions.

1 files changed, 43 insertions, 56 deletions

diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index 187fe5342..74c8374de 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -110,17 +110,14 @@ even if some inlining is done, the inlined constant are nevertheless
 printed, to ensure session-independent programs.
 
 Concerning Haskell, type-preserving optimizations are less useful
-because of lazyness. We still make some optimizations, for example in
+because of laziness. We still make some optimizations, for example in
 order to produce more readable code.
 
 The type-preserving optimizations are controlled by the following \Coq\ options:
 
 \begin{description}
 
-\item \optindex{Extraction Optimize}
-{\tt Set Extraction Optimize.}
-
-\item {\tt Unset Extraction Optimize.}
+\item \optindex{Extraction Optimize} {\tt Unset Extraction Optimize.}
 
 Default is Set. This controls all type-preserving optimizations made on
 the ML terms (mostly reduction of dummy beta/iota redexes, but also
@@ -130,8 +127,6 @@ ML term as close as possible to the Coq term.
 \item \optindex{Extraction Conservative Types}
 {\tt Set Extraction Conservative Types.}
 
-\item {\tt Unset Extraction Conservative Types.}
-
 Default is Unset. This controls the non type-preserving optimizations
 made on ML terms (which try to avoid function abstraction of dummy
 types). Turn this option to Set to make sure that {\tt e:t}
@@ -141,8 +136,6 @@ code of {\tt e} and {\tt t} respectively.
 \item \optindex{Extraction KeepSingleton}
 {\tt Set Extraction KeepSingleton.}
 
-\item {\tt Unset Extraction KeepSingleton.}
-
 Default is Unset. Normally, 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
@@ -150,21 +143,15 @@ removed and this type is seen as an alias to the inner type.
 The typical example is {\tt sig}. This option allows disabling this
 optimization when one wishes to preserve the inductive structure of types.
 
-\item \optindex{Extraction AutoInline}
-{\tt Set Extraction AutoInline.} 
-
-\item {\tt Unset Extraction AutoInline.} 
+\item \optindex{Extraction AutoInline} {\tt Unset Extraction AutoInline.}
 
-Default is Set, so by default, the extraction mechanism is free to
-inline the bodies of some defined constants, according to some heuristics
+Default is Set. The extraction mechanism
+inlines the bodies of some defined constants, according to some heuristics
 like size of bodies, uselessness of some arguments, etc. Those heuristics are
 not always perfect; if you want to disable this feature, do it by Unset.
 
-\item \comindex{Extraction Inline}
-{\tt Extraction Inline} \qualid$_1$ \dots\ \qualid$_n$. 
-
-\item \comindex{Extraction NoInline}
-{\tt Extraction NoInline} \qualid$_1$ \dots\ \qualid$_n$. 
+\item \comindex{Extraction Inline} \comindex{Extraction NoInline}
+{\tt Extraction [Inline|NoInline] \qualid$_1$ \dots\ \qualid$_n$}.
 
 In addition to the automatic inline feature, you can tell to
 inline some more constants by the {\tt Extraction Inline} command. Conversely, 
@@ -265,28 +252,28 @@ extracted files. The extraction recognizes whether the realized axiom
 should become a ML type constant or a ML object declaration.
 
 \Example
-\begin{coq_example}
+\begin{coq_example*}
 Axiom X:Set.
 Axiom x:X.
 Extract Constant X => "int".
 Extract Constant x => "0".
-\end{coq_example}   
+\end{coq_example*}
 
 Notice that in the case of type scheme axiom (i.e. whose type is an
 arity, that is a sequence of product finished by a sort), then some type
-variables has to be given. The syntax is then: 
+variables have to be given. The syntax is then:
 
 \begin{description}
-\item{\tt Extract Constant} \qualid\ \str$_1$ \dots\ \str$_n$ {\tt =>} \str.
+\item{\tt Extract Constant \qualid\ \str$_1$ \dots\ \str$_n$ => \str.}
 \end{description}
 
 The number of type variables is checked by the system. 
 
 \Example
-\begin{coq_example}
+\begin{coq_example*}
 Axiom Y : Set -> Set -> Set.
 Extract Constant Y "'a" "'b" => " 'a*'b ".
-\end{coq_example}
+\end{coq_example*}
 
 Realizing an axiom via {\tt Extract Constant} is only useful in the
 case of an informative axiom (of sort Type or Set). A logical axiom
@@ -308,7 +295,7 @@ types and constructors.  For instance, the user may want to use the ML
 native boolean type instead of \Coq\ one.  The syntax is the following:
 
 \begin{description}
-\item{\tt Extract Inductive} \qualid\ {\tt =>} \str\ {\tt [} \str\ \dots\ \str\ {\tt ]}\ {\it optstring}.\par
+\item{\tt Extract Inductive \qualid\ => \str\ [ \str\ \dots\ \str\ ] {\it optstring}.}\par
   Give an ML extraction for the given inductive type. You must specify
   extractions for the type itself (first \str) and all its
   constructors (between square brackets). If given, the final optional
@@ -412,7 +399,7 @@ For example, here are two kinds of problem that can occur:
 \begin{itemize}
   \item If some part of the program is {\em very} polymorphic, there
     may be no ML type for it. In that case the extraction to ML works
-    all right but the generated code may be refused by the ML
+    alright but the generated code may be refused by the ML
     type-checker. A very well known example is the {\em distr-pair}
     function:
 \begin{verbatim}
@@ -549,34 +536,34 @@ Some pathological examples of extraction are grouped in the file
 
 \asubsection{Users' Contributions}
 
- Several of the \Coq\ Users' Contributions use extraction to produce 
- certified programs. In particular the following ones have an automatic 
- extraction test (just run {\tt make} in those directories): 
-
- \begin{itemize}
- \item Bordeaux/Additions
- \item Bordeaux/EXCEPTIONS
- \item Bordeaux/SearchTrees
- \item Dyade/BDDS
- \item Lannion
- \item Lyon/CIRCUITS
- \item Lyon/FIRING-SQUAD
- \item Marseille/CIRCUITS
- \item Muenchen/Higman
- \item Nancy/FOUnify
- \item Rocq/ARITH/Chinese
- \item Rocq/COC
- \item Rocq/GRAPHS
- \item Rocq/HIGMAN
- \item Sophia-Antipolis/Stalmarck
- \item Suresnes/BDD
- \end{itemize}
-
- Lannion, Rocq/HIGMAN and Lyon/CIRCUITS are a bit particular. They are 
- examples of developments where {\tt Obj.magic} are needed.
- This is probably due to an heavy use of impredicativity.
- After compilation those two examples run nonetheless,
- thanks to the correction of the extraction~\cite{Let02}. 
+Several of the \Coq\ Users' Contributions use extraction to produce
+certified programs. In particular the following ones have an automatic
+extraction test:
+
+\begin{itemize}
+\item {\tt additions}
+\item {\tt bdds}
+\item {\tt canon-bdds}
+\item {\tt chinese}
+\item {\tt continuations}
+\item {\tt coq-in-coq}
+\item {\tt exceptions}
+\item {\tt firing-squad}
+\item {\tt founify}
+\item {\tt graphs}
+\item {\tt higman-cf}
+\item {\tt higman-nw}
+\item {\tt hardware}
+\item {\tt multiplier}
+\item {\tt search-trees}
+\item {\tt stalmarck}
+\end{itemize}
+
+{\tt continuations} and {\tt multiplier} are a bit particular. They are
+examples of developments where {\tt Obj.magic} are needed.  This is
+probably due to an heavy use of impredicativity. After compilation, those
+two examples run nonetheless, thanks to the correction of the
+extraction~\cite{Let02}.
 
 %%% Local Variables: 
 %%% mode: latex