MAJ V7.1

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

1 files changed, 24 insertions, 11 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}