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.
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
Adapt to coq/coq#13842 #1418
Adapt to coq/coq#13842 #1418
Conversation
The CI failure seem unrelated |
If this is backwards compatible, can we get this merged before the upstream PR? Thanks. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Works for me.
IIUC HoTT CI is currently broken, so we can't be sure this PR is fine? Can't it be tested locally so that it can get merged? I'd like to merge the upstream PR soon but doing so would force you to merge this one right after anyways. |
If you want to trust me: I compiled it on my machine and it was fine. |
I already checked it locally and approved it, and it's been 2 days, so i think we're good to merge. |
Thanks! |
This should be backward compatible.