MAJ V7.1

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

4 files changed, 43 insertions, 18 deletions

diff --git a/doc/AddRefMan-pre.tex b/doc/AddRefMan-pre.tex
index 2f0b52834c..2dd2aec414 100644
--- a/doc/AddRefMan-pre.tex
+++ b/doc/AddRefMan-pre.tex
@@ -12,28 +12,41 @@ Manual.
 
 \begin{description}
 
-\item[Cases] This chapter details the use of generalized pattern-matching.
-  It is contributed by Cristina Cornes.
+\item[Extended pattern-matching] This chapter details the use of
+  generalized pattern-matching. It is contributed by Cristina Cornes
+  and Hugo Herbelin
 
-\item[Coercion] This chapter details the use of the coercion mechanism.
-  It is contributed by Amokrane Saïbi.
+\item[Implicit coercions] This chapter details the use of the coercion
+  mechanism.  It is contributed by Amokrane Saïbi.
 
-\item[Extraction] This chapter explains how to extract in practice ML
-  files from $\FW$ terms. 
+\item[Proof of imperative programs] This chapter explains how to
+  prove properties of annotated programs with imperative features.
+  It is contributed by Jean-Christophe Filliâtre
 
-\item[Natural] This chapter is due to Yann Coscoy. It is the user
-  manual of the tools he wrote for printing proofs in natural
-  language. At this time, French and English languages are supported.
+\item[Program extraction] This chapter explains how to extract in practice ML
+  files from $\FW$ terms.   It is contributed by Jean-Christophe
+  Filliâtre and Pierre Letouzey.
+
+%\item[Natural] This chapter is due to Yann Coscoy. It is the user
+%  manual of the tools he wrote for printing proofs in natural
+%  language. At this time, French and English languages are supported.
 
 \item[Omega] \texttt{Omega}, written by Pierre Crégut, solves a whole
   class of arithmetic problems.
 
 \item[Program] The \texttt{Program} technology intends to inverse the
   extraction mechanism. It allows the developments of certified
-  programs in \Coq. This chapter is due to Catherine Parent.
+  programs in \Coq. This chapter is due to Catherine Parent. {\bf This
+  feature is not available in {\Coq} version 7.}
 
-\item[Ring] \texttt{Ring} is a tactic to do AC rewriting. This
+\item[The {\tt Ring} tactic] This is a tactic to do AC rewriting. This
   chapter explains how to use it and how it works.
+  The chapter is contributed by Patrick Loiseleur.
+
+\item[The {\tt Setoid\_replace} tactic] This is a
+  tactic to do rewriting on types equipped with specific (only partially
+  substitutive) equality. The chapter is contributed by Clément Renard.
+
 
 \end{description}
 
diff --git a/doc/Cases.tex b/doc/Cases.tex
index 5b218e83e7..cb9ff0963b 100644
--- a/doc/Cases.tex
+++ b/doc/Cases.tex
@@ -1,4 +1,4 @@
-\achapter{ML-style pattern-matching}\defaultheaders
+\achapter{Extended pattern-matching}\defaultheaders
 \aauthor{Cristina Cornes}
 
 \label{Mult-Cases-full}
diff --git a/doc/Extraction.tex b/doc/Extraction.tex
index 3e630e20d7..fa8ce6c87b 100755
--- a/doc/Extraction.tex
+++ b/doc/Extraction.tex
@@ -21,7 +21,7 @@ when possible and ``ML'' will be used to refer to any of the target
 dialects.
 
 \Rem
-The extraction mechanism has been completely rewritten in version 7.0.
+The current extraction mechanism is new from version 7.0 of {\Coq}.
 In particular, the \FW\ toplevel used as intermediate step between 
 \Coq\ and ML has been abandoned.  It is also not possible 
 any more to import ML objects in this \FW\ toplevel.
diff --git a/doc/RefMan-com.tex b/doc/RefMan-com.tex
index b769e9b84d..aaef1943f0 100755
--- a/doc/RefMan-com.tex
+++ b/doc/RefMan-com.tex
@@ -19,7 +19,7 @@ roughly described below. You can also look at the \verb!man! pages of
 \section{Interactive use ({\tt coqtop})}
 In the interactive mode, also known as the \Coq~toplevel, the user can
 develop his theories and proofs step by step.  The \Coq~toplevel is
-ran by the command {\tt coqtop}. 
+run by the command {\tt coqtop}. 
 
 \index{byte-code}
 \index{native code}
@@ -68,7 +68,7 @@ arbitrary name for the resource file (see option \verb:-init-file:
 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
+This file may contain, for instance, \verb:Add LoadPath: commands to add
 directories to the load path of \Coq.
 It is possible to skip the loading of the resource file with the
 option \verb:-q:.
@@ -104,9 +104,10 @@ The following command-line options are recognized by the commands {\tt
   Add {\em directory} to the searched directories when looking for a
   file.
 
-\item[{\tt -R} {\em directory} {\em logical-path}]\ \\
-  Add recursively {\em directory} to the searched directories when looking for
-  a file, and maps this root directory to the given {\em logical path}.
+\item[{\tt -R} {\em directory} {\dirpath}]\ \\
+  This maps the subdirectory structure of physical {\em directory} to
+  logical {\dirpath} and adds {\em directory} and its subdirectories
+  to the searched directories when looking for a file.
 
 \item[{\tt -is} {\em file}, {\tt -inputstate} {\em file}]\ \\
   Cause \Coq~to use the state put in the file {\em file} as its input
@@ -150,6 +151,17 @@ The following command-line options are recognized by the commands {\tt
   Load \Coq~compiled file {\em file}{\tt .vo} and import it ({\tt
     Require} {\em file}).
 
+\item[{\tt -compile} {\em file}]\ \\
+  This compiles file {\em file}{\tt .v} into {\em file}{\tt .vo}.
+  This option implies option {\tt -batch} and {\tt -silent}. It is
+  only available for {\tt coqtop}.
+
+%\item[{\tt -compile-verbose} {\em file}]\ \\
+%  This compiles file {\em file}{\tt .v} into {\em file}{\tt .vo} with
+%  a copy of the contents of the file on standard input.
+%  This option implies option {\tt -batch} and {\tt -silent}. It is
+%  only available for {\tt coqtop}.
+
 \item[{\tt -batch}]\ \\
   Batch mode : exit just after arguments parsing. This option is only
   used by {\tt coqc}.