Remove workarounds for coq/coq#8994

[Alizter]

coq/coq#12975 / coq/coq#8994 has now been fixed by coq/coq#9711, so we can finally remove workarounds. I am only aware of https://github.com/HoTT/HoTT/blob/d49e8b11e212b188e9d3d49115ddc8aef8f351e8/theories/WildCat/Equiv.v#L46-L48 at the moment, so it would be good to note any others here.

Once we update to 8.14 we will no longer need to do the workarounds.

[mikeshulman]

https://github.com/HoTT/HoTT/blob/ab1bb7f53948cc968b7a7d5e8f7276cc20bea57c/theories/Modalities/ReflectiveSubuniverse.v#L35-L36

[mikeshulman]

(How do I make GFM display a snippet?)

[SkySkimmer]

github displays a snippet when you link to a specific commit. master is a branch so no snippet

protip: when on the file's page, shortcut y will change the url from the branch to the current commit without reloading

[JasonGross]

You can also click "copy permalink" rather than "copy link" from the drop-down when highlighting lines

[mikeshulman]

Thanks!

[Alizter]

I was working on this and found an anomaly https://github.com/coq/coq/issues/15042. Fixing this will have to wait till I can work out how to deal with it.