Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Remove workarounds for coq/coq#8994 #1541

Open
Alizter opened this issue May 30, 2021 · 6 comments · May be fixed by #1807
Open

Remove workarounds for coq/coq#8994 #1541

Alizter opened this issue May 30, 2021 · 6 comments · May be fixed by #1807
Labels
8.14 task

Comments

@Alizter
Copy link
Collaborator

Alizter commented May 30, 2021 •
edited
Loading

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
Copy link
Contributor

mikeshulman commented Jun 1, 2021 •
edited by SkySkimmer
Loading

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

@mikeshulman
Copy link
Contributor

(How do I make GFM display a snippet?)

@SkySkimmer
Copy link
Collaborator

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
Copy link
Contributor

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

@mikeshulman
Copy link
Contributor

Thanks!

@Alizter
Copy link
Collaborator Author

Alizter commented Oct 18, 2021

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

Alizter added a commit to Alizter/HoTT that referenced this issue Jan 12, 2024
@Alizter
remove workaround for coq/coq#8994
5b53a31 
- fixes HoTT#1541

Signed-off-by: Ali Caglayan <[email protected]>
@Alizter Alizter linked a pull request Jan 12, 2024 that will close this issue
Open
Alizter added a commit to Alizter/HoTT that referenced this issue Feb 19, 2024
@Alizter
remove workaround for coq/coq#8994
cc98084 
- fixes HoTT#1541

Signed-off-by: Ali Caglayan <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
8.14 task
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

remove workaround for coq/coq#8994 Alizter/HoTT
4 participants
@JasonGross @mikeshulman @SkySkimmer @Alizter