From 9718eaf4aac92516b80373655a28e608b3786593 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Fri, 20 Jun 2025 16:39:04 +0200
Subject: [PATCH] Adapt to https://github.com/rocq-prover/rocq/pull/17876

Don't rereserve notation already reserved in Corelib
---
 Kami/Lib/Word.v | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/Kami/Lib/Word.v b/Kami/Lib/Word.v
index b925671..5aa3d66 100644
--- a/Kami/Lib/Word.v
+++ b/Kami/Lib/Word.v
@@ -235,10 +235,8 @@ Definition wremN := wordBinN Nat.modulo.
 
 Definition wminusN sz (x y : word sz) : word sz := wplusN x (wnegN y).
 
-Notation "w ~ 1" := (WS true w)
- (at level 7, left associativity, format "w '~' '1'") : word_scope.
-Notation "w ~ 0" := (WS false w)
- (at level 7, left associativity, format "w '~' '0'") : word_scope.
+Notation "w ~ 1" := (WS true w) : word_scope.
+Notation "w ~ 0" := (WS false w) : word_scope.
 
 Notation "^~" := wneg.
 Notation "l ^+ r" := (@wplus _ l%word r%word) (at level 50, left associativity).