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

[declare] Call interp_proof_using only once per mutual block. #18998

Merged
merged 1 commit into from May 14, 2024
Merged

[declare] Call interp_proof_using only once per mutual block. #18998

merged 1 commit into from May 14, 2024

Conversation

ejgallego
Copy link
Member

Follow-up to #18890

Not sure what the effect on this will be, doing as suggested by the PR
discussion.

@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 May 2, 2024
@ejgallego ejgallego mentioned this pull request May 2, 2024
Merged
@ejgallego ejgallego added this to Ready in Proof Handling May 6, 2024
@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 May 8, 2024
@ejgallego
[declare] Call interp_proof_using only once per mutual block.
95177b4 
Follow-up to coq#18890

Not sure what the effect on this will be, doing as suggested by the PR
discussion.
@coqbot-app coqbot-app bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label May 13, 2024
@ejgallego ejgallego marked this pull request as ready for review May 13, 2024 18:37
@ejgallego ejgallego requested a review from a team as a code owner May 13, 2024 18:37
@ejgallego
Copy link
Member Author

@coqbot run full CI

@coqbot-app coqbot-app bot removed 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 May 13, 2024
@herbelin herbelin self-assigned this May 13, 2024
@herbelin herbelin added this to the 8.20+rc1 milestone May 14, 2024
@herbelin
Copy link
Member

Going to merge soon.

@herbelin herbelin added kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. kind: cleanup Code removal, deprecation, refactorings, etc. labels May 14, 2024
herbelin
herbelin approved these changes May 14, 2024
View reviewed changes
Copy link
Member

@herbelin herbelin left a comment

Choose a reason for hiding this comment

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

Morally, "using" clauses are common to all components of a co/fixpoint from the moment they are really recursive. No need to compute n times the same clause (knowing that each individual body already contains all the components of the co/fixpoint).

@herbelin
Copy link
Member

@coqbot merge now

@coqbot-app coqbot-app bot merged commit ee3d13e into coq:master May 14, 2024
6 checks passed
Proof Handling automation moved this from Ready to Done May 14, 2024
@ejgallego ejgallego deleted the mutual_pinfo_interp branch May 14, 2024 16:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@herbelin herbelin herbelin approved these changes

Assignees

@herbelin herbelin

Labels
kind: cleanup Code removal, deprecation, refactorings, etc. kind: enhancement Enhancement to an existing user-facing feature, tactic, etc.
Projects
Proof Handling
  
Done
Milestone
8.20+rc1
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@ejgallego @herbelin