Coq.Structures.Orders.LebNotation defines notations at levels incompatible with the rest of the standard library

[JasonGross]

Consider:

coq/theories/Structures/Orders.v

Lines 194 to 200 in b079040

	Module Type LebNotation (T:Typ)(E:HasLeb T).
	Infix "<=?" := E.leb (at level 35).
	End LebNotation.
	Module Type LtbNotation (T:Typ)(E:HasLtb T).
	Infix "<?" := E.ltb (at level 35).
	End LtbNotation.

$ git grep "<=\??" | grep level
theories/Arith/PeanoNat.v:Infix "<=?" := Nat.leb (at level 70) : nat_scope.
theories/Arith/PeanoNat.v:Infix "<?" := Nat.ltb (at level 70) : nat_scope.
theories/Init/Nat.v:Infix "<=?" := leb (at level 70) : nat_scope.
theories/Init/Nat.v:Infix "<?" := ltb (at level 70) : nat_scope.
theories/NArith/BinNat.v:Infix "<=?" := N.leb (at level 70, no associativity) : N_scope.
theories/NArith/BinNat.v:Infix "<?" := N.ltb (at level 70, no associativity) : N_scope.
theories/NArith/BinNatDef.v:Infix "<=?" := leb (at level 70, no associativity) : N_scope.
theories/NArith/BinNatDef.v:Infix "<?" := ltb (at level 70, no associativity) : N_scope.
theories/Numbers/Natural/Peano/NPeano.v:Infix "<=?" := Nat.leb (at level 70) : nat_scope.
theories/Numbers/Natural/Peano/NPeano.v:Infix "<?" := Nat.ltb (at level 70) : nat_scope.
theories/PArith/BinPos.v:Infix "<=?" := Pos.leb (at level 70, no associativity) : positive_scope.
theories/PArith/BinPos.v:Infix "<?" := Pos.ltb (at level 70, no associativity) : positive_scope.
theories/PArith/BinPosDef.v:Infix "<=?" := leb (at level 70, no associativity) : positive_scope.
theories/PArith/BinPosDef.v:Infix "<?" := ltb (at level 70, no associativity) : positive_scope.
theories/Sorting/Mergesort.v:  Infix "<=?" := leb (at level 35).
theories/Structures/Orders.v: Infix "<=?" := E.leb (at level 35).
theories/Structures/Orders.v: Infix "<?" := E.ltb (at level 35).
theories/ZArith/BinInt.v:Infix "<=?" := Z.leb (at level 70, no associativity) : Z_scope.
theories/ZArith/BinInt.v:Infix "<?" := Z.ltb (at level 70, no associativity) : Z_scope.
theories/ZArith/BinIntDef.v:Infix "<=?" := leb (at level 70, no associativity) : Z_scope.
theories/ZArith/BinIntDef.v:Infix "<?" := ltb (at level 70, no associativity) : Z_scope.

[JasonGross]

Here is a small test case:

Require Import Coq.Structures.Orders Coq.ZArith.ZArith.
(* Note that this has always worked fine without the '; we are testing importing notations from the stdlib here *)
Declare Module A : LeBool'.
Declare Module B : LtBool'.
Import A B.
(*
Error: Notation "_ <=? _" is already defined at level 70 with arguments constr
at next level, constr at next level while it is now required to be at level 35
with arguments constr at next level, constr at next level.
*)