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

Addresses #17985: error on duplicate notation variable levels #17988

Merged
merged 2 commits into from Aug 30, 2023
Merged

Addresses #17985: error on duplicate notation variable levels #17988

merged 2 commits into from Aug 30, 2023

Conversation

herbelin
Copy link
Member

Closes #17985

  • Added / updated test-suite.
  • Added changelog.

@herbelin herbelin added part: notations The notation system. kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. labels Aug 29, 2023
@herbelin herbelin added this to the 8.19+rc1 milestone Aug 29, 2023
@herbelin herbelin requested a review from a team as a code owner August 29, 2023 12:05
@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Aug 29, 2023
@herbelin herbelin mentioned this pull request Aug 29, 2023
Closed
@herbelin
Fixes coq#17985: Error on level of notation variable set more than once.
537ca34 
In practice, it is enough to simplify the code for setting levels
thanks to the pre-parsing of the main entry in 359cac9.

Also, we reset the syntax modifiers in the natural order after having
parsed the non-syntax modifiers.
@herbelin
Adding overlay for coq#17988
d95afdf
@herbelin herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Aug 29, 2023
@herbelin herbelin force-pushed the master+fix17985-error-on-duplicate-notation-variable-levels branch from 4072f7d to d95afdf Compare August 29, 2023 14:51
@coqbot-app coqbot-app bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Aug 29, 2023
@ppedrot ppedrot self-assigned this Aug 30, 2023
@ppedrot
Copy link
Member

ppedrot commented Aug 30, 2023

@coqbot merge now

@coqbot-app coqbot-app bot merged commit e0d96f9 into coq:master Aug 30, 2023
6 checks passed
Villetaneuse pushed a commit to Villetaneuse/coq that referenced this pull request Sep 9, 2023
@herbelin @Villetaneuse
Adding overlay for coq#17988
2ec8a13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ppedrot ppedrot ppedrot approved these changes

Assignees

@ppedrot ppedrot

Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: notations The notation system.
Projects
None yet
Milestone
8.19+rc1
Development

Successfully merging this pull request may close these issues.

Issue a warning when a notation declares different levels for the same term
2 participants
@herbelin @ppedrot