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

Fixes #18223: nested entry coercions possibly printed in the wrong order depending on the order in which coercions were declared #18230

Merged
merged 2 commits into from Nov 3, 2023
Merged

Fixes #18223: nested entry coercions possibly printed in the wrong order depending on the order in which coercions were declared #18230

merged 2 commits into from Nov 3, 2023

Conversation

herbelin
Copy link
Member

Fixes / closes #18223

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

@herbelin herbelin added kind: fix This fixes a bug or incorrect documentation. part: notations The notation system. part: custom The custom notation system. labels Oct 30, 2023
@herbelin herbelin added this to the 8.19+rc1 milestone Oct 30, 2023
@herbelin herbelin requested a review from a team as a code owner October 30, 2023 20:33
@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 Oct 30, 2023
@herbelin herbelin mentioned this pull request Oct 30, 2023
Closed
@proux01 proux01 self-assigned this Oct 31, 2023
@proux01
Copy link
Contributor

proux01 commented Oct 31, 2023

@coqbot run full ci

@coqbot-app coqbot-app bot removed 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 Oct 31, 2023
@coqbot-app coqbot-app
Copy link
Contributor

coqbot-app bot commented Oct 31, 2023

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

@proux01
Copy link
Contributor

proux01 commented Nov 3, 2023

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 2af3ead into coq:master Nov 3, 2023
19 checks passed
@ejgallego
Copy link
Member

Should this go into 8.18.1 ?

@proux01
Copy link
Contributor

proux01 commented Nov 5, 2023

It's not immediate to backport so I'd say no.

@herbelin herbelin mentioned this pull request Feb 25, 2024
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@proux01 proux01 proux01 approved these changes

Assignees

@proux01 proux01

Labels
kind: fix This fixes a bug or incorrect documentation. part: custom The custom notation system. part: notations The notation system.
Projects
None yet
Milestone
8.19+rc1
Development

Successfully merging this pull request may close these issues.

Coq uses wrong notations using custom entries
3 participants
@herbelin @proux01 @ejgallego