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.

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

cbn: do not refold constants with ! and / when the ! matched. #15204

Merged
merged 1 commit into from Nov 23, 2021

Conversation

SkySkimmer
Copy link
Contributor

Fix #4555
Fix #7674

@SkySkimmer SkySkimmer requested a review from a team as a code owner November 16, 2021 11:59
@coq coq deleted a comment from coqbot-app bot Nov 16, 2021
@coq coq deleted a comment from coqbot-app bot Nov 16, 2021
@ppedrot ppedrot self-assigned this Nov 16, 2021
@SkySkimmer
Copy link
Contributor Author

@coq/coqbot-maintainers are there supposed to be this many reported checks? (on 84d8ed6, pipeline https://gitlab.com/coq/coq/-/pipelines/409828074)

@SkySkimmer SkySkimmer added the needs: changelog entry This should be documented in doc/changelog. label Nov 16, 2021
@SkySkimmer SkySkimmer removed the needs: changelog entry This should be documented in doc/changelog. label Nov 17, 2021
@SkySkimmer SkySkimmer added this to the 8.15+rc1 milestone Nov 18, 2021
@SkySkimmer SkySkimmer added the kind: fix This fixes a bug or incorrect documentation. label Nov 18, 2021
@SkySkimmer
Copy link
Contributor Author

@ppedrot ping

@ppedrot
Copy link
Member

ppedrot commented Nov 23, 2021

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 0639f0c into coq:master Nov 23, 2021
@coqbot-app coqbot-app bot added this to Request 8.15+rc1 inclusion in Coq 8.15 Nov 23, 2021
@SkySkimmer SkySkimmer deleted the cbn-volatile branch November 23, 2021 14:57
SkySkimmer added a commit to SkySkimmer/coq that referenced this pull request Nov 23, 2021
@coqbot-app coqbot-app bot moved this from Request 8.15+rc1 inclusion to Shipped in 8.15+rc1 in Coq 8.15 Nov 24, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: fix This fixes a bug or incorrect documentation.
Projects
No open projects
Coq 8.15
  
Shipped in 8.15+rc1
Development

Successfully merging this pull request may close these issues.

cbn fails to unfold even though argument is a constructor Cbn does not simplify non-recursive definition
2 participants