Skip to content

Guard fix cleaner#22109

Draft
yannl35133 wants to merge 8 commits into
rocq-prover:masterfrom
Yann-Leray:guard-fix-cleaner
Draft

Guard fix cleaner#22109
yannl35133 wants to merge 8 commits into
rocq-prover:masterfrom
Yann-Leray:guard-fix-cleaner

Conversation

@yannl35133

Copy link
Copy Markdown
Contributor

Depends on #21814 and #22081

Clean up how fixpoints are checked in the guard condition, and finish the reindentation of the rest of the functions.

@yannl35133 yannl35133 added kind: cleanup Code removal, deprecation, refactorings, etc. needs: merge of dependency This PR depends on another PR being merged first. request: full CI Use this label when you want your next push to trigger a full CI. part: fixpoints About Fixpoint, fix and mutual statements labels Jun 9, 2026
@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 Jun 9, 2026
@yannl35133 yannl35133 added the request: full CI Use this label when you want your next push to trigger a full CI. label Jun 10, 2026
@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 Jun 10, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

kind: cleanup Code removal, deprecation, refactorings, etc. needs: merge of dependency This PR depends on another PR being merged first. part: fixpoints About Fixpoint, fix and mutual statements

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant