Merging the code paths for fixpoint and cofixpoints - #19107
Merged
coqbot-app[bot] merged 3 commits intoJun 21, 2024
Merged
Conversation
herbelin
added
kind: cleanup
coqbot-app
Bot
added
the
needs: full CI
1 task
github-actions
Bot
added
the
needs: rebase
proux01
removed
the
needs: merge of dependency
proux01
force-pushed
the
master+unify-fixpoint-cofixpoint-execution-paths
branch
from
June 12, 2024 14:22
d398c7a to
c995ce3
Compare
coqbot-app
Bot
removed
the
needs: rebase
Member
Author
|
@coqbot run full ci |
coqbot-app
Bot
removed
the
needs: full CI
Contributor
|
Certainly a nice cleanup we want to merge in master but no particular need to get it in 8.20, postponing the milestone. |
herbelin
added
the
request: full CI
herbelin
force-pushed
the
master+unify-fixpoint-cofixpoint-execution-paths
branch
from
June 18, 2024 09:35
c995ce3 to
d088556
Compare
coqbot-app
Bot
removed
the
request: full CI
SkySkimmer
approved these changes
Jun 18, 2024
herbelin
added
the
request: full CI
herbelin
force-pushed
the
master+unify-fixpoint-cofixpoint-execution-paths
branch
from
June 19, 2024 08:02
d088556 to
16dfbaa
Compare
coqbot-app
Bot
removed
the
request: full CI
Member
Author
|
Rebased to restart CI. |
This was referenced Jun 19, 2024
herbelin
added
the
request: full CI
coqbot-app
Bot
removed
the
request: full CI
herbelin
added
the
request: full CI
herbelin
force-pushed
the
master+unify-fixpoint-cofixpoint-execution-paths
branch
from
June 19, 2024 18:11
bd51aa0 to
ef7d108
Compare
coqbot-app
Bot
removed
the
request: full CI
Member
Author
|
At first view, the CI failures are the standard current ones. |
Contributor
|
@coqbot merge now |
Contributor
|
@SkySkimmer: Please take care of the following overlays:
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This is the second part of #18811.
The merge is obtained by using a data type
recursion_order_exprthat tells if an optionalstruct/wf/measure(as inFixpoint) or a corecursion (as inCoFixpoint) or an unknown cause of recursion (as inTheorem with). This is then interpreted as apossible_guard(which can be either a recursion or a corecursion, thanks to #18743).Depends on:
Synchronous overlays: