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 #17897: lost of canonical name of auxiliary constants of mutual fix/cofix at refolding time in "cbn" #18616

Merged
merged 3 commits into from Feb 4, 2024
Merged

Fixes #17897: lost of canonical name of auxiliary constants of mutual fix/cofix at refolding time in "cbn" #18616

merged 3 commits into from Feb 4, 2024

Conversation

herbelin
Copy link
Member

@herbelin herbelin commented Feb 3, 2024 •
edited

Fixes / closes #17897

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

@herbelin herbelin added kind: fix This fixes a bug or incorrect documentation. part: tactics part: reduction strategies The Strategy command for defining reduction straegies. labels Feb 3, 2024
@herbelin herbelin added this to the 8.20+rc1 milestone Feb 3, 2024
@herbelin herbelin requested review from a team as code owners February 3, 2024 12:26
@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 Feb 3, 2024
@herbelin herbelin mentioned this pull request Feb 3, 2024
Closed
@herbelin herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Feb 3, 2024
herbelin added a commit to herbelin/github-coq that referenced this pull request Feb 3, 2024
@herbelin
Change log for coq#18616
4981907
@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 Feb 3, 2024
ppedrot
ppedrot reviewed Feb 3, 2024
View reviewed changes
tactics/cbn.ml Outdated Show resolved Hide resolved
@ppedrot ppedrot self-assigned this Feb 3, 2024
@herbelin herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Feb 3, 2024
herbelin added a commit to herbelin/github-coq that referenced this pull request Feb 3, 2024
@herbelin
Change log for coq#18616
1122998
@herbelin herbelin force-pushed the master+fix17897-cbn-wrong-canonical-name-refolding branch from 4981907 to 1122998 Compare February 3, 2024 13:27
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Feb 3, 2024
@herbelin herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Feb 3, 2024
@herbelin herbelin force-pushed the master+fix17897-cbn-wrong-canonical-name-refolding branch from 1122998 to 84dd115 Compare February 3, 2024 14:18
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Feb 3, 2024
@ppedrot
Copy link
Member

ppedrot commented Feb 4, 2024

@coqbot merge now

@coqbot-app coqbot-app bot merged commit cee5193 into coq:master Feb 4, 2024
5 of 6 checks passed
louiseddp pushed a commit to louiseddp/coq that referenced this pull request Feb 27, 2024
@herbelin @louiseddp
Change log for coq#18616
af8fa09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@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. part: tactics
Projects
None yet
Milestone
8.20+rc1
Development

Successfully merging this pull request may close these issues.

cbn leaves behind unnamable constants when asked to reduce Pos.add_carry
2 participants
@herbelin @ppedrot