Meven Lennon-Bertrand (Jan 09 2023 at 12:07): Meven Lennon-Bertrand (Jan 09 2023 at 12:07):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?
Gaëtan Gilbert (Jan 09 2023 at 12:14):Export Set Warning around the notation
Notification Bot (Jan 09 2023 at 13:43):Meven Lennon-Bertrand has marked this topic as resolved.
Last updated: Oct 04 2023 at 21:01 UTC