[Corelib] Adapt

Author: proux01

doc/changelog/11-corelib/17876-master+gramlib-support-for-non-assoc-and-non-recovery-Changed.rst

@@ -0,0 +1,5 @@
+- **Changed:**
+  Level of ``_~0`` and ``_~1`` reserved notations (used for positive
+  numbers) from level 7 to level 1
+  (`#17876 <https://github.com/rocq-prover/rocq/pull/17876>`_,
+  by Pierre Roux).

theories/Corelib/BinNums/PosDef.v

@@ -28,10 +28,8 @@ Local Open Scope positive_scope.
     for the number 6 (which is 110 in binary notation).
 *)
 
-Notation "p ~ 1" := (xI p)
- (at level 7, left associativity, format "p '~' '1'") : positive_scope.
-Notation "p ~ 0" := (xO p)
- (at level 7, left associativity, format "p '~' '0'") : positive_scope.
+Notation "p ~ 1" := (xI p) (format "p '~' '1'") : positive_scope.
+Notation "p ~ 0" := (xO p) (format "p '~' '0'") : positive_scope.
 
 Notation "1" := xH : positive_scope.
 Notation "2" := 1~0 : positive_scope.