Possible typo in Section 6.5 "Using a generic theory"

[czhang03]

The first lemma of Section 6.5:

Lemma eqP (T : eqType) : Equality.axiom (@Equality.op T).

With custom defined Equality module in 6.4, it will fail with

T : eqType
The term "T" has type "eqType" while it is expected to have type "Type".

without custom diffed Equality module in 6.4, it will fail with

In environment
T : eqType
The term "Equality.op (T:=T)" has type "Equality.mixin_of T -> rel T"
while it is expected to have type "rel (Equality.mixin_of T)"
(cannot unify "Equality.mixin_of T" and "Equality.sort T").

Here is the simplest way to fix this:

Lemma EqP (T : eqType) : Equality.axiom (@eq_op T).

---

Coq version:

The Coq Proof Assistant, version 8.13.2 (April 2021)
compiled on Apr 9 2021 9:40:34 with OCaml 4.07.1

Installed via Coq Platform: https://github.com/coq/platform

[gares]

Thanks for reporting. We just restored the code snippets, see the homepage of the book.