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
Deprecate NZDomain #18539
Deprecate NZDomain #18539
Conversation
theories/Numbers/NatInt/NZDomain.v
Outdated
Attributes deprecated(since="8.20", | ||
note="Please open an issue if you think this file is of general interest.") |
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.
Attributes deprecated(since="8.20", | |
note="Please open an issue if you think this file is of general interest.") | |
Attributes deprecated(since="8.20"). |
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.
Do you want the same change in the changelog?
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.
Why not, the sentence is not very useful.
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.
Done, thank you for your suggestions.
e9e7a26
to
3c7cbbd
Compare
The file NZDomain, while informative and well written, is of little use to the end user and makes NatInt depend on PeanoNat.
3c7cbbd
to
1d3fa5e
Compare
@coqbot run full ci |
@coqbot merge now |
The file NZDomain, while informative and well written, is of little use to the end user and makes NatInt depend on PeanoNat.