It is a real pleasure to read this clear text about Coq. If it may help
here are some typos and suggestions about the version draft 0, August 27,
2016. Capital letters (such as S in the first line below) signal something to
add or remove, depending on what is in the book.
0.1.2: aN librarian
Page 13: an operation on an object -> an operation on one object
Page 14: n + 2 -> n + 1 (twice)
Page 18 [remove space], implyb -> , AND implyb
Page 20: the immediate subterm of n AND the computation proceeds
Page 20: we need to revert to the “match .. with .. end” syntax.'' ->
it is more convenient/simpler to ..'', because one can also use nested
'if .. then .. else' constructs.
Page 20: onE can prefix the fiRst pattern
Page 21: can also containS
Page 21: ``When computing with a natural number, all the pattern matching rules
are tried successively against this number.'' More important is that patterns
may 'overlap' (i.e. share matching cases) and that the result is given by
the first one that matches (in the order they are written).
Page 21: u.+1.+1.+.1 -> u.+1.+1.+1
Page 21: showing a syntactic facility to scrutinized -> showing a syntactic
facility to scrutinize
Page 22: Recursion for integers -> Recursion for natural numbers
Page 22: In this line, -> In these lines,
Page 22: the Coq systems -> the Coq system
Page 24: this chapterS
Page 24: Exchange n and m in ``(m > n) is only accepted in input and is always
printed as (n < m).'' for correspondence with the names in the block above.
That's all for today. Hope it may help.