search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.26k stars 194 forks source link

Remove workarounds for coq/coq#8994 #1541

Open Alizter opened 3 years ago

Alizter commented 3 years ago

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 commented 3 years ago

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

mikeshulman commented 3 years ago

(How do I make GFM display a snippet?)

SkySkimmer commented 3 years ago

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 commented 3 years ago

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

mikeshulman commented 3 years ago

Thanks!

Alizter commented 3 years ago

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.