1 files changed, 5 insertions, 5 deletions

diff --git a/doc/refman/AddRefMan-pre.tex b/doc/refman/AddRefMan-pre.tex
index 461e8e6d0c..eee41a6798 100644
--- a/doc/refman/AddRefMan-pre.tex
+++ b/doc/refman/AddRefMan-pre.tex
@@ -18,15 +18,15 @@ Manual.
   and Hugo Herbelin.
 
 \item[Implicit coercions] This chapter details the use of the coercion
-  mechanism.  It is contributed by Amokrane Saïbi.
+  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
+%  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
-  Filliâtre and Pierre Letouzey.
+  Filliâtre and Pierre Letouzey.
 
 \item[Program] This chapter explains the use of the \texttt{Program}
   vernacular which allows the development of certified
@@ -37,7 +37,7 @@ Manual.
 %  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
+\item[omega] \texttt{omega}, written by Pierre Crégut, solves a whole
   class of arithmetic problems.
 
 \item[The {\tt ring} tactic] This is a tactic to do AC rewriting. This
@@ -46,7 +46,7 @@ Manual.
 
 \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.
+  substitutive) equality. The chapter is contributed by Clément Renard.
 
 \item[Calling external provers] This chapter describes several tactics
   which call external provers.