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

Notation Warnings #228

Open
mrhaandi opened this issue Jan 17, 2025 · 4 comments
Open

Notation Warnings #228

mrhaandi opened this issue Jan 17, 2025 · 4 comments
Assignees
@DmxLarchey

Comments

@mrhaandi
Copy link
Collaborator

@DmxLarchey In the master branch, I suppressed some notation warnings in your code via -closed-notation-not-level-0,-postfix-notation-not-level-1.
Could you verify that suppressing the warning will not break the code after the deprecation deprecation phase? Or (if possible) fix the underlying issues?
@DmxLarchey DmxLarchey self-assigned this Jan 20, 2025
@DmxLarchey
Copy link
Collaborator

Hi @mrhaandi, is master supposed to be compiled with rocq only ?

@DmxLarchey DmxLarchey mentioned this issue Jan 20, 2025
Merged
@DmxLarchey
Copy link
Collaborator

See #229

@mrhaandi
Copy link
Collaborator Author

is master supposed to be compiled with rocq only ?

Currently it requires rocq as the minimum. It would be nice to keep it that way for maximal compatibility and long-term maintenance.
Of course, you if you have the coq layer installed in addition (for development / debugging) it should also compile.

@mrhaandi
Copy link
Collaborator Author

mrhaandi commented Jan 20, 2025 •
edited
Loading

@yforster I did not touch the CI (which currently fails and needs a corresponding adjustment for rocq compilation).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@DmxLarchey DmxLarchey

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@DmxLarchey @mrhaandi