I'd like to get rid of a `notation-overriden`

warning globally for one specific notation. (FTR, the notation in question is `~ P`

from the stdlib, that I want to map to `notT P`

rather than `not P`

, so that I can also negate `Type`

-level propositions). If I locally use `Set Warning "-notation-overriden"`

and `Set Warning "notation-overriden"`

around the culprit notation, I silence the warning there, but it still gets raised whenever I import that file. I saw that there is a shining, attribute based technique to do this in the latest Coq versions, but what is the way to do this in older (8.15) Coq versions?

Export Set Warning around the notation

Meven Lennon-Bertrand has marked this topic as resolved.

Last updated: Oct 04 2023 at 21:01 UTC