Skip to content

Let post-processing of Derive statements take the same route as Definition and Theorem - #19578

Merged
coqbot-app[bot] merged 2 commits into
rocq-prover:masterfrom
herbelin:master+merge-derive-proof-processing
Oct 29, 2024
Merged

Let post-processing of Derive statements take the same route as Definition and Theorem#19578
coqbot-app[bot] merged 2 commits into
rocq-prover:masterfrom
herbelin:master+merge-derive-proof-processing

Conversation

@herbelin

@herbelin herbelin commented Sep 20, 2024 •
edited
Loading

Copy link
Copy Markdown
Member

With #19092 and #19322, we can now see Derive statements as non-recursive telescopic blocks of theorems and take the standard now-unified route in use for Definition and Theorem.

As a particular case, polymorphic Derive directly inherits the private polymorphism feature for its opaque componens.

Depends on:

@herbelin herbelin added kind: cleanup Code removal, deprecation, refactorings, etc. needs: merge of dependency This PR depends on another PR being merged first. part: derive request: full CI Use this label when you want your next push to trigger a full CI. labels Sep 20, 2024
@herbelin herbelin added this to the 8.21+rc1 milestone Sep 20, 2024
@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 Sep 20, 2024
@herbelin herbelin mentioned this pull request Sep 20, 2024
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 Sep 20, 2024
@herbelin
herbelin force-pushed the master+merge-derive-proof-processing branch from f46607d to 5726a82 Compare September 20, 2024 19:53
@coqbot-app coqbot-app Bot added needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. and removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels Sep 20, 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 Sep 30, 2024
@herbelin
herbelin force-pushed the master+merge-derive-proof-processing branch from 5726a82 to cf06650 Compare October 2, 2024 14:30
@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 Oct 2, 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 Oct 11, 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 Oct 12, 2024
@herbelin
herbelin force-pushed the master+merge-derive-proof-processing branch from cf06650 to 8595dbc Compare October 23, 2024 08:06
@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 Oct 23, 2024
@herbelin
herbelin marked this pull request as ready for review October 23, 2024 18:39
@herbelin
herbelin requested a review from a team as a code owner October 23, 2024 18:39
SkySkimmer
SkySkimmer approved these changes Oct 29, 2024
View reviewed changes

@SkySkimmer SkySkimmer left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

goodbye End_derive, we won't miss you

@SkySkimmer SkySkimmer self-assigned this Oct 29, 2024
@SkySkimmer

SkySkimmer commented Oct 29, 2024

Copy link
Copy Markdown
Contributor

@coqbot merge now

@coqbot-app
coqbot-app Bot merged commit fddde8e into rocq-prover:master Oct 29, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@SkySkimmer SkySkimmer SkySkimmer approved these changes

Assignees

@SkySkimmer SkySkimmer

Labels

kind: cleanup Code removal, deprecation, refactorings, etc. part: derive

Projects

None yet

Milestone

9.0+rc1

Development

Successfully merging this pull request may close these issues.

2 participants

@herbelin @SkySkimmer