Stream: Coq users

Topic: ✔ Silencing notation-overriden warning


view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Jan 09 2023 at 12:14):

Export Set Warning around the notation

view this post on Zulip Notification Bot (Jan 09 2023 at 13:43):

Meven Lennon-Bertrand has marked this topic as resolved.


Last updated: Mar 29 2024 at 01:40 UTC