remove workaround for coq/coq#8994

[Alizter]

This changed the behaviour of resolution in a few places, but nothing a quick modification to the proof wouldn't fix.

• fixes Remove workarounds for coq/coq#8994 #1541

[jdchristensen]

What about the other fields that still have primed versions?

[Alizter]

Actually that's a good point. I've only addressed one. I'll draft this for now and make sure I've got them all.

Well, specifically about that bug anyway. I need to think a bit more about why we still have primed fields in CatEquiv.

[jdchristensen]

(Just to be clear, I meant the other fields of the same Class.)

[Alizter]

I tried removing the primes in the other fields and got the wildcat library working, however Coq gets stuck on the Defined of one of the proofs of ExactSequence. Specifically isexact_connect_R.

Not sure what is going on there. I'll keep my changes and submit in a PR after this is merged if you want to take a closer look.

[jdchristensen]

I guess the issue is the one explained in a comment: Since apparently a field of a record can't be the source of a coercion ....

I think it's fine to merge this to at least get rid of one redefinition.

[Alizter]

I also had a go at removing InO_internal from ReflectiveSubuniverse but I was not successful.

[Alizter]

Rebasing this breaks DisplayedEquiv. @gio256 could you have a look at what is wrong? I wasn't able to fix it.