canonical_names.v overwrites a lot of standard notation

[langston-barrett]

For instance = and +. This causes a ton of conflict, and has caused me to write stuff like this:

Require Import MathClasses.interfaces.canonical_names.
(* math-classes uses (=) to denote equivalence, but we will use it for equality *)
Infix "=" := eq : type_scope.
Notation "(=)" := eq (only parsing) : mc_scope.
Notation "( x =)" := (eq x) (only parsing) : mc_scope.
Notation "(= x )" := (λ y, eq y x) (only parsing) : mc_scope.

Could we perhaps separate this into two files, one that exports stuff compatible with standard notation, and one that doesn't?

[langston-barrett]

For a particularly glaring example, consider the following attempt to define Le on the natural numbers:

Instance Nat_Le : Le nat := le.

This fails with the following error:

Error: Unable to satisfy the following constraints:

?Le : "Le nat"

[spitters]

Sorry, it looks like I have been missing a lot of notifications.

In math-classes we defined our own natural numbers, so we overwrote the default notation. I would assume that most files would still use both of the files, so I am afraid it will be difficult to change this. However, I am happy to be proven wrong.