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 cbv evar case #18195

Merged
merged 3 commits into from Oct 30, 2023
Merged

Fix cbv evar case #18195

merged 3 commits into from Oct 30, 2023

Conversation

yannl35133
Copy link
Contributor

Fixes #18194

@yannl35133 yannl35133 requested a review from a team as a code owner October 22, 2023 20:35
@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 22, 2023
@yannl35133 yannl35133 mentioned this pull request Oct 22, 2023
Closed
herbelin
herbelin approved these changes Oct 23, 2023
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.

Well spotted! Could you also add the test?

@herbelin herbelin added kind: fix This fixes a bug or incorrect documentation. part: reduction strategies The Strategy command for defining reduction straegies. labels Oct 23, 2023
@herbelin herbelin added this to the 8.19+rc1 milestone Oct 23, 2023
@herbelin
Copy link
Member

Not sure it needs a full ci (others may know better than me). A change log telling it fixes #18194 would however be good (using dev/tools/make-changelog.sh).

@ppedrot
Copy link
Member

ppedrot commented Oct 23, 2023

It doesn't hurt to run a full ci: @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 23, 2023
@ppedrot ppedrot self-assigned this Oct 30, 2023
@ppedrot
Copy link
Member

ppedrot commented Oct 30, 2023

CI failures are spurious, so @coqbot merge now

@coqbot-app coqbot-app bot merged commit 03e9548 into coq:master Oct 30, 2023
5 of 8 checks passed
@yannl35133 yannl35133 deleted the cbv-evar-case branch October 30, 2023 18:16
@herbelin herbelin mentioned this pull request May 13, 2024
Open
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

@ppedrot ppedrot ppedrot approved these changes

Assignees

@ppedrot ppedrot

Labels
kind: fix This fixes a bug or incorrect documentation. part: reduction strategies The Strategy command for defining reduction straegies.
Projects
None yet
Milestone
8.19+rc1
Development

Successfully merging this pull request may close these issues.

cbv on undefined evars under binders when the substitution involves cases produces unbound rel
3 participants
@yannl35133 @herbelin @ppedrot