Fixed some typos in the reference manual.

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

1 files changed, 4 insertions, 3 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 501f9b0b1..276c4c47a 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -161,7 +161,7 @@ Reset Initial.
    \item The body of {\ident$_i$} uses an incorrect elimination for
      {\ident} (see Sections~\ref{Fixpoint} and~\ref{Caseexpr}).
    \item The type of the projections {\ident$_i$} depends on previous
-   projections which themselves couldn't be defined.
+   projections which themselves could not be defined.
    \end{enumerate}  
 \end{Warnings}     
 
@@ -763,7 +763,8 @@ defined:
 
 %Complete!!
 The way this recursive function is defined is the subject of several
-papers by Yves Bertot and Antonia Balaa on one hand and  Gilles Barthe, Julien Forest, David Pichardie and Vlad Rusu on the other hand.
+papers by Yves Bertot and Antonia Balaa on the one hand, and Gilles Barthe,
+Julien Forest, David Pichardie, and Vlad Rusu on the other hand.
 
 %Exemples ok ici
 
@@ -1097,7 +1098,7 @@ a-priori and a-posteriori.
 
 \subsubsection{Implicit Argument Binders}
 
-In the first setting, one wants to explicitely give the implicit
+In the first setting, one wants to explicitly give the implicit
 arguments of a constant as part of its definition. To do this, one has
 to surround the bindings of implicit arguments by curly braces:
 \begin{coq_eval}