Background:

I am using the “Coquelicot/Hierarchy” library, which defines a notation for pairs as follows:

```
Notation "[ x1 , .. , xn ]" := (pair x1 .. (pair xn tt) .. ).
```

As a result, in the following codes,

```
Require Import List.
Import ListNotations.
From Coquelicot Require Import Coquelicot.
Check [1]. (* : nat * unit *)
Import ListNotations.
Check [1]. (* : nat * unit *)
```

the expression `[1]`

has the type `nat * unit`

.

However, I prefer to use list notations and expect to get a `list nat`

type.

Attempts and Issues:

- I attempted to close the scope of that notation within Coquelicot, but it does not define a scope.
- I used the
`Import ListNotations.`

command to bring the list notations to the top,

but it had no effect. The reason is same as last attempt. - In the end, I used the
`Disable Notation "[ x1 , .. , xn ]".`

command, which succeeded. However, this now results in a message:

```
The following notations have been disabled:
Notation "[ x1 , .. , xn ]" := (pair x1 .. (pair xn tt) ..)
```

This message is printed every time the current module is imported, either directly or indirectly. As a result, in a larger project, these messages are numerous and become annoying.

For example,

```
coq_makefile -f _CoqProject -o Makefile.coq
COQC testA.v
The following notations have been disabled:
Notation "[ x1 , .. , xn ]" := (pair x1 .. (pair xn tt) ..)
COQC testB.v
The following notations have been disabled:
Notation "[ x1 , .. , xn ]" := (pair x1 .. (pair xn tt) ..)
COQC testC.v
The following notations have been disabled:
Notation "[ x1 , .. , xn ]" := (pair x1 .. (pair xn tt) ..)
The following notations have been disabled:
Notation "[ x1 , .. , xn ]" := (pair x1 .. (pair xn tt) ..)
COQC testE.v
The following notations have been disabled:
Notation "[ x1 , .. , xn ]" := (pair x1 .. (pair xn tt) ..)
```

Question:

How can I suppress the repeated warning messages generated by the “Disable Notation …” command?