From c039f7edaaa1a80d77ee8926cf73299405d4c92e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Tue, 17 Dec 2024 15:10:11 +0100
Subject: [PATCH] Remove warning "overwriting-delimiting-key"

The delimiter is in fact not overwritten for parsing (ie both the old
and new delimiters are accepted), it is only replaced for printing.
IMO this means it's not worth warning about.
---
 interp/notation.ml                 |  8 +-------
 test-suite/output/DelimitScope.out |  8 ++++++++
 test-suite/output/DelimitScope.v   | 13 +++++++++++++
 theories/ssr/ssrbool.v             |  2 --
 4 files changed, 22 insertions(+), 9 deletions(-)
 create mode 100644 test-suite/output/DelimitScope.out
 create mode 100644 test-suite/output/DelimitScope.v

diff --git a/interp/notation.ml b/interp/notation.ml
index 964b586533b5e..3bc21494ef6aa 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -224,9 +224,6 @@ let warn_scope_delimiter_start_ =
     ~default:CWarnings.AsError
     (fun () -> strbrk "Scope delimiters should not start with an underscore.")
 
-let warn_overwriting_key = CWarnings.create ~name:"overwriting-delimiting-key" ~category:CWarnings.CoreCategories.parsing
-    Pp.(fun (oldkey,scope) -> str "Overwriting previous delimiting key " ++ str oldkey ++ str " in scope " ++ str scope)
-
 let warn_hiding_key =  CWarnings.create ~name:"hiding-delimiting-key" ~category:CWarnings.CoreCategories.parsing
     Pp.(fun (key,oldscope) -> str "Hiding binding of key " ++ str key ++ str " to " ++ str oldscope)
 
@@ -237,10 +234,7 @@ let declare_delimiters scope key =
   begin match sc.delimiters with
     | None -> scope_map := String.Map.add scope newsc !scope_map
     | Some oldkey when String.equal oldkey key -> ()
-    | Some oldkey ->
-      (* FIXME: implement multikey scopes? *)
-      warn_overwriting_key (oldkey,scope);
-      scope_map := String.Map.add scope newsc !scope_map
+    | Some oldkey -> scope_map := String.Map.add scope newsc !scope_map
   end;
   try
     let oldscope = String.Map.find key !delimiters_map in
diff --git a/test-suite/output/DelimitScope.out b/test-suite/output/DelimitScope.out
new file mode 100644
index 0000000000000..16320fc346cc3
--- /dev/null
+++ b/test-suite/output/DelimitScope.out
@@ -0,0 +1,8 @@
+(~~ false)%bool
+     : bool
+(~~ false)%B
+     : bool
+(~~ false)%B
+     : bool
+(~~ false)%B
+     : bool
diff --git a/test-suite/output/DelimitScope.v b/test-suite/output/DelimitScope.v
new file mode 100644
index 0000000000000..75a1e0b36297f
--- /dev/null
+++ b/test-suite/output/DelimitScope.v
@@ -0,0 +1,13 @@
+Reserved Notation "~~ b" (at level 35, right associativity).
+
+Notation "~~ b" := (negb b) : bool_scope.
+
+Check negb false.
+
+Delimit Scope bool_scope with B.
+
+Check negb false.
+
+(* %bool still works even if not used by printing *)
+Check (~~ false)%bool.
+Check (~~ false)%B.
diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v
index eded2b05701be..4c88cdbb90b19 100644
--- a/theories/ssr/ssrbool.v
+++ b/theories/ssr/ssrbool.v
@@ -465,9 +465,7 @@ Reserved Notation "[ ==> b1 , b2 , .. , bn => c ]" (at level 0, format
   "'[hv' [ ==> '['  b1 , '/'  b2 , '/'  .. , '/'  bn ']' '/'  =>  c ] ']'").
 
 (**  Shorter delimiter  **)
-#[export] Set Warnings "-overwriting-delimiting-key".
 Delimit Scope bool_scope with B.
-#[export] Set Warnings "overwriting-delimiting-key".
 Open Scope bool_scope.
 
 (**  An alternative to xorb that behaves somewhat better wrt simplification. **)