Merge PR coq#17920: ssrbool: reenable overwriting-delimiting-key

Reviewed-by: proux01 Co-authored-by: proux01 <[email protected]>
SkySkimmer · Dec 4, 2023 · 691049e · 691049e
2 parents ababbf4 + 5fe1563
commit 691049e
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v
@@ -15,8 +15,6 @@
 Require Bool.
 Require Import ssreflect ssrfun.
 
-#[export] Set Warnings "-overwriting-delimiting-key".
-
 (**
  A theory of boolean predicates and operators. A large part of this file is
  concerned with boolean reflection.
@@ -468,7 +466,9 @@ 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. **)