mise a jour V7

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

3 files changed, 106 insertions, 151 deletions

diff --git a/doc/RefMan-com.tex b/doc/RefMan-com.tex
index 63e97dff5f..b769e9b84d 100755
--- a/doc/RefMan-com.tex
+++ b/doc/RefMan-com.tex
@@ -49,8 +49,8 @@ compile it into a {\em file}{\tt .vo} file (See ~\ref{compiled}).
 \Warning The name {\em file} must be a regular {\Coq} identifier, as
 defined in the section \ref{lexical}. It
 must only contain letters, digits or underscores
-(\_). Thus it can be \verb+/bar/foo/toto.v+ but not 
-\verb+/bar/foo/to-to+ . 
+(\_). Thus it can be \verb+/bar/foo/toto.v+ but cannot be
+\verb+/bar/foo/to-to.v+ . 
 
 Notice that the \verb!-byte! and \verb!-opt! options are still
 available with \verb!coqc!  and allow you to select the byte-code or
@@ -69,46 +69,7 @@ below), or the name of another user to load the resource file of
 someone else (see option \verb:-user:).
 
 This file may contain, for instance, \verb:AddPath: commands to add
-directories to the load path of \Coq.  You can use the environment
-variable \verb:$COQLIB: which refer to the \Coq\
-library. Remember that the
-default load path already contains the following directories:
-\begin{verbatim}
-           .
-           $CAMLP4LIB
-           $COQLIB/tactics/tcc
-           $COQLIB/tactics/programs/EXAMPLES
-           $COQLIB/tactics/programs
-           $COQLIB/tactics/contrib/polynom
-           $COQLIB/tactics/contrib/omega
-           $COQLIB/tactics/contrib/natural
-           $COQLIB/tactics/contrib/linear
-           $COQLIB/tactics/contrib/extraction
-           $COQLIB/tactics/contrib/acdsimpl/simplify_rings
-           $COQLIB/tactics/contrib/acdsimpl/simplify_naturals
-           $COQLIB/tactics/contrib/acdsimpl/acd_simpl_def
-           $COQLIB/tactics/contrib/acdsimpl
-           $COQLIB/tactics/contrib
-           $COQLIB/theories/ZARITH
-           $COQLIB/theories/TREES
-           $COQLIB/theories/TESTS
-           $COQLIB/theories/SORTING
-           $COQLIB/theories/SETS
-           $COQLIB/theories/RELATIONS/WELLFOUNDED
-           $COQLIB/theories/RELATIONS
-           $COQLIB/theories/LOGIC
-           $COQLIB/theories/LISTS
-           $COQLIB/theories/INIT
-           $COQLIB/theories/DEMOS/PROGRAMS
-           $COQLIB/theories/DEMOS/OMEGA
-           $COQLIB/theories/DEMOS
-           $COQLIB/theories/BOOL
-           $COQLIB/theories/REALS
-           $COQLIB/theories/ARITH
-           $COQLIB/tactics
-           $COQLIB/states
-\end{verbatim}
-
+directories to the load path of \Coq.
 It is possible to skip the loading of the resource file with the
 option \verb:-q:.
 
@@ -116,14 +77,14 @@ option \verb:-q:.
 \label{EnvVariables}
 \index{Environment variables}
 
-There are 3 environment variables used by the \Coq\ system.
+There are three environment variables used by the \Coq\ system.
 \verb:$COQBIN: for the directory where the binaries are,
 \verb:$COQLIB: for the directory whrer the standard library is, and 
 \verb:$COQTOP: for the directory of the sources. The latter is useful
-only for developpers that are writing there own tactics using
+only for developers that are writing their own tactics and are using
 \texttt{coq\_makefile} (see \ref{Makefile}). If \verb:$COQBIN: or
 \verb:$COQLIB: are not defined, \Coq\ will use the default values
-(choosen at installation time). So these variables are useful onlt if
+(defined at installation time). So these variables are useful only if
 you move the \Coq\ binaries and library after installation.
 
 \section{Options}
@@ -149,7 +110,7 @@ The following command-line options are recognized by the commands {\tt
 
 \item[{\tt -is} {\em file}, {\tt -inputstate} {\em file}]\ \\
   Cause \Coq~to use the state put in the file {\em file} as its input
-  state. The default state is {\em tactics.coq}.
+  state. The default state is {\em initial.coq}.
   Mainly useful to build the standard input state.
 
 \item[{\tt -nois}]\ \\
@@ -157,11 +118,10 @@ The following command-line options are recognized by the commands {\tt
   standard input state.
 
 \item[{\tt -notactics}]\ \\
-  Forbid the dynamic loading of tactics, and start on the input state
-  {\em state.coq}.
+  Forbid the dynamic loading of tactics.
 
 \item[{\tt -init-file} {\em file}]\ \\
-  Take {\em file} as resource file, instead of {\tt \$HOME/.coqrc.7.0}.
+  Take {\em file} as the resource file.
 
 \item[{\tt -q}]\ \\
   Cause \Coq~not to load the resource file.
@@ -209,13 +169,14 @@ The following command-line options are recognized by the commands {\tt
   instead of the standard one. Not of general use.
 
 \item[{\tt -bindir} {\em directory}]\ \\
+  Set the directory containing \Coq\ binaries.
   It is equivalent to do \texttt{export COQBIN=}{\em directory}
   before lauching \Coq.
 
 \item[{\tt -libdir} {\em file}]\ \\
+  Set the directory containing \Coq\ libraries.
   It is equivalent to do \texttt{export COQLIB=}{\em directory}
   before lauching \Coq.
-  
 
 \item[{\tt -where}]\ \\
   Print the \Coq's standard library location and exit.
@@ -227,15 +188,14 @@ The following command-line options are recognized by the commands {\tt
   Print a short usage and exit.
 \end{description}
 
-{\tt coqtop} owns an additional option:
+% {\tt coqtop} owns an additional option:
 
-\begin{description}
-\item[{\tt -searchisos}]\ \\
-  Launch the {\sf Coq\_SearchIsos} toplevel
-  (see section~\ref{coqsearchisos}, page~\pageref{coqsearchisos}).
-\end{description}
+% \begin{description}
+% \item[{\tt -searchisos}]\ \\
+%   Launch the {\sf Coq\_SearchIsos} toplevel
+%   (see section~\ref{coqsearchisos}, page~\pageref{coqsearchisos}).
+% \end{description}
 
-See the manual pages for more details.
 % $Id$ 
 
 %%% Local Variables: 
diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex
index ac71826301..1bc2ada370 100644
--- a/doc/RefMan-gal.tex
+++ b/doc/RefMan-gal.tex
@@ -28,7 +28,7 @@ The notation ``\nelist{\gensymbol}{sep}'' stands for a non empty
 sequence of expressions parsed by the ``{\gensymbol}'' entry and
 separated by the literal ``{\tt sep}''\footnote{This is similar to the
 expression ``{\gensymbol} $\{$ {\tt sep} {\gensymbol} $\}$'' in
-standard BNF, or``{\gensymbol} $($ {\tt sep} {\gensymbol} $)$*'' in
+standard BNF, or ``{\gensymbol} $($ {\tt sep} {\gensymbol} $)$*'' in
 the syntax of regular expressions.}.
 
 Similarly, the notation ``\nelist{\gensymbol}{}'' stands for a non
@@ -64,7 +64,7 @@ they are recognized by the following lexical class:
 \begin{tabular}{rcl} 
 {\firstletter} & ::= & \ml{a..z}\op\ml{A..Z}\op\ml{\_}\op\ml{\$} \\
 {\subsequentletter} & ::= & \ml{a..z}\op\ml{A..Z}\op\ml{0..9}\op\ml{\_}\op\ml{\$}\op\ml{'} \\
-{\ident} & ::= & {\firstletter}\sequencewithoutblank{\subsequentletter}{}\\
+{\ident} & ::= & {\firstletter} \sequencewithoutblank{\subsequentletter}{}\\
 \end{tabular}
 \end{center}
 Identifiers can contain at most 80 characters, and all characters are
@@ -107,7 +107,7 @@ the end of each line, just before the newline. For instance,
 \begin{flushleft}
 \begin{small}
 \begin{verbatim}
-AddPath "$COQLIB/\
+AddPath "/usr/local/coq/\
 contrib/Rocq/LAMBDA".
 \end{verbatim}
 \end{small}
diff --git a/doc/RefMan-uti.tex b/doc/RefMan-uti.tex
index cd266d4cf1..67f838127f 100755
--- a/doc/RefMan-uti.tex
+++ b/doc/RefMan-uti.tex
@@ -17,14 +17,12 @@ which source is in {\tt tactic.ml} with the command
      % coqmktop -opt -o mytop.out tactic.cmx
 \end{verbatim}
 where {\tt tactic.ml} has been compiled with the native-code
-compiler {\tt ocamlopt}. This command generates an image of \Coq\ 
-called {\tt mytop.out}. One can run this new toplevel with the command
-{\tt coqtop -image mytop.out}.
+compiler {\tt ocamlopt}. This command generates an executable
+called {\tt mytop.out}. To use this executable to compile your \Coq\
+files, use {\tt coqc -image mytop.out}.
 
-A basic example is the native-code version of \Coq\ ({\tt coqtop
-  -opt}), which can be generated by {\tt coqmktop -opt -o coqopt.out}.
-
-See the man page of {\tt coqmktop} for more details and options.
+A basic example is the native-code version of \Coq\ ({\tt coqtop.opt}),
+which can be generated by {\tt coqmktop -opt -o coqopt.opt}.
 
 
 \paragraph{Application: how to use the Objective Caml debugger with Coq.}
@@ -43,7 +41,7 @@ bytecode toplevel with the following command:
 \end{quotation}
 
 
-To launch the \ocaml debugger with the image you need to execute it in
+To launch the \ocaml\ debugger with the image you need to execute it in
 an environment which correctly sets the \texttt{COQLIB} variable.
 Moreover, you have to indicate the directories in which
 \texttt{ocamldebug} should search for Caml modules.
@@ -52,7 +50,7 @@ A possible solution is to use a wrapper around \texttt{ocamldebug}
 which detects the executables containing the word \texttt{coq}. In
 this case, the debugger is called with the required additional
 arguments. In other cases, the debugger is simply called without additional
-arguments. Such a wrapper can be found in the \texttt{tools/dev}
+arguments. Such a wrapper can be found in the \texttt{dev/}
 subdirectory of the sources. 
 
 \section{Modules dependencies}\label{Dependencies}\index{Dependencies}
@@ -71,7 +69,9 @@ commands ({\tt Require}, {\tt Requi\-re Export}, {\tt Require Import},
 {\tt Require Implementation}), but also at the command {\tt Declare ML Module}.
 
 Dependencies of \ocaml\ modules are computed by looking at
-\verb!open! commands and the dot notation {\em module.value}.
+\verb!open! commands and the dot notation {\em module.value}. However,
+this is done approximatively and you are advised to use {\tt ocamldep}
+instead for the \ocaml\ modules dependencies.
 
 See the man page of {\tt coqdep} for more details and options.
 
@@ -79,21 +79,21 @@ See the man page of {\tt coqdep} for more details and options.
 \section{Creating a {\tt Makefile} for \Coq\ modules}
 \label{Makefile}
 \index{Makefile@{\tt Makefile}}
-\index{DoMakefile@{\tt do\_Makefile}}
+\index{CoqMakefile@{\tt coq\_Makefile}}
 
 When a proof development becomes large and is split into several files,
 it becomes crucial to use a tool like {\tt make} to compile \Coq\
 modules.
 
-The writing of a generic and complete {\tt Makefile} may seem tedious
+The writing of a generic and complete {\tt Makefile} may be a tedious work
 and that's why \Coq\ provides a tool to automate its creation,
-{\tt do\_Makefile}. Given the files to compile, the command {\tt
-do\_Makefile} prints a 
+{\tt coq\_makefile}. Given the files to compile, the command {\tt
+coq\_makefile} prints a 
 {\tt Makefile} on the standard output. So one has just to run the
 command:
 
 \begin{quotation}
-\texttt{\% do\_Makefile} {\em file$_1$.v \dots\ file$_n$.v} \texttt{> Makefile}
+\texttt{\% coq\_makefile} {\em file$_1$.v \dots\ file$_n$.v} \texttt{> Makefile}
 \end{quotation}
 
 The resulted {\tt Makefile} has a target {\tt depend} which computes the
@@ -117,53 +117,53 @@ There is a target {\tt all} to compile all the files {\em file$_1$
 the corresponding {\tt .v} file (so you can do {\tt make} {\em file}{\tt.vo}
 to compile the file {\em file}{\tt.v}).
 
-{\tt do\_Makefile} can also handle the case of ML files and
+{\tt coq\_makefile} can also handle the case of ML files and
 subdirectories. For more options type
 
 \begin{quotation}
-\texttt{\% do\_Makefile --help}
+\texttt{\% coq\_makefile --help}
 \end{quotation}
 
 \Warning To compile a project containing \ocaml{} files you must keep
 the sources of \Coq{} somewhere and have an environment variable named
 \texttt{COQTOP} that points to that directory.
 
-\section{{\sf Coq\_SearchIsos}: information retrieval in a \Coq\ proofs
-library}
-\label{coqsearchisos}
-\index{Coq\_SearchIsos@{\sf Coq\_SearchIsos}}
-
-In the \Coq\ distribution, there is also a separated and independent tool,
-called {\sf Coq\_SearchIsos}, which allows the search in accordance with {\tt
-SearchIsos}\index{SearchIsos@{\tt SearchIsos}} (see section~\ref{searchisos})
-in a \Coq\ proofs library. More precisely, this program begins, once launched
-by {\tt coqtop -searchisos}\index{coqtopsearchisos@{\tt
-coqtop -searchisos}}, loading lightly (by using specifications functions)
-all the \Coq\ objects files ({\tt .vo}) accessible by the {\tt LoadPath} (see
-section~\ref{loadpath}). Next, a prompt appears and four commands are then
-available:
-
-\begin{description}
-\item [{\tt SearchIsos}]\ \\
-  Scans the fixed context.
-\item [{\tt Time}]\index{Time@{\tt Time}}\ \\
-  Turns on the Time Search Display mode (see section~\ref{time}).
-\item [{\tt Untime}]\index{Untime@{\tt Untime}}\ \\
-  Turns off the Time Search Display mode (see section~\ref{time}).
-\item [{\tt Quit}]\index{Quit@{\tt Quit}}\ \\
-  Ends the {\tt coqtop -searchisos} session.
-\end{description}
-
-When running {\tt coqtop -searchisos} you can use the two options:
-
-\begin{description}
-\item[{\tt -opt}]\ \\
-  Runs the native-code version of {\sf Coq\_SearchIsos}.
-
-\item[{\tt -image} {\em file}]\ \\
-  This option sets the binary image to be used to be {\em file}
-  instead of the standard one. Not of general use.
-\end{description}
+% \section{{\sf Coq\_SearchIsos}: information retrieval in a \Coq\ proofs
+% library}
+% \label{coqsearchisos}
+% \index{Coq\_SearchIsos@{\sf Coq\_SearchIsos}}
+
+% In the \Coq\ distribution, there is also a separated and independent tool,
+% called {\sf Coq\_SearchIsos}, which allows the search in accordance with {\tt
+% SearchIsos}\index{SearchIsos@{\tt SearchIsos}} (see section~\ref{searchisos})
+% in a \Coq\ proofs library. More precisely, this program begins, once launched
+% by {\tt coqtop -searchisos}\index{coqtopsearchisos@{\tt
+% coqtop -searchisos}}, loading lightly (by using specifications functions)
+% all the \Coq\ objects files ({\tt .vo}) accessible by the {\tt LoadPath} (see
+% section~\ref{loadpath}). Next, a prompt appears and four commands are then
+% available:
+
+% \begin{description}
+% \item [{\tt SearchIsos}]\ \\
+%   Scans the fixed context.
+% \item [{\tt Time}]\index{Time@{\tt Time}}\ \\
+%   Turns on the Time Search Display mode (see section~\ref{time}).
+% \item [{\tt Untime}]\index{Untime@{\tt Untime}}\ \\
+%   Turns off the Time Search Display mode (see section~\ref{time}).
+% \item [{\tt Quit}]\index{Quit@{\tt Quit}}\ \\
+%   Ends the {\tt coqtop -searchisos} session.
+% \end{description}
+
+% When running {\tt coqtop -searchisos} you can use the two options:
+
+% \begin{description}
+% \item[{\tt -opt}]\ \\
+%   Runs the native-code version of {\sf Coq\_SearchIsos}.
+
+% \item[{\tt -image} {\em file}]\ \\
+%   This option sets the binary image to be used to be {\em file}
+%   instead of the standard one. Not of general use.
+% \end{description}
 
 
 \section{\Coq\ and \LaTeX}\label{Latex}
@@ -192,51 +192,34 @@ See the man page of {\tt coq-tex} for more details.
 have been completely produced with {\tt coq-tex}.
 
 
-\subsection{Pretty printing \Coq\ listings with \LaTeX}
-  \index{Coq2latex@{\tt coq2latex}}
-
-\verb!coq2latex! is a tool for printing \Coq\ listings using \LaTeX\ : 
-keywords are printed in bold face, comments in italic, some tokens
-are printed in a nicer way (\verb!->! becomes $\rightarrow$, etc.)
-and indentations are kept at the beginning of lines.
-Line numbers are printed in the right margin, every 10 lines.
-
-In regular mode, the command 
+\subsection{Documenting \Coq\ files with \LaTeX}
+  \index{Coqweb@{\tt coqweb}}
 
-\begin{flushleft}
-~~~~~\texttt{\% coq2latex {\rm\em file}}
-\end{flushleft}
+\verb!coqweb! is a ``literate programming'' tool for \Coq, inspired
+by Knuth's WEB tool. The user documents his or her files with \LaTeX\ material
+inside \Coq\ comments and \verb!coqweb! produces a \LaTeX\ document
+from this unique source.
+\Coq\ parts are displayed in a nice way (\verb!->! becomes
+$\rightarrow$, keywords are typeset in a bold face,
+etc.). Additionally, an index is produced which gives the places where
+the various globals are introduced.
 
-\noindent produces a \LaTeX\ file which is sent to the \verb!latex! command,
-and the result to the \verb!dvips! command. 
-
-It is also possible to  get the \LaTeX\  file, DVI file or  PostSCript
-file,  on the standard output or  in a file.  See the man page of {\tt
-coq2latex} for more details and options.
+\verb!coqweb! is developped and distributed independently of the
+system \Coq. It is freely available, with sources, binaries and a full
+documentation, at \verb!www.lri.fr/~filliatr/coqweb!.
 
 
 \section{\Coq\ and HTML}\label{Html}\index{HTML}
-  \index{Coq2html@{\tt coq2html}}
-
-As for \LaTeX, it is also possible to pretty print \Coq\ listing with
-HTML. The document looks like the \LaTeX\ one, with links added when
-possible : links to other \Coq\ modules in {\tt Require} commands, and
-links to identifiers defined in other modules (when they are found in a
-path given with {\tt -I} options).
-
-In regular mode, the command 
 
-\begin{flushleft}
-~~~~~\texttt{\% coq2html {\rm\em file}.v}
-\end{flushleft}
-
-\noindent produces an HTML document {{\em file}{\tt .html}}.
-
-See the man page of {\tt coq2html} for more details and options.
+An HTML output can be obtained from \Coq\ files documented using
+\verb!coqweb! (see the previous paragraph). See the documentation of
+\verb!coqweb! for more details.
 
 
 \section{\Coq\ and \emacs}\label{Emacs}\index{Emacs}
 
+\subsection{The \Coq\ Emacs mode}
+
 \Coq\ comes with a Major mode for \emacs, {\tt coq.el}. This mode provides
 syntax highlighting (assuming your \emacs\ library provides
 {\tt hilit19.el}) and also a rudimentary indentation facility
@@ -263,6 +246,19 @@ the \Coq\ language, and also a rudimentary indentation facility:
   \item M-{\sc Tab} decreases the indentation level.
 \end{itemize}
 
+\subsection{Proof General}\index{Proof General}
+
+Proof General is a generic interface for proof assistants based on
+Emacs (or XEmacs). The main idea is that the \Coq\ commands you are
+editing are sent to a \Coq\ toplevel running behind Emacs and the
+answers of the system automatically inserted into other Emacs buffers. 
+Thus you don't need to copy-paste the \Coq\ material from your files
+to the \Coq\ toplevel or conversely from the \Coq\ toplevel to some
+files. 
+
+Proof General is developped and distributed independently of the
+system \Coq. It is freely available at \verb!www.proofgeneral.org!.
+
 
 \section{Module specification}\label{gallina}\index{Gallina@{\tt gallina}}
 
@@ -277,9 +273,8 @@ See the man page of {\tt gallina} for more details and options.
 
 \section{Man pages}\label{ManPages}\index{Man pages}
 
-There are man pages for the commands {\tt coqtop}, {\tt coqc}, {\tt coqmktop},
-{\tt coqdep}, {\tt gallina},\linebreak{} {\tt coq-tex}, {\tt
-coq2latex} and {\tt coq2html}. Man pages are installed at installation time
+There are man pages for the commands {\tt coqdep}, {\tt gallina} and
+{\tt coq-tex}. Man pages are installed at installation time
 (see installation instructions in file {\tt INSTALL}, step 6).
 
 \addtocontents{sh}{ENDREFMAN=\thepage}