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 #15221: a case of invalid eta-expansion in notation printing #17841

Merged
merged 3 commits into from Jul 14, 2023
Merged

Fixes #15221: a case of invalid eta-expansion in notation printing #17841

merged 3 commits into from Jul 14, 2023

Conversation

herbelin
Copy link
Member

@herbelin herbelin commented Jul 11, 2023 •
edited

#15221 revealed two problems with notations:

  • We knew that the eta-expansion done when printing notations was not necessarily well-typed and Invalid eta expansion in notation pretty-printer #15221 is an example of it. We adopt the heuristics that if the head of an application in a notation is not a variable, then the term matched will inherit the well-typing the types of the notation and eta-expansion or the corresponding argument be well-typed.
  • Applicative notations with a flexible head were considered having a fixed number of arguments.

Fixes / closes #15221

  • Added / updated test-suite.

  • Added changelog.

@herbelin herbelin added kind: fix This fixes a bug or incorrect documentation. part: notations The notation system. labels Jul 11, 2023
@herbelin herbelin added this to the 8.18+rc1 milestone Jul 11, 2023
@herbelin herbelin requested a review from a team as a code owner July 11, 2023 15:18
@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 Jul 11, 2023
@herbelin herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 11, 2023
@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 Jul 11, 2023
@herbelin herbelin mentioned this pull request Jul 11, 2023
Closed
@herbelin
Copy link
Member Author

I don't know if it is too late for 8.18. It is an easy PR so I put a 8.18 milestone, but 8.19 would also be ok.

@proux01 proux01 self-assigned this Jul 14, 2023
@proux01
Copy link
Contributor

proux01 commented Jul 14, 2023

@coqbot merge now

@coqbot-app coqbot-app bot merged commit d78feae into coq:master Jul 14, 2023
5 of 8 checks passed
@coqbot-app coqbot-app bot added this to Request 8.18+rc1 inclusion in Coq 8.18 Jul 14, 2023
@proux01
Copy link
Contributor

proux01 commented Jul 14, 2023

@gares @maximedenes I left the 8.18+rc1 milestone but feel free to postpone

@gares gares modified the milestones: 8.18+rc1, 8.19+rc1 Jul 24, 2023
@gares gares removed this from Request 8.18+rc1 inclusion in Coq 8.18 Jul 24, 2023
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: notations The notation system.
Projects
None yet
Milestone
8.19+rc1
Development

Successfully merging this pull request may close these issues.

Invalid eta expansion in notation pretty-printer
3 participants
@herbelin @proux01 @gares