Skip to content

Merging the code paths for Program Co/Fixpoint and Co/Fixpoint - #19257

Merged
coqbot-app[bot] merged 9 commits into
rocq-prover:masterfrom
herbelin:master+merge-fixpoint-program-fixpoint
Jun 27, 2024
Merged

Merging the code paths for Program Co/Fixpoint and Co/Fixpoint#19257
coqbot-app[bot] merged 9 commits into
rocq-prover:masterfrom
herbelin:master+merge-fixpoint-program-fixpoint

Conversation

@herbelin

@herbelin herbelin commented Jun 22, 2024 •
edited
Loading

Copy link
Copy Markdown
Member

This is the sixth part of #18811.

This is mostly about moving/factorizing code from comProgramFixpoint.ml to comFixpoint.ml applying either finish_regular or finish_program to deal with evars depending on whether Program is on or not (main commit is the last one).

Incidentally, a record is introduced to collect all the components of a fixpoint declaration.

Incidentally fixes #16906

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

Minor dependency on:

@herbelin herbelin added kind: cleanup Code removal, deprecation, refactorings, etc. part: program needs: merge of dependency This PR depends on another PR being merged first. part: fixpoints About Fixpoint, fix and mutual statements part: cofixpoints About CoFixpoint, cofix and mutual statements labels Jun 22, 2024
@herbelin herbelin added this to the 8.21+rc1 milestone Jun 22, 2024
@herbelin
herbelin requested review from a team as code owners June 22, 2024 10:31
@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 Jun 22, 2024
This was referenced Jun 22, 2024
Merged
Closed
@herbelin herbelin added the kind: fix This fixes a bug or incorrect documentation. label Jun 22, 2024
This was referenced Jun 22, 2024
Merged
Merged
@github-actions github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jun 24, 2024
@herbelin herbelin added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: merge of dependency This PR depends on another PR being merged first. labels Jun 24, 2024
@herbelin
herbelin force-pushed the master+merge-fixpoint-program-fixpoint branch from 3913e21 to f665619 Compare June 24, 2024 17:31
@coqbot-app coqbot-app Bot removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. 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 Jun 24, 2024
ppedrot
ppedrot approved these changes Jun 25, 2024
View reviewed changes

@ppedrot ppedrot left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM.

@ppedrot ppedrot self-assigned this Jun 27, 2024
@ppedrot

ppedrot commented Jun 27, 2024

Copy link
Copy Markdown
Member

@coqbot merge now

@coqbot-app
coqbot-app Bot merged commit 27085c3 into rocq-prover:master Jun 27, 2024
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: cleanup Code removal, deprecation, refactorings, etc. kind: fix This fixes a bug or incorrect documentation. part: cofixpoints About CoFixpoint, cofix and mutual statements part: fixpoints About Fixpoint, fix and mutual statements part: program

Projects

None yet

Milestone

9.0+rc1

Development

Successfully merging this pull request may close these issues.

Program Fixpoint mishandles let binders (Error: Anomaly "Uncaught exception Not_found.")

2 participants

@herbelin @ppedrot