Merge PR coq#19946: Remove warning "overwriting-delimiting-key"

Reviewed-by: proux01 Co-authored-by: proux01 <proux01@users.noreply.github.com>
SkySkimmer · Dec 18, 2024 · 4feee16 · 4feee16
2 parents eafed8f + f2e74ad
commit 4feee16
Show file tree

Hide file tree

Showing 8 changed files with 23 additions and 31 deletions.
diff --git 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/stdlib/test-suite/micromega/bug_14054.v b/stdlib/test-suite/micromega/bug_14054.v
@@ -10,7 +10,7 @@ From Stdlib.Init Require Byte.
 From Stdlib.Strings Require Byte.
 From Stdlib Require Import ZifyClasses Lia.
 
-Notation byte := Stdlib.Init.Byte.byte.
+Notation byte := Corelib.Init.Byte.byte.
 
 Module byte.
   Definition unsigned(b: byte): Z := Z.of_N (Byte.to_N b).

diff --git a/stdlib/test-suite/output/Sint63NumberSyntax.out b/stdlib/test-suite/output/Sint63NumberSyntax.out
@@ -56,15 +56,9 @@ Cannot interpret this number as a value of type int
      : nat
 2%sint63
      : int
-File "./output/Sint63NumberSyntax.v", line 34, characters 0-37:
-Warning: Overwriting previous delimiting key sint63 in scope sint63_scope
-[overwriting-delimiting-key,parsing,default]
 t = 2%si63
      : int
 File "./output/Sint63NumberSyntax.v", line 37, characters 0-36:
-Warning: Overwriting previous delimiting key nat in scope nat_scope
-[overwriting-delimiting-key,parsing,default]
-File "./output/Sint63NumberSyntax.v", line 37, characters 0-36:
 Warning: Hiding binding of key sint63 to sint63_scope
 [hiding-delimiting-key,parsing,default]
 t = 2%si63
@@ -74,9 +68,6 @@ t = 2%si63
 2
      : int
 File "./output/Sint63NumberSyntax.v", line 43, characters 0-39:
-Warning: Overwriting previous delimiting key si63 in scope sint63_scope
-[overwriting-delimiting-key,parsing,default]
-File "./output/Sint63NumberSyntax.v", line 43, characters 0-39:
 Warning: Hiding binding of key sint63 to nat_scope
 [hiding-delimiting-key,parsing,default]
 (2 + 2)%sint63

diff --git a/test-suite/output/DelimitScope.out 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
@@ -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/test-suite/output/FloatNumberSyntax.out b/test-suite/output/FloatNumberSyntax.out
@@ -78,15 +78,9 @@ neg_infinity
      : nat
 2%float
      : float
-File "./output/FloatNumberSyntax.v", line 47, characters 0-35:
-Warning: Overwriting previous delimiting key float in scope float_scope
-[overwriting-delimiting-key,parsing,default]
 t = 2%flt
      : float
 File "./output/FloatNumberSyntax.v", line 50, characters 0-35:
-Warning: Overwriting previous delimiting key nat in scope nat_scope
-[overwriting-delimiting-key,parsing,default]
-File "./output/FloatNumberSyntax.v", line 50, characters 0-35:
 Warning: Hiding binding of key float to float_scope
 [hiding-delimiting-key,parsing,default]
 t = 2%flt

diff --git a/test-suite/output/Int63NumberSyntax.out b/test-suite/output/Int63NumberSyntax.out
@@ -50,15 +50,9 @@ Overflow in int63 literal: 9223372036854775808.
      : nat
 2%uint63
      : int
-File "./output/Int63NumberSyntax.v", line 31, characters 0-37:
-Warning: Overwriting previous delimiting key uint63 in scope uint63_scope
-[overwriting-delimiting-key,parsing,default]
 t = 2%ui63
      : int
 File "./output/Int63NumberSyntax.v", line 34, characters 0-36:
-Warning: Overwriting previous delimiting key nat in scope nat_scope
-[overwriting-delimiting-key,parsing,default]
-File "./output/Int63NumberSyntax.v", line 34, characters 0-36:
 Warning: Hiding binding of key uint63 to uint63_scope
 [hiding-delimiting-key,parsing,default]
 t = 2%ui63

diff --git 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. **)