diff --git a/tex/chFingroup.tex b/tex/chFingroup.tex
index 39b02aa7..c83cfb51 100644
--- a/tex/chFingroup.tex
+++ b/tex/chFingroup.tex
@@ -92,7 +92,7 @@ \chapter{Finite group theory}
 Notation "G ><| H" := (sdprod G H)%g (at level 40, left associativity).
 \end{coq}
 Note that by equating an expression \C{(A ><| B)} with a group one
-imposes that the pre conditions hold, since a group is never the
+imposes that the preconditions hold, since a group is never the
 empty set.  Here \C{group_set} is a predicate asserting that a set
 is closed under multiplication and contains the unit; \C{1\%G} is
 the trivial group.
diff --git a/tex/chHierarchy.tex b/tex/chHierarchy.tex
index 58ea0d80..05b82462 100644
--- a/tex/chHierarchy.tex
+++ b/tex/chHierarchy.tex
@@ -592,7 +592,7 @@ \section{Packed classes}\label{sec:packed}
 \end{coq}
 
 Line 1 merely lets us explicitly use a \C{choiceType} where an
-\C{eqType} is expected, which is rare as structures are almost alway
+\C{eqType} is expected, which is rare as structures are almost always
 implicit and inferred.  It is line 2 that really lets \C{choiceType}
 extend \C{eqType}, because it makes it possible to use any
 \emph{element} \C{(T : choiceType)} as an element of an \C{eqType},
@@ -733,7 +733,7 @@ \section{Packed classes}\label{sec:packed}
 Structure type := Pack {sort; _ : class_of sort}.
 \end{coq}
 \index[coq]{\C{comRingType}}
-The two structures that are coumpounded this way can be declared
+The two structures that are compounded this way can be declared
 indifferently as \C{base} or as \C{mixin}.
 Since we construct explicitly the links between structures with the
 packed class pattern, the fact that the hierarchy is no longer a tree
@@ -858,7 +858,7 @@ \section{Parameters and constructors}\label{sec:phant}
 allows us to write \C{(V : lmodType (int * rat))}. Indeed, type inference
 fills in the unsightly expression
 \lstinline/(pair_ringType int_ringType rat_ringType)/ for \C{R}. This elaboration happens when
-solving the unification problem triggerd by the need to unify
+solving the unification problem triggered by the need to unify
 \C{(Phant ?)} with \C{(int * rat)}.
 
 
diff --git a/tex/chNumbers.tex b/tex/chNumbers.tex
index e668274b..31bae03c 100644
--- a/tex/chNumbers.tex
+++ b/tex/chNumbers.tex
@@ -56,7 +56,7 @@ \chapter{Numbers}
 zmodp is not a quotient of Z but the finite type ordinals equipped with
 arith ops.
 
-Cauchy reals have no decideable equality, not an eqtype, unless you axiom
+Cauchy reals have no decidable equality, not an eqtype, unless you axiom
 but then the setoid presentation is stupid.
 
 minor: int = pos nat + neg\_or\_zero nat (you get only 2 cases in proofs)
diff --git a/tex/chProgramming.tex b/tex/chProgramming.tex
index 6cbdf50b..f7fcbf65 100644
--- a/tex/chProgramming.tex
+++ b/tex/chProgramming.tex
@@ -545,7 +545,7 @@ \subsection{Local definitions}
 \C{(fun x => x + x + x) B}, we use the variable \C{x} as an
 abbreviation for \C{B}. It is specially useful when \C{B} happens to
 be a very large expression: readability is improved by avoiding the
-repetition of \C{B}, which may otherwise obfuscate the triplication
+repetition of \C{B}, which may otherwise obfuscate the triplicate
 pattern. In the \Coq{}
 language, declaring such an abbreviation can be made even more
 readable by bringing closer the name of the abbreviation \C{x} and the
@@ -737,7 +737,7 @@ \subsection{Boolean values}\label{ssec:boolval}
 compute to the same result.  In this sense, the conjunction operation
 is associative.  We shall see in chapter~\ref{ch:proofs} that this
 known property can be \emph{stated} explicitly. To a practiced pair of
-eyes, this associativity property is implicitely used in the reading
+eyes, this associativity property is implicitly used in the reading
 process, so that the two forms of three-argument conjunctions are
 identified.
 However, when manipulating boolean expressions of the \Coq{} language,
@@ -1422,7 +1422,7 @@ \subsection{The (polymorphic) sequence data type}
 \index[coq]{\C{forall}}
 so as to \emph{bind} the value \C{A} of the argument in the type of
 the output. Even if the $\forall$ symbol is actually written and displayed as
-\verb+forall+ in Coq, in this book we typeset it usfollowing the standard
+\verb+forall+ in Coq, in this book we typeset it following the standard
 mathematical notation for that quantifier.
 The same goes for the other constructor of \C{seq}, named
 \C{cons}.  This function actually takes three arguments: a type \C{A},
@@ -2173,7 +2173,7 @@ \section{Iterators and mathematical notations}
 $$
 and, more generally, in order to make explicit the meaning of the capital
 notations like $\bigcap_{i=1}^nA_i,
-\prod_{i=1}^nu_i, \dots$, we need to decribe an iteration procedure
+\prod_{i=1}^nu_i, \dots$, we need to describe an iteration procedure
 akin to the \C{foldr} program. We illustrate this on the example of
 the summation symbol (for a finite sum):
 
diff --git a/tex/chProofLanguage.tex b/tex/chProofLanguage.tex
index 1c86c687..d94a66b3 100644
--- a/tex/chProofLanguage.tex
+++ b/tex/chProofLanguage.tex
@@ -10,7 +10,7 @@ \chapter{A proof language for formal proofs}{}
 Still, the use of a dedicated proof language enables a higher level
 description of the formal proof being constructed.  
 The \mcbSSR{} proof language give us tools to structure proofs and
-to tame bookeeping, a form of bureaucracy typical of formal proofs.
+to tame bookkeeping, a form of bureaucracy typical of formal proofs.
 
 Structure is given by splitting large proofs in blocks with a
 specific, declared, purpose and by factoring repetition such as
@@ -19,7 +19,7 @@ \chapter{A proof language for formal proofs}{}
 or a generalization of the goal. The \C{have} and \C{without loss} tactics
 precisely cover this need.
 
-Bookeeping is the ubiquitous activity of context management, that is
+Bookkeeping is the ubiquitous activity of context management, that is
 naming or discarding assumptions in order to track their lifetime to tide
 the context up, as well as massaging assumptions and goals as to
 please the formality requirements of Coq.  A paradigmatic bookkeeping
@@ -27,7 +27,7 @@ \chapter{A proof language for formal proofs}{}
 distinct names to \C{A} and \C{B}: unlikely to be a pregnant step of
 the proof.  The language of intro-patterns together with then
 goal-as-stack model provides a very flexible tool to
-succinctly deal with bookeeping.
+succinctly deal with bookkeeping.
 
 Structure and manageable size are key to the maintenance of proofs by
 a team of people.  Being small in size helps maintenance since when
@@ -1249,7 +1249,7 @@ \section{Proof maintenance: a matter of style}
 contribute in a substantial way to write maintainable formal proofs.
 Coming up with a list of unobjectionable golden rules would be quite pretentious,
 and probably impossible to do, but we will anyway try to give some
-advices out of our experience. 
+advice out of our experience.
 
 The first and most important one is that formal proofs are just computer code
 about mathematical proofs, hence \emph{good practices in both domains}
@@ -1262,7 +1262,7 @@ \section{Proof maintenance: a matter of style}
 More specifically, each mathematical object comes with properties that are
 pervasively and silently used in each and every proof. In order to make a
 formal proof look like pen and paper one, this conciseness has to be retained,
-or the noise of formality risks to hide the salient part of the proof.
+or the noise of formality risks hiding the salient part of the proof.
 
 A striking similarity lies in the usability of lemmas
 compared to the one of computer code procedures (functions, or methods).
@@ -1383,7 +1383,7 @@ \subsection{On the readability of formal proofs}
 achieve that: At worse, if the step is too obscure, the reader will
 ignore the text, and just see what happens by executing it.\\
 In other words, the flow of a proof script should be homogeneous and
-distil human-readable information at a suitable, regular pace.
+distill human-readable information at a suitable, regular pace.
 
 
 \subsection{Fail early and locally to ease repair}
diff --git a/tex/chSigmaBool.tex b/tex/chSigmaBool.tex
index 2fabae12..cadaecf7 100644
--- a/tex/chSigmaBool.tex
+++ b/tex/chSigmaBool.tex
@@ -594,7 +594,7 @@ \section{Finite types and their theory}
 \end{coq}
 
 Given that the most recurrent way of showing that an enumeration
-validates \C{Finite.axiom} is by proving that it is both duplicate free
+validates \C{Finite.axiom} is by proving that it is both duplicate-free
 and exhaustive, a convenience mixin constructor is provided.
 
 \begin{coq}{name=fintype}{title=Declare a finType}
@@ -771,7 +771,7 @@ \section{Finite functions}
 of finite functions changed.
 The new implementation is based on a specific list-like data type indexed over
 the list of the elements of the domain. Thanks to this more sophisticated
-ecoding, the current Coq type checker acceps, for example, the following
+ecoding, the current Coq type checker accepts, for example, the following
 declaration of a 3-branch tree:
 \C{Inductive tree3 := Leaf of nat | Node of \{ffun 'I_3 -> tree3\}.}
 At the time of writing Coq rejects the declaration above with the definition
@@ -808,7 +808,7 @@ \section{Finite functions}
 
 \begin{coq}{name=subtdecl}{}
 Definition fun_of_fin aT rT f x := tnth (@fgraph aT rT f) (enum_rank x).
-Coercion fun_of_fin : finfun >-> FunClass.
+Coercion fun_of_fin : finfun >-> Funclass.
 Definition finfun aT rT f := @Finfun aT rT (codom_tuple f).
 Notation "[ 'ffun' x : aT => F ]" := (finfun (fun x : aT => F))
 \end{coq}
diff --git a/tex/chSpecification.tex b/tex/chSpecification.tex
index f3c4902e..5adf9fe0 100644
--- a/tex/chSpecification.tex
+++ b/tex/chSpecification.tex
@@ -868,14 +868,14 @@ \subsection{Inductive specs with indices}\label{ssec:specs}
 writing \C{andP} is equivalent to \C{(@andP _ _)}, a term whose type
 is \C{(reflect (_ /\\ _) (_ && _))}.  The value of the index of the
 inductive family, to be replaced by \C{true} and \C{false} in the
-respective branches of a case analysi, is thus
+respective branches of a case analysis, is thus
 a pattern \C{(_ && _)}. Therefore, the goal is searched for an instance of
 such pattern.  The matching algorithm used to find an instance of this
 pattern is the same as one used by the \C{rewrite} tactic, for the
-instanciation of rewrite rules.
+instantiation of rewrite rules.
 
 
-The following proof script illustrates how to deal with a boolen
+The following proof script illustrates how to deal with a boolean
 conjunction \C{a && b}, which appears in the premise of a boolean
 implication, almost as conveniently as if it were a conjunction in
 \C{Prop}.
@@ -971,7 +971,7 @@ \subsection{Inductive specs with indices}\label{ssec:specs}
 \index[coq]{\C{ltngtP}}
 
 In practice lines of reasoning consisting in a specific branching of
-a proof can often be modelled by an appropriate spec lemma.
+a proof can often be modeled by an appropriate spec lemma.
 
 \mantra{The structure of the proof shall not be driven by the syntax of the
 definition/predicate under study but by the view/spec used to reason about it.}
@@ -1357,7 +1357,7 @@ \section{Notational aspects of specifications}
 This notational trick is reminiscent of Kronecker's $\delta$ notation.
 Similarly, in the last line the membership test is turned into
 a number, that is shown to be equivalent to the count of any
-element in a list that is duplicate free.
+element in a list that is duplicate-free.
 
 % Another example of a coercion that is related to the running example
 % of the current chapter is \lstinline/sort/.  Typically the projection
diff --git a/tex/chTT.tex b/tex/chTT.tex
index e2edc134..66cc2616 100644
--- a/tex/chTT.tex
+++ b/tex/chTT.tex
@@ -305,7 +305,7 @@ \section{Terms, types, sorts}\label{sec:terms}
 though. First, there is no way in type theory to introduce a term, even
 a variable, without simultaneously introducing its type. Things are
 different in set theory, where an object $a$ can be constructed without
-necessarily being casted as being the element of a super-set
+necessarily being cast as being the element of a super-set
 $A$. Second, a judgment is not a proposition in the same sense as the
 set-theoretic sentence $t \in T$ would be. In particular, one cannot
 reason (internally) by case analysis on the proof that
@@ -877,7 +877,7 @@ \section{Inductive types}\label{ssec:indtypes}
 
 \section{More connectives}\label{sec:moreconns}
 We have seen in section~\ref{sec:propiuq} that functions, i.e.~terms
-with a product type, provide a datastructure for proofs of implication
+with a product type, provide a data structure for proofs of implication
 and universally quantified statements.
 Using inductive types, it is possible to describe more data
 structures than mere functions. %of the formalism
@@ -920,7 +920,7 @@ \section{More connectives}\label{sec:moreconns}
 Moreover \C{and} is polymorphic:
 \C{A} and \C{B} are parameters standing for arbitrary propositions.
 As a consequence, it models faithfully the introduction rule of
-conjunction, i.e. the rule govering the construction of proofs of
+conjunction, i.e. the rule governing the construction of proofs of
 conjunctive statements.
 
 Note that the definition of the pair data type,
@@ -1150,7 +1150,7 @@ \section{Inductive reasoning}\label{ssec:indreason}
 It is worth mentioning that this principle is general enough to
 prove the ``stronger'' induction principle that give access, in
 the inductive step, to the property \C{P} on all numbers
-small than \C{n.+1} and not just its predecessor.
+smaller than \C{n.+1} and not just its predecessor.
 
 \begin{coq}{}{}
 Lemma strong_nat_ind (P : nat -> Prop)
@@ -1243,7 +1243,7 @@ \section{Inductive reasoning}\label{ssec:indreason}
 %% Excluded middle, in its generality, can only be \emph{axiomatized},
 %% i.e., assumed globally.
 
-%% The \mcbMC{} library is axiom free.  This makes the library compatible
+%% The \mcbMC{} library is axiom-free.  This makes the library compatible
 %% with any combination of axioms that is known to be consistent with the
 %% Calculus of Inductive Constructions. Some formal developments in
 %% \Coq{} tend to assume the excluded middle axiom, even if the proofs
diff --git a/tex/chTypeInference.tex b/tex/chTypeInference.tex
index a0ba26f6..2ce20838 100644
--- a/tex/chTypeInference.tex
+++ b/tex/chTypeInference.tex
@@ -49,7 +49,7 @@ \chapter{Implicit parameters}{}
 said to be declarative when it explains what it computes rather than
 how. The programs in question are strictly linked with the Prolog
 programming language, a technology that found applications in artificial
-intelligence and computational linguistic.}
+intelligence and computational linguistics.}
 that have access to
 %\marginnote{explain declarative programs}
 the library of already formalized facts.  In this way one can make the
@@ -234,7 +234,7 @@ \section{Type inference by example}
 heuristic is applied in a systematic way when a global option is
 declared: every definition posterior to the declaration may feature
 implicit arguments even if not \C{Argument} command is used to declare
-them mannualy. This has been the case so far, and in the rest of the
+them manually. This has been the case so far, and in the rest of the
 section and of the book, we will work again under the assumption that
 following the global options have been set, in accordance with
 Chapter~\ref{ssec:runcoq}:
@@ -1136,7 +1136,7 @@ \section{The generic theory of sequences}\label{sec:seqtypetheory}
 \C{ReflectT} and \C{ReflectF} carry a proof, each branch of this
 analysis features an extra assumption; the branch corresponding to
 \C{ReflectT} has the hypothesis \C{x1 = x2} and the branch
-corrsponding to \C{ReflectF} has its negation \C{x1 != x2}.
+corresponding to \C{ReflectF} has its negation \C{x1 != x2}.
 
 As an example we build a sequence of sequences, and we assert that
 we can use the \C{==} and \C{\\in} notation on it, as well as apply
diff --git a/tex/nat.tex b/tex/nat.tex
index 1363f808..57bf463e 100644
--- a/tex/nat.tex
+++ b/tex/nat.tex
@@ -59,7 +59,7 @@ \section{Comparisons}
 \paragraph{See also}
 Section~\ref{nat:more-rel}.
 
-\section{Basic arithmetics}
+\section{Basic arithmetic}
 
 \begin{tabular}{llll}
 Notation  & Term      & Type & Meaning \\\hline