Skip to content

Conversation

SkySkimmer added 2 commits May 6, 2025 14:17
Subflags like coercion locality are only present when the projection
is to be declared as a projection.

Get rid of `check_priorities` as something like

~~~coq
Class x0 (n:nat) := {}.
Record foo := { x1 : nat; baz :: x0 x1 | 3 }.
~~~

does not need to error.
@SkySkimmer SkySkimmer requested a review from a team as a code owner May 6, 2025 12:31
@SkySkimmer SkySkimmer added kind: cleanup Code removal, deprecation, refactorings, etc. kind: internal API, ML documentation... labels May 6, 2025
@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 6, 2025
SkySkimmer added a commit to SkySkimmer/coq-elpi that referenced this pull request May 6, 2025
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label May 6, 2025
@coqbot-app coqbot-app bot removed 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 May 6, 2025
@SkySkimmer SkySkimmer added the needs: overlay This is breaking external developments we track in CI. label May 6, 2025
SkySkimmer added a commit to SkySkimmer/MetaRocq that referenced this pull request May 6, 2025
SkySkimmer added a commit to SkySkimmer/rocq-lean-import that referenced this pull request May 6, 2025
SkySkimmer added a commit to SkySkimmer/coq-lsp that referenced this pull request May 6, 2025
@SkySkimmer SkySkimmer added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: overlay This is breaking external developments we track in CI. labels May 6, 2025
@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 May 6, 2025
ejgallego added a commit to ejgallego/rocq-lsp that referenced this pull request May 6, 2025
@ppedrot ppedrot self-assigned this May 13, 2025
@ppedrot ppedrot added this to the 9.1+rc1 milestone May 13, 2025
@ppedrot
Copy link
Member

ppedrot commented May 15, 2025

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 6492a2c into rocq-prover:master May 15, 2025
5 checks passed

This comment was marked as resolved.

ppedrot added a commit to MetaRocq/metarocq that referenced this pull request May 15, 2025
ppedrot added a commit to LPCIC/coq-elpi that referenced this pull request May 15, 2025
SkySkimmer added a commit to rocq-community/rocq-lean-import that referenced this pull request May 15, 2025
@SkySkimmer SkySkimmer deleted the simpl-proj-flags branch May 15, 2025 10:57
@andres-erbsen
Copy link
Contributor

andres-erbsen commented May 17, 2025

stdlib CI for metarocq is failing with the error introduced in this commit https://github.com/rocq-prover/stdlib/actions/runs/15085835936/job/42408257533?pr=144#step:11:3672

@SkySkimmer
Copy link
Contributor Author

The error is correct

@andres-erbsen
Copy link
Contributor

andres-erbsen commented May 17, 2025

In what sense is the error correct? Are you saying it was always there, or should have been? I am asking because this is a kind:cleanup kind:internal PR without a changelog, so having a non-plugin build that passed before fail now is not automatically expected.

@SkySkimmer
Copy link
Contributor Author

It should have been

@andres-erbsen
Copy link
Contributor

Makes sense. When you get a chance, could you please write changelog / porting guidance and point the metarocq maintainers to it. Thanks!

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. kind: internal API, ML documentation...

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants