-
Notifications
You must be signed in to change notification settings - Fork 66
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
Compatibility with Coq 8.8? #11
Comments
It is not compatible yet. I have an item on my own private task list to report some bugs against the Coq tracker for things like the above. It's not that hard to move past the issue you're seeing now by defining the body of the list equivalence separately, but then you'll just run into another anamoly a bit further down the file. |
I'm still using Coq 8.7 for all my uses of this library, but I think that moving to 8.8 should become a priority now. |
Okay, thanks for getting back to me so quickly! |
@siddharthist I'm more interrupt driven than I like to think, but your questions have prompted me to create those bugs today. Running the bug minifier now, and will update this issue to point to the Coq bug once created. |
Logged as coq/coq#8004 |
Once you get this working with 8.8 / master, you should add it to Coq's CI so that it doesn't accidentally break. |
@JasonGross How does one add something to Coq's CI? |
8.8 is now supported. |
Hi, I'm trying to update the version of this library in nixpkgs, but when I add the following lines to the
default.nix
there:and
I get this error when building:
Is this library compatible with Coq 8.8?
The text was updated successfully, but these errors were encountered: