Diagnose bad coercion

[gio256]

Related to #1807.

So far I've been able to remove all the primed fields except cate_fun'. Declaring the method of the typeclass directly as the corecion CatEquiv >-> Hom makes at least one proof in Homotopy/ExactSequence.v hang.

Steps to reproduce:

• search and replace cate_fun' to cate_fun in the HasEquivs class declaration in WildCat/Equiv.v.
• Comment out the definition of cate_fun in WildCat/Equiv.v.
• Check the proof marked @todo in Homotopy/ExactSequence.v

I'm not sure what the problem is yet, but it might just be that using a typeclass method as a coercion doesn't work well enough to bother with. I'll see if I can't minimize a bug or find a fix still, though.

[gio256]

Also still primed are cate_inv', cate_issect', and cate_isretr', but these are more of a design decision I think.

Currently cate_inv' builds only the inverse map b $-> a while cate_inv builds the equivalence b $<~> a. So in contrast to the other redefined fields of HasEquivs, one could reasonably want to use both the primed and unprimed version of all three of these fields, and it's just a question of which version should have a prime on it.

[Alizter]

This is likely because typeclass resolution is hanging. You can try to see what it is doing with Set Typeclasses Depth 3 and Set Typeclasses Debug. Alternatively, you can use nrefine which is short for notypeclasses refine, this will leave the goals that are typeclasses out. We probably don't need many typeclasses for the goal to be well-typed here anyway. Once you've used nrefine or snrefine for the simple variant which doesn't hide goals that can be inferred, you can resolve the typeclass proofs with 1: exact _..