Merge pull request #103 from math-comp/typos

typos

tex/ch0.tex

@@ -20,7 +20,7 @@ \chapter*{Introduction}
 non-standard presentation of \Coq{}, putting upfront the formalization
 choices and the proof style that are the pillars of the library.
 
-This books targets two classes of public.  On the one hand, newcomers,
+This book targets two classes of public.  On the one hand, newcomers,
 even the more mathematically inclined ones, %may
 find a soft
 introduction to the programming
@@ -123,7 +123,7 @@ \subsection*{Part 2: \parttwoname{}}
 Such solutions typically involve notions and theorems that
 are part of the \mcbMC{} library.  By programming type inference
 one can hence teach \Coq{} the contents of the library.  The system
-is then able to reconstruct the non-trivial missing pieces of information,
+is then able to reconstruct non-trivial missing pieces of information,
 as the informed reader typically does when reading a mathematical text.
 
 Formalized knowledge is organized by means of interfaces (in the spirit of
@@ -178,7 +178,7 @@ \subsection*{Conventions}
 \sum_(0 <= i < n.+2) i = (n.+1 * n.+2) %/ 2
 \end{coqout}
 
-Names of components one can \C{Require} in \Coq{} are written
+Names of library components one can \C{Require} in \Coq{} are written
 like \lib{ssreflect} or \lib{fintype}.
 
 \subsection*{Running examples in the \Coq{} system}
@@ -200,8 +200,8 @@ \subsection*{Running examples in the \Coq{} system}
 alternative approaches to integrate \Coq{} in their preferred programming
 environment.  For instance, there exist special extensions of \Coq{} for the
 popular \texttt{Emacs} programming editor (known as \texttt{Proof General})
-and for the \texttt{Eclipse} programming environment
-(known as \texttt{coqoon}).  These extensions and similar projects can easily
+and for the \texttt{Visual Studio Code} programming environment
+(known as \texttt{vscoq}).  These extensions and similar projects can easily
 be found by a search on the Internet.
 
 When starting a \Coq{} session, a few commands must be sent to the \Coq{}

tex/chProofs.tex

@@ -1122,7 +1122,7 @@ \subsubsection{Rewriting many identities in one go}
 of the arguments of the product being zero. And \C{(n1 - n2 == 0)}
 means \C{(n1 <= n2)}.
 
-The first step is performed using the following equation:
+The first step is performed using the following equation:\label{leqE}
 
 \begin{coq}{name=LeqDef}{}
 Lemma leqE m n : (m <= n) = (m - n == 0).
@@ -1853,7 +1853,7 @@ \subsection{Proofs by induction}\label{ssec:ind}
 
 Here \C{P} is quantified exactly as \C{n} is, but its type is a bit more
 complex and deserves an explanation.  As we have seen in the first
-chapter, the \C{->} denotes the type of functions; hence \C{P} is a\marginpar{There is a problem with the \C{-} macro when the first character is -, which cancels the space that precedes it}
+chapter, the ~\C{->} denotes the type of functions; hence \C{P} is a
 function from \C{nat} to \C{Prop}.  Recall that \C{Prop} is the type
 of \emph{propositions}, i.e., something we may want to prove.  In the
 light of that, \C{P} is a function producing a proposition out of a natural
@@ -2178,9 +2178,7 @@ \section{Rewrite, a Swiss army knife}\label{sec:rewrite}
 Another form of simplification that is often needed is the
 unfolding of a definition.
 For example, the lemma \C{leqE} that we used in
-\marginpar{When reading the text, I thought that \C{leqE} did exist.  I
-think we should avoid misleading readers like that.}
-the proof of \C{leq_mul2l} back in section~\ref{sec:multirew}
+the proof of \C{leq_mul2l} back in page~\pageref{leqE}
 does not exist in the library, and there is no name associated to this
 equation. It is simply the definition of \C{leq}, and we actually do
 not need to state a lemma in order to relate