typographie

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

1 files changed, 9 insertions, 9 deletions

diff --git a/doc/AddRefMan-pre.tex b/doc/AddRefMan-pre.tex
index 3ddf2e0c5f..bd661aeefe 100644
--- a/doc/AddRefMan-pre.tex
+++ b/doc/AddRefMan-pre.tex
@@ -9,21 +9,21 @@
 Here you will find several pieces of additional documentation for the
 \Coq\ Reference Manual. Each of this chapters is concentrated on a
 particular topic, that should interest only a fraction of the \Coq\
-users : that's the reason why they are apart from the Reference
+users: that's the reason why they are apart from the Reference
 Manual.
 
 \begin{description}
 
 \item[Extended pattern-matching] This chapter details the use of
   generalized pattern-matching. It is contributed by Cristina Cornes
-  and Hugo Herbelin
+  and Hugo Herbelin.
 
 \item[Implicit coercions] This chapter details the use of the coercion
   mechanism.  It is contributed by Amokrane Saïbi.
 
-\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[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[Program extraction] This chapter explains how to extract in practice ML
   files from $\FW$ terms.   It is contributed by Jean-Christophe
@@ -36,10 +36,10 @@ Manual.
 \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. {\bf This
-  feature is not available in {\Coq} version 7.}
+%\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. {\bf This
+%  feature is not available in {\Coq} version 7.}
 
 \item[The {\tt Ring} tactic] This is a tactic to do AC rewriting. This
   chapter explains how to use it and how it works.