Coq-HoTT
Coq-HoTT copied to clipboard
Remove workarounds for coq/coq#8994
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.
https://github.com/HoTT/HoTT/blob/ab1bb7f53948cc968b7a7d5e8f7276cc20bea57c/theories/Modalities/ReflectiveSubuniverse.v#L35-L36
(How do I make GFM display a snippet?)
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
You can also click "copy permalink" rather than "copy link" from the drop-down when highlighting lines
Thanks!
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.