"Print" works for some notations but not all.

[RalfJung]

Description of the problem

I recently noticed that Print "=" works and prints eq, but Print "<>" does not work and just says

Unable to interpret "<>" as a reference.

Why can some notations be printed and others not? Is this a bug or somehow intended?

Coq Version

8.16.1

[SkySkimmer]

It works when the notation is basically just the reference (cf

coq/interp/notation.ml

Line 2364 in 41944f5

let global_reference_of_notation ~head test (ntn,sc,(on_parsing,on_printing,{not_interp = (_,c)})) =

).
In the case of "x = y" := (@eq _ x y) this is the case but for "x <> y" := (not (@eq _ x y)) it's not.

[RalfJung]

Oh I see... Print "<>" would have to print not and eq somehow but it's only supposed to print one thing. Yeah that makes sense, thanks!

[herbelin]

Maybe the message should be improved?

[RalfJung]

Yeah that would be a good idea.

[herbelin]

Unable to non-ambiguously interpret "<>" as a reference. ??

(At the same time, we should take some time to rethink the articulation between Print, Check and About. There was an issue about it but I don't find it again. It would also be possible to give a positive answer on Print "<>", say Notation "x <> y" := (not (eq x y)).)

[RalfJung]

Those 3 I actually see as fairly different, but Print and Locate have a lot of overlap... also see #18097.

Unable to non-ambiguously interpret "<>" as a reference. ??

What about something like

Unable to non-ambiguously interpret "<>" as a reference; found:
Notation "x <> y" := (not (eq x y)).

[herbelin]

OK, adopted, made #18104.