Conflicting use of "~=" in Coq.Program.Equality and Coq.Structures.Equalities

[imaxw]

Description of the problem

The Coq.Structures.Equalities library file declares the ~= notation (in the empty scope) to mean inequivalence according to some equivalence relation:

Module Type EqNotation (Import E:Eq).
  Infix "==" := eq (at level 70, no associativity).
  Notation "x ~= y" := (~eq x y) (at level 70, no associativity).
End EqNotation.

The Coq.Program.Equality library file, however, declares it to mean heterogeneous-type equality:

Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity).

This is not exactly a bug but leads to annoying redefinition warnings when including EqNotation in a module where the Equality library is imported.

Since most projects importing Coq.Program.Equality are probably doing so for access to its tactics, and not making use of the declared ~= notation, it is probably unnecessary to export that notation at all. I cannot find any actual uses of it within the standard library, so simply deleting the notation from Coq.Program.Equality is probably an acceptable solution. If in fact it is being used, another solution would be to declare it in type_scope or program_scope rather than the empty scope. However, it is in any case probably bad practice to use the same notation for equality in one setting and inequality in another, so probably some change should be made to one or the other of these declarations.

Coq Version

The Coq Proof Assistant, version 8.15.2
compiled with OCaml 4.13.1