3 files changed, 39 insertions, 48 deletions
diff --git a/doc/Extraction.tex b/doc/Extraction.tex
index cb9949d97..45f7b81e5 100755
--- a/doc/Extraction.tex
+++ b/doc/Extraction.tex
@@ -1,16 +1,16 @@
-\achapter{Execution of extracted programs in Caml and Haskell}
-\label{CamlHaskellExtraction}
-\aauthor{Benjamin Werner and Jean-Christophe Filliātre}
+\achapter{Execution of extracted programs in Objective Caml and Haskell}
+\label{Extraction}
+\aauthor{Jean-Christophe Filliātre and Pierre Letouzey}
 \index{Extraction}
 
 It is possible to use \Coq\ to build certified and relatively
 efficient programs, extracting them from the proofs of their
-specifications. The extracted objects are terms of \FW, and can be 
+specifications. The extracted objects can be 
 obtained at the \Coq\ toplevel with the command {\tt Extraction}
-(see \ref{Extraction}).
+(see \ref{ExtractionTerm}).
 
 We present here a \Coq\ module, {\tt Extraction}, which translates the
-extracted terms to ML dialects, namely Caml Light, Objective Caml and
+extracted terms to ML dialects, namely Objective Caml and
 Haskell. In the following, we will not refer to a particular dialect
 when possible and ``ML'' will be used to refer to any of the target
 dialects.
diff --git a/doc/RefMan-com.tex b/doc/RefMan-com.tex
index 081687a8b..63e97dff5 100755
--- a/doc/RefMan-com.tex
+++ b/doc/RefMan-com.tex
@@ -12,7 +12,7 @@ There are two \Coq~commands:
 \bigskip
 
 The options are (basically) the same for the two commands, and
-roughly described below. You can also look at the \verb!man!  pages of
+roughly described below. You can also look at the \verb!man! pages of
 \verb!coqtop! and \verb!coqc! for more details.
 
 
@@ -24,23 +24,17 @@ ran by the command {\tt coqtop}.
 \index{byte-code}
 \index{native code}
 \label{binary-images}
-They are three different binary images of \Coq: the byte-code one,
-the native-code one and the full native-code one.  When invoking
-\verb!coqtop!, the byte-code version of the system is used.  The
-command \verb!coqtop -opt! runs a native-code version of the
-\Coq~system, and the command \verb!coqtop -full! a native-code version
-with the implementation code of all the tactics (that is with the code
-of the tactics \verb!Linear!, \verb!Ring! and \verb!Omega! which then
-can be required by \verb=Require=) and tools (\verb!Extraction! and
-\verb!Natural! which again become available through the command
-\verb=Require=).  Those toplevels are significantly faster than the
-byte-code one.  Notice that it is no longer possible to access the
-Caml toplevel, neither to load tactics.
-
-This byte-code toplevel is based on a Caml
+They are two different binary images of \Coq: the byte-code one and
+the native-code one (if Objective Caml provides a native-code compiler
+for your platform, which is supposed in the following).  When invoking
+\verb!coqtop! or \verb!coqc!, the native-code version of the system is
+used.  The command-line options \verb!-byte! and \verb!-opt! explicitly
+select the byte-code and the native-code versions, respectively.
+
+The byte-code toplevel is based on a Caml
 toplevel (to allow the dynamic link of tactics).  You can switch to
 the Caml toplevel with the command \verb!Drop.!, and come back to the
-\Coq~toplevel with the command \verb!Coqtoplevel.go();;!.
+\Coq~toplevel with the command \verb!Toplevel.loop();;!.
 
 % The command \verb!coqtop -searchisos! runs the search tool {\sf
 %   Coq\_SearchIsos} (see section~\ref{coqsearchisos},
@@ -51,8 +45,6 @@ the Caml toplevel with the command \verb!Drop.!, and come back to the
 The {\tt coqc} command takes a name {\em file} as argument.  Then it
 looks for a vernacular file named {\em file}{\tt .v}, and tries to
 compile it into a {\em file}{\tt .vo} file (See ~\ref{compiled}).
-With the \verb!-i! option, it compiles the specification module {\em
-file}{\tt .vi}. 
 
 \Warning The name {\em file} must be a regular {\Coq} identifier, as
 defined in the section \ref{lexical}. It
@@ -60,9 +52,9 @@ must only contain letters, digits or underscores
 (\_). Thus it can be \verb+/bar/foo/toto.v+ but not 
 \verb+/bar/foo/to-to+ . 
 
-Notice that the \verb!-opt! and \verb!-full! options are still
-available with \verb!coqc!  and allow you to compile \Coq\ files with
-an efficient version of the system.
+Notice that the \verb!-byte! and \verb!-opt! options are still
+available with \verb!coqc!  and allow you to select the byte-code or
+native-code versions of the system.
 
 
 \section{Resource file}
@@ -141,20 +133,19 @@ The following command-line options are recognized by the commands {\tt
   coqc} and {\tt coqtop}:
 
 \begin{description}
-\item[{\tt -opt}]\ \\
-  Run the native-code version of \Coq{} (or {\sf Coq\_SearchIsos} for {\tt
-coqtop}).
+\item[{\tt -byte}]\ \\
+  Run the byte-code version of \Coq{}.
 
-\item[{\tt -full}]\ \\
-  Run a native-code version of {\Coq} with all tactics.
+\item[{\tt -opt}]\ \\
+  Run the native-code version of \Coq{}.
 
 \item[{\tt -I} {\em directory}, {\tt -include} {\em directory}]\ \\
   Add {\em directory} to the searched directories when looking for a
   file.
 
-\item[{\tt -R} {\em directory}]\ \\
+\item[{\tt -R} {\em directory} {\em logical-path}]\ \\
   Add recursively {\em directory} to the searched directories when looking for
-  a file.
+  a file, and maps this root directory to the given {\em logical path}.
 
 \item[{\tt -is} {\em file}, {\tt -inputstate} {\em file}]\ \\
   Cause \Coq~to use the state put in the file {\em file} as its input
diff --git a/doc/RefMan-oth.tex b/doc/RefMan-oth.tex
index 91b89650b..c33aede1f 100644
--- a/doc/RefMan-oth.tex
+++ b/doc/RefMan-oth.tex
@@ -66,20 +66,20 @@ progress).
 
 \SeeAlso section~\ref{Conversion-tactics}.
 
-\subsection{\tt Extraction \ident.}
-\label{ExtractionIdent}
-\comindex{Extraction}
-This command displays the \FW-term extracted from {\ident}. The name
-{\ident} must refer to a defined constant or a theorem. The \FW-term
-is extracted from the term defining {\ident} when {\ident} is a
-defined constant, or from the proof-term when {\ident} is a
-theorem. The extraction is processed according to the distinction
+\subsection{\tt Extraction \term.}
+\label{ExtractionTerm}
+\comindex{Extraction} 
+This command displays the extracted term from
+{\term}. The extraction is processed according to the distinction
 between {\Set} and {\Prop}; that is to say, between logical and
-computational content (see section \ref{Sorts}).
+computational content (see section \ref{Sorts}). The extracted term is
+displayed in Objective Caml syntax, where global identifiers are still
+displayed as in \Coq\ terms.
 
-\begin{ErrMsgs}
-\item \errindex{Non informative term}
-\end{ErrMsgs}
+\begin{Variants}
+\item \texttt{Recursive Extraction {\term}.}\\
+  Recursively extracts all the material needed for the extraction of \term.
+\end{Variants}
 
 \SeeAlso chapter \ref{Extraction}
 
@@ -604,13 +604,13 @@ Objective Caml toplevel. The Objective Caml command:
 
 \begin{flushleft}
 \begin{verbatim}
-#use "include.ml";;
+#use "include";;
 \end{verbatim}
 \end{flushleft}
 
 \noindent add the right loadpaths and loads some toplevel printers for
 all abstract types of \Coq - section\_path, identfifiers, terms, judgements,
-\dots. You can also use the file \texttt{base\_include.ml} instead,
+\dots. You can also use the file \texttt{base\_include} instead,
 that loads only the pretty-printers for section\_paths and
 identfifiers. See section \ref{test-and-debug} more information on the
 usage of the toplevel. You can return back to \Coq{} with the command: