Deprecate the nonuniform attribute#17716
Merged
coqbot-app[bot] merged 2 commits intorocq-prover:masterfrom Jun 15, 2023
Merged
Conversation
coqbot-app
bot
added
the
needs: full CI
Alizter
reviewed
Jun 9, 2023
proux01
force-pushed
the
deprecate_nonuniform
branch
from
d62a7b6 to
b0fcc20
Compare
Contributor
|
You could make |
Now subsumed byt the #[warning="-uniform-inheritance"] attribute introduced in rocq-prover#16902 .
proux01
force-pushed
the
deprecate_nonuniform
branch
from
b0fcc20 to
c68837b
Compare
Contributor
Author
I see, you want me to write the overlays now ;) but you're right, let's do that. |
proux01
added a commit
to proux01/coq-elpi
that referenced
this pull request
Jun 9, 2023
proux01
added a commit
to proux01/Mtac2
that referenced
this pull request
Jun 9, 2023
Contributor
Author
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
Member
|
I take it |
Contributor
Author
Yes, it's the name of the warning the attribute |
proux01
added a commit
to proux01/coq-elpi
that referenced
this pull request
Jun 10, 2023
Contributor
Author
|
CI green |
proux01
added
kind: cleanup
Contributor
Author
|
@Alizter would you be the assignee? this is ready |
Alizter
approved these changes
Jun 15, 2023
Contributor
|
@coqbot merge now |
Contributor
|
@Alizter: Please take care of the following overlays:
|
bors bot
added a commit
to Mtac2/Mtac2
that referenced
this pull request
Jun 15, 2023
388: Adapt to rocq-prover/rocq#17716 r=Janno a=proux01 Adapt to rocq-prover/rocq#17716 To be merged in sync with the upstream PR. Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
bors bot
added a commit
to Mtac2/Mtac2
that referenced
this pull request
Jun 15, 2023
388: Adapt to rocq-prover/rocq#17716 r=proux01 a=proux01 Adapt to rocq-prover/rocq#17716 To be merged in sync with the upstream PR. Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
bors bot
added a commit
to Mtac2/Mtac2
that referenced
this pull request
Jun 15, 2023
388: Adapt to rocq-prover/rocq#17716 r=proux01 a=proux01 Adapt to rocq-prover/rocq#17716 To be merged in sync with the upstream PR. Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
gares
added a commit
to LPCIC/coq-elpi
that referenced
this pull request
Jun 15, 2023
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Now subsumed byt the #[warning="-uniform-inheritance"] attribute introduced in #16902 .
Following a remark from @Alizter in #17713
Documented any new / changed user messages.Updated documented syntax by runningmake doc_gram_rsts.Overlays