8000 Fully sort polymorphic inductives by SkySkimmer · Pull Request #18331 · rocq-prover/rocq · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Fully sort polymorphic inductives #18331

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
Merged
merged 10 commits into from
Nov 29, 2023
Merged

Fully sort polymorphic inductives #18331

merged 10 commits into from
Nov 29, 2023

Conversation

SkySkimmer
Copy link
Contributor
@SkySkimmer SkySkimmer commented Nov 17, 2023 •
edited
Loading

@SkySkimmer SkySkimmer added needs: documentation Documentation was not added or updated. request: full CI Use this label when you want your next push to trigger a full CI. labels Nov 17, 2023
@SkySkimmer SkySkimmer added this to the 8.19+rc1 milestone Nov 17, 2023
@SkySkimmer SkySkimmer requested review from a team as code owners November 17, 2023 16:55
@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 Nov 17, 2023
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Nov 17, 2023
@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 Nov 17, 2023
@SkySkimmer SkySkimmer added the needs: overlay This is breaking external developments we track in CI. label Nov 19, 2023
SkySkimmer added a commit to SkySkimmer/coq-elpi that referenced this pull request Nov 20, 2023
@SkySkimmer
Adapt to rocq-prover/rocq#18331 (mind_kelim -> mind_squashed)
131853c
SkySkimmer added a commit to rocq-community/rocq-lean-import that referenced this pull request Nov 20, 2023
@SkySkimmer
Adapt to rocq-prover/rocq#18331 (mind_kelim -> mind_squashed)
98b5e34
SkySkimmer added a commit to SkySkimmer/MetaRocq that referenced this pull request Nov 20, 2023
@SkySkimmer
Adapt to rocq-prover/rocq#18331 (mind_kelim -> mind_squashed)
8d6c1cc
@SkySkimmer SkySkimmer added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: documentation Documentation was not added or updated. needs: overlay This is breaking external developments we track in CI. labels Nov 20, 2023
@SkySkimmer SkySkimmer requested a review from a team as a code owner November 20, 2023 14:55
@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 Nov 20, 2023
@SkySkimmer SkySkimmer added the needs: merge of dependency This PR depends on another PR being merged first. label Nov 20, 2023
@jfehrle jfehrle added the needs: changelog entry This should be documented in doc/changelog. label Nov 21, 2023
@SkySkimmer SkySkimmer removed the needs: changelog entry This should be documented in doc/changelog. label Nov 21, 2023
@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 Nov 21, 2023
@ppedrot ppedrot self-assigned this Nov 22, 2023
@SkySkimmer SkySkimmer removed the needs: merge of dependency This PR depends on another PR being merged first. label Nov 23, 2023
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Nov 24, 2023
@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 Nov 24, 2023
ppedrot
ppedrot reviewed Nov 24, 2023
View reviewed changes
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Nov 24, 2023
@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 Nov 24, 2023
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Nov 24, 2023
@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 Nov 24, 2023
@SkySkimmer SkySkimmer added needs: fixing The proposed code change is broken. needs: overlay This is breaking external developments we track in CI. labels Nov 27, 2023
SkySkimmer added a commit to SkySkimmer/coq-serapi that referenced this pull request Nov 27, 2023
@SkySkimmer
Adapt to rocq-prover/rocq#18331 (sort poly inductives)
b3b3d8b
@SkySkimmer SkySkimmer added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: fixing The proposed code change is broken. needs: overlay This is breaking external developments we track in CI. labels Nov 27, 2023
@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 Nov 27, 2023
@ppedrot
Copy link
Member
ppedrot commented Nov 29, 2023

@coqbot merge now

@coqbot-app coqbot-app bot merged commit d98e511 into rocq-prover:master Nov 29, 2023
@coqbot-app coqbot-app
Copy link
Contributor
coqbot-app bot commented Nov 29, 2023

@ppedrot: Please take care of the following overlays:

  • 18331-SkySkimmer-sort-poly-ind.sh

ppedrot added a commit to LPCIC/coq-elpi that referenced this pull request Nov 29, 2023
@ppedrot
Merge pull request #548 from SkySkimmer/sort-poly-ind
d85ca2d 
Adapt to rocq-prover/rocq#18331 (mind_kelim -> mind_squashed)
ppedrot added a commit to MetaRocq/metarocq that referenced this pull request Nov 29, 2023
@ppedrot
Merge pull request #1015 from SkySkimmer/sort-poly-ind
194116d 
Adapt to rocq-prover/rocq#18331 (mind_kelim -> mind_squashed)
ppedrot added a commit to rocq-archive/coq-serapi that referenced this pull request Nov 29, 2023
@ppedrot
Merge pull request #374 from SkySkimmer/sort-poly-ind
5174bf6 
Adapt to rocq-prover/rocq#18331 (sort poly inductives)
@SkySkimmer SkySkimmer deleted the sort-poly-ind branch December 4, 2023 12:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tabareau tabareau tabareau left review comments

@ppedrot ppedrot ppedrot approved these changes

Assignees

@ppedrot ppedrot

Labels
kind: feature New user-facing feature request or implementation. part: kernel
Projects
None yet
Milestone
8.19+rc1
Development

Successfully merging this pull request may close these issues.
4 participants
@SkySkimmer @ppedrot @tabareau @jfehrle
0