Wish: attributes to disable warnings

[ana-borges]

Sometimes the desired way to deal with a warning is to locally disable it. This is particularly obvious for the several warnings generated by importing MathComp, but it is also true in other circumstances, such as overriding notations, declaring nonuniform coercions that don't have a uniform version, declaring a coercion that leads to ambiguous paths we don't care about, etc.

There is already a way to deal with this, which is to disable and enable the warnings surrounding the problematic lines:

Set Warnings "-notation-overridden, -ambiguous-paths".
From mathcomp Require Import all_ssreflect.
Set Warnings "notation-overridden, ambiguous-paths".

However, it would be nicer if there were attributes for disabling each warning (or a sensible subset of the warnings), such as the nonuniform one implemented recently in #15853.

[Zimmi48]

I support this feature request, but what I would recommend is a generic attribute that can be used to disable locally any warning specified by its name or category.

[Zimmi48]

On the other hand, having specific attributes for commands where we expect a warning that makes sense to disable, like in #15853, also makes sense.