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

Fix handling of recursive notations with custom entries #11311

Merged
merged 2 commits into from
Dec 21, 2019
Merged

Fix handling of recursive notations with custom entries #11311

merged 2 commits into from
Dec 21, 2019

Conversation

maximedenes
Copy link
Member

Fixes #9532
Fixes #9490

@maximedenes maximedenes requested review from mattam82 and a team as code owners December 19, 2019 11:51
@maximedenes maximedenes added kind: fix This fixes a bug or incorrect documentation. part: notations The notation system. labels Dec 19, 2019
@maximedenes maximedenes mentioned this pull request Dec 19, 2019
Closed
@maximedenes maximedenes added this to the 8.11.0 milestone Dec 19, 2019
herbelin
herbelin approved these changes Dec 19, 2019
View reviewed changes
Copy link
Member

@herbelin herbelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks very good. Well done!

@maximedenes maximedenes added the needs: changelog entry This should be documented in doc/changelog. label Dec 19, 2019
@maximedenes
Copy link
Member Author

@coq/ci-maintainers is the bedrock2 failure known?

@maximedenes
Copy link
Member Author

@coq/ci-maintainers is the bedrock2 failure known?

Ah yes, just saw mit-plv/bedrock2#120, sorry.

@maximedenes maximedenes requested a review from a team as a code owner December 20, 2019 12:27
@maximedenes maximedenes removed the needs: changelog entry This should be documented in doc/changelog. label Dec 20, 2019
@maximedenes
Copy link
Member Author

@herbelin I believe this fix is ready for merge, the windows and bedrock2 failures are known to be spurious.

@herbelin herbelin self-assigned this Dec 21, 2019
@herbelin
Copy link
Member

OK, I assign and will merge.

herbelin added a commit that referenced this pull request Dec 21, 2019
@herbelin
Merge PR #11311: Fix handling of recursive notations with custom entries
9c75b6a 
Reviewed-by: herbelin
@herbelin herbelin merged commit 515bdf5 into coq:master Dec 21, 2019
ppedrot added a commit to ppedrot/coq that referenced this pull request Dec 22, 2019
@ppedrot
Backport PR coq#11311: Fix handling of recursive notations with custo…
f7df01d 
…m entries
@maximedenes maximedenes deleted the fix-unknown-level branch August 26, 2023 09:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@herbelin herbelin herbelin approved these changes

@mattam82 mattam82 Awaiting requested review from mattam82

Assignees

@herbelin herbelin

Labels
kind: fix This fixes a bug or incorrect documentation. part: notations The notation system.
Projects
None yet
Milestone
8.11.0
2 participants
@maximedenes @herbelin