How is it possible that importing things in one order leads to a notation conflict, while importing in the other order does not? And how can I find out where that notation is defined?

```
From mathcomp Require Import ssreflect.
From VST Require Import floyd.proofauto.
(*
Notation "_ : _" is already defined at level 100 with arguments constr
at next level, constr at level 100 while it is now required to be at level 26
with arguments constr at next level, constr at level 26.
*)
```

```
From VST Require Import floyd.proofauto.
From mathcomp Require Import ssreflect.
(* OK *)
```

I think it is in ssreflect.v or ssrfun.v, both in coq (not mc, they are loaded transitively).

To avoid the conflict you should be explicit, since there are defaults which may be different from what the other notation declares. cc @Hugo Herbelin

Coq accepts the following sequence (and rejects the converse one). I have no idea if it is on purpose or a bug:

```
Notation "x @ y" := (x + y) (at level 26, only printing).
Reserved Notation "x @ y" (at level 100).
```

it seems `only printing`

is failing to skip the consistency check

but since it doesn't add the notation the next command can succeed

But should it actually succeed? It feels like it should not. Because once you do `Notation "x @ y" := (x - y).`

, things become crazy with respect to associativity and levels.

I agree that rejecting both orders seems simpler

or rather: it’s a bug, unless somebody can describe a compelling use-case for the more liberal alternative. “Fewer errors on imports of incompatible notations” does not qualify as “compelling” if the resulting grammar isn’t robust…

Enrico Tassi said:

To avoid the conflict you should be explicit, since there are defaults which may be different from what the other notation declares. cc Hugo Herbelin

This is discussed at #6078, #11088, #11657. There was a PR at #6134 but it did not reach the level of preserving compatibility everywhere. Somehow looking for someone courageous to find a solution which works at best...

Alternatives include:

- making progress on #12324 which mostly requires deciding a concrete user syntax for deactivating a notation
- moving the ssreflect notation to a submodule that is then loaded only optionally
- ...

Guillaume Melquiond said:

Coq accepts the following sequence (and rejects the converse one). I have no idea if it is on purpose or a bug:

`Notation "x @ y" := (x + y) (at level 26, only printing). Reserved Notation "x @ y" (at level 100).`

From memory, I would have said that both orders are accepted since #12950, so that an arbitrary number of printing notations can be given (under the responsability of the user). There might be a bug then.

Last updated: Dec 06 2023 at 14:01 UTC