Skip to content

Commit

Permalink
Remove warning "overwriting-delimiting-key"
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
SkySkimmer committed Dec 17, 2024
1 parent 8e6284f commit c039f7e
Show file tree
Hide file tree
Showing 4 changed files with 22 additions and 9 deletions.
8 changes: 1 addition & 7 deletions interp/notation.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand All @@ -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
Expand Down
8 changes: 8 additions & 0 deletions test-suite/output/DelimitScope.out
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
(~~ false)%bool
: bool
(~~ false)%B
: bool
(~~ false)%B
: bool
(~~ false)%B
: bool
13 changes: 13 additions & 0 deletions test-suite/output/DelimitScope.v
Original file line number Diff line number Diff line change
@@ -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.
2 changes: 0 additions & 2 deletions theories/ssr/ssrbool.v
Original file line number Diff line number Diff line change
Expand Up @@ -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. **)
Expand Down

0 comments on commit c039f7e

Please sign in to comment.