Merge PR #6526: Fixing various typos in the Credits chapter.

1 files changed, 5 insertions, 5 deletions

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 991c9745e..05775bfbe 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -499,7 +499,7 @@ Claude Marché coordinated the edition of the Reference Manual for
 Pierre Letouzey and Jacek Chrz\k{a}szcz respectively maintained the
 extraction tool and module system of {\Coq}.
 
-Jean-Christophe Filliâtre, Pierre Letouzey, Hugo Herbelin ando
+Jean-Christophe Filliâtre, Pierre Letouzey, Hugo Herbelin and other
 contributors from Sophia-Antipolis and Nijmegen participated to the
 extension of the library.
 
@@ -659,7 +659,7 @@ Matthieu Sozeau extended the \textsc{Russell} language, ending in an
 convenient way to write programs of given specifications, Pierre
 Corbineau extended the Mathematical Proof Language and the
 automatization tools that accompany it, Pierre Letouzey supervised and
-extended various parts the standard library, Stéphane Glondu
+extended various parts of the standard library, Stéphane Glondu
 contributed a few tactics and improvements, Jean-Marc Notin provided
 help in debugging, general maintenance and {\tt coqdoc} support,
 Vincent Siles contributed extensions of the {\tt Scheme} command and
@@ -680,7 +680,7 @@ Nicolas Tabareau made the adaptation of the interface of the old
 the interaction between Coq and its external interfaces. With Samuel
 Mimram, he also helped making Coq compatible with recent software
 tools.  Russell O'Connor, Cezary Kaliscyk, Milad Niqui contributed to
-improved the libraries of integers, rational, and real numbers. We
+improve the libraries of integers, rational, and real numbers. We
 also thank many users and partners for suggestions and feedback, in
 particular Pierre Castéran and Arthur Charguéraud, the INRIA Marelle
 team, Georges Gonthier and the INRIA-Microsoft Mathematical Components team, 
@@ -714,7 +714,7 @@ implementation of $\mathbb{N}$, $\mathbb{Z}$ or
 $\mathbb{Z}/n\mathbb{Z}$. 
 
 The main other evolutions of the library are due to Hugo Herbelin who
-made a revision of the sorting library (includingh a certified
+made a revision of the sorting library (including a certified
 merge-sort) and to Guillaume Melquiond who slightly revised and
 cleaned up the library of reals.
 
@@ -723,7 +723,7 @@ some efficiency issues and a more flexible construction of module
 types, Élie Soubiran brought a new model of name equivalence, the
 $\Delta$-equivalence, which respects as much as possible the names
 given by the users. He also designed with Pierre Letouzey a new
-convenient operator \verb!<+! for nesting functor application, what
+convenient operator \verb!<+! for nesting functor application, that
 provides a light notation for inheriting the properties of cascading
 modules.