From f2e74ad014ff7131e546e0d67ecd20d6e046cc07 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= 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 +------- stdlib/test-suite/micromega/bug_14054.v | 2 +- stdlib/test-suite/output/Sint63NumberSyntax.out | 9 --------- test-suite/output/DelimitScope.out | 8 ++++++++ test-suite/output/DelimitScope.v | 13 +++++++++++++ test-suite/output/FloatNumberSyntax.out | 6 ------ test-suite/output/Int63NumberSyntax.out | 6 ------ theories/ssr/ssrbool.v | 2 -- 8 files changed, 23 insertions(+), 31 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 964b586533b5..3bc21494ef6a 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/stdlib/test-suite/micromega/bug_14054.v b/stdlib/test-suite/micromega/bug_14054.v index 18262c310768..5a051a881ba3 100644 --- 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 index 649927a13e57..79c3b04053c4 100644 --- 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 new file mode 100644 index 000000000000..16320fc346cc --- /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 000000000000..75a1e0b36297 --- /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/test-suite/output/FloatNumberSyntax.out b/test-suite/output/FloatNumberSyntax.out index 7f31c1685dd2..9e548b79f7e1 100644 --- 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 index 2c8f1f37fa9b..fedc62924bb2 100644 --- 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 index eded2b05701b..4c88cdbb90b1 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. **)