# Annoying warnings when Requiring/Importing ssreflect

**URL:** <https://discourse.rocq-prover.org/t/annoying-warnings-when-requiring-importing-ssreflect/1611>\
**Category:** Using Rocq\
**Tags:** notation\
**Created:** [March 28, 2022, 6:25am UTC](https://discourse.rocq-prover.org/t/annoying-warnings-when-requiring-importing-ssreflect/1611 "2022-03-28T06:25:05Z")\
**Posts on this page:** 5\
**Page:** 1

<div class="post-metadata">

**Author:** ![nobrowser](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/nobrowser/32/300_2.png) [@nobrowser](https://discourse.rocq-prover.org/u/nobrowser)\
**Post date:** [March 28, 2022, 6:25am UTC](https://discourse.rocq-prover.org/t/annoying-warnings-when-requiring-importing-ssreflect/1611/1 "2022-03-28T06:25:05Z")

</div>

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:

```auto
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:

```auto
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?

---

<div class="post-metadata">

**Author:** ![ana-borges](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ana-borges/32/645_2.png) [@ana-borges](https://discourse.rocq-prover.org/u/ana-borges)\
**Post date:** [March 28, 2022, 10:09am UTC](https://discourse.rocq-prover.org/t/annoying-warnings-when-requiring-importing-ssreflect/1611/2 "2022-03-28T10:09:25Z")

</div>

In Coq 8.14 this doesn’t show me any warnings, while in 8.15 the following appears:

```auto
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:

```auto
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

```auto
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](https://github.com/math-comp/math-comp/issues/90) about it, but it’s quite stale at this point.

---

<div class="post-metadata">

**Author:** ![Blaisorblade](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/blaisorblade/32/56_2.png) [@Blaisorblade](https://discourse.rocq-prover.org/u/Blaisorblade)\
**Post date:** [March 28, 2022, 10:37am UTC](https://discourse.rocq-prover.org/t/annoying-warnings-when-requiring-importing-ssreflect/1611/3 "2022-03-28T10:37:03Z")

</div>

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`.

```auto
Set Warnings "-notation-overridden".
From mathcomp Require Import ssreflect ssrfun ssrbool.
Set Warnings "notation-overridden".

```

To support both versions, apparently you can use both:

```auto
Set Warnings "-notation-overridden, -notation-overriden".
From mathcomp Require Import ssreflect ssrfun ssrbool.
Set Warnings "notation-overridden, notation-overriden".

```

---

<div class="post-metadata">

**Author:** ![ana-borges](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ana-borges/32/645_2.png) [@ana-borges](https://discourse.rocq-prover.org/u/ana-borges)\
**Post date:** [March 28, 2022, 1:53pm UTC](https://discourse.rocq-prover.org/t/annoying-warnings-when-requiring-importing-ssreflect/1611/4 "2022-03-28T13:53:58Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![nobrowser](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/nobrowser/32/300_2.png) [@nobrowser](https://discourse.rocq-prover.org/u/nobrowser)\
**Post date:** [March 28, 2022, 3:55pm UTC](https://discourse.rocq-prover.org/t/annoying-warnings-when-requiring-importing-ssreflect/1611/5 "2022-03-28T15:55:30Z")

</div>

Bingo, that was embarassing. Thanks, Ana.