Suppressing Repeated Warnings from "Disable Notation" Command in Coq

Using Coq
1

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:

  1. I attempted to close the scope of that notation within Coquelicot, but it does not define a scope.
  2. 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.
  3. 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?

1 Like
2

Try not importing ListNotations before Coquelicot.

Require Import List.
From Coquelicot Require Import Coquelicot.
Import ListNotations.
Check [1].
3

Thank you for the solution; it works.

However, I will be importing the Coquelicot library in a module named Math, which will be used by other developers. They might not be aware of the Notation issue and could write the import order as:

Import ListNotations. 
Import Math.

which would still result in problems. I’m not sure if there’s another way around this issue.

4

Maybe ask the maintainers of coquelicot whether they would consider using notation scopes, or whether they have a better solution.

2 Likes
5

Yes, I agree with this idea too.