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.

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 PR #18795 (more uniform API for declare.ml) #599

Merged

Conversation

herbelin
Copy link
Contributor

@herbelin herbelin commented May 20, 2024

By uniformity, and to ensure awareness of what opacity is chosen, coq/coq#18795 proposes that opaque is now made a mandatory label of add_definition, like it is for other declaration functions of the API.

The label term is also renamed to body, again by consistency of naming.

To be merged synchronously with coq/coq#18795.

@herbelin herbelin force-pushed the main+adapt-coq-pr18795-more-uniform-declare.ml branch from 9a616f9 to ac8dc90 Compare May 20, 2024 11:27
@ppedrot ppedrot merged commit abf3cdf into mattam82:main May 28, 2024
0 of 3 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants