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/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. **)