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").
The first lemma of Section 6.5:
With custom defined
Equality
module in 6.4, it will fail withwithout custom diffed
Equality
module in 6.4, it will fail withHere is the simplest way to fix this:
Coq version:
Installed via Coq Platform: https://github.com/coq/platform