I use Ssreflect by including this line at the top of my .v files:
From mathcomp Require Import ssreflect ssrfun ssrbool.
When compiling my code I always get a bunch of warnings like this:
File "./Board_definitions.v", line 3, characters 0-54:
Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope.
I thought I could work around it by wrapping the import line like this:
Set Warnings "-notation-overriden".
From mathcomp Require Import ssreflect ssrfun ssrbool.
Set Warnings "+notation-overriden".
but it seems to have no effect, the warnings still happen. There has to be a way, right?
In Coq 8.14 this doesn’t show me any warnings, while in 8.15 the following appears:
Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope.
[notation-overridden,parsing]
So it seems this warning is now both a notation-overridden and parsing warning. Thus the following makes it disappear:
Set Warnings "-notation-overriden, -parsing".
From mathcomp Require Import ssrbool.
By the way, in order to set the warnings back, you might want to do
Set Warnings "notation-overriden, parsing".
instead (note the lack of +), as your version sets these messages as errors instead of warnings.
The warnings are truly annoying. There is an open issue about it, but it’s quite stale at this point.
You don’t need to disable all parsing warnings — you can use either category, as long as your spelling matches the one used by Coq. In 8.14 you need one d in overriden (which is misspelled), in 8.15 they fixed it so you need two ds, so overridden.
Set Warnings "-notation-overridden".
From mathcomp Require Import ssreflect ssrfun ssrbool.
Set Warnings "notation-overridden".
To support both versions, apparently you can use both:
Set Warnings "-notation-overridden, -notation-overriden".
From mathcomp Require Import ssreflect ssrfun ssrbool.
Set Warnings "notation-overridden, notation-overriden".
Wait, I think there was never any typo in the Coq repo. I accidentally tested the version with the typo on Coq 8.15 and the version without the typo on Coq 8.14. So probably the conclusion is that there was a typo in @nobrowser’s code and that’s why it didn’t work.
Bingo, that was embarassing. Thanks, Ana.