Add a nonuniform attribute silencing warning on coercions#15853
Add a nonuniform attribute silencing warning on coercions#15853coqbot-app[bot] merged 2 commits intorocq-prover:masterfrom
Conversation
proux01
added
kind: enhancement
proux01
force-pushed
the
nonuniform_attr
branch
from
5115e65 to
cfc6f87
Compare
proux01
force-pushed
the
nonuniform_attr
branch
from
cfc6f87 to
85c561c
Compare
jfehrle
left a comment
jfehrle
left a comment
There was a problem hiding this comment.
A couple suggestions but looks good.
proux01
force-pushed
the
nonuniform_attr
branch
from
5e569b8 to
bf0fd68
Compare
proux01
force-pushed
the
nonuniform_attr
branch
from
bf0fd68 to
145f27d
Compare
|
This is looking for an assignee, maybe @ana-borges since you somewhat requested the feature? (I don't think you have push rights, but maybe we can ask) |
The #[nonuniform] boolean attribute helps silencing the non-uniform-inheritance warning on coercions when the user needs to declare such a coercion on purpose. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
Sure! Indeed I don't think I have the rights to merge, unless that comes with being a member of the Coq organization, which I already am. |
|
Let's ask @Zimmi48 , I think you should have a look to the maintainer teams: https://github.com/orgs/coq/teams/contributors/teams |
|
I guess the bedrock2 failure is unrelated. @SkySkimmer are you done reviewing? |
|
yes |
|
@coqbot: merge now |
|
@ana-borges: You can't merge the PR because it hasn't been approved yet. |
|
Right, so @SkySkimmer can you please approve? |
|
Why not do it yourself? |
|
Seemed to make more sense for the person who actually reviewed to approve and I didn't want to overstep. Consider my notion of the reviewing culture duly updated. |
|
@coqbot: merge now |
|
@ana-borges: Please take care of the following overlays:
|
|
I didn't review in depth, I just had a look. |
355: Adapt to rocq-prover/rocq#15853 r=proux01 a=proux01 To be merged synchronously with the upstream PR rocq-prover/rocq#15853 Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
|
Thanks everybody! |
This depends on coq v8.16 and is not usable on lower versions. Relevant issues and PRs from the coq repo: rocq-prover/rocq#15789, rocq-prover/rocq#15853, rocq-prover/rocq#4593, rocq-prover/rocq#3115
This depends on coq v8.16 and is not usable on lower versions. Relevant issues and PRs from the coq repo: rocq-prover/rocq#15789, rocq-prover/rocq#15853, rocq-prover/rocq#4593, rocq-prover/rocq#3115
4 participants
This is a follow up of #15789 implementing a comment of @CohenCyril on Zulip: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Identity.20Coercions/near/276371166
The #[nonuniform] boolean attribute helps silencing the non-uniform-inheritance warning on coercions when the user needs to declare such a coercion on purpose.
Overlays (to be merged synchronously with the PR)