diff options
| -rw-r--r-- | interp/notation.ml | 32 | ||||
| -rw-r--r-- | test-suite/bugs/closed/7462.v | 6 |
2 files changed, 21 insertions, 17 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 4a6d2a154..76d0efb72 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -49,7 +49,6 @@ type notation_location = (DirPath.t * DirPath.t) * string type notation_data = { not_interp : interpretation; not_location : notation_location; - not_onlyprinting : bool; } type scope = { @@ -449,20 +448,21 @@ let warn_notation_overridden = let declare_notation_interpretation ntn scopt pat df ~onlyprint = let scope = match scopt with Some s -> s | None -> default_scope in let sc = find_scope scope in - let () = - if String.Map.mem ntn sc.notations then - let which_scope = match scopt with - | None -> mt () - | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in - warn_notation_overridden (ntn,which_scope) - in - let notdata = { - not_interp = pat; - not_location = df; - not_onlyprinting = onlyprint; - } in - let sc = { sc with notations = String.Map.add ntn notdata sc.notations } in - let () = scope_map := String.Map.add scope sc !scope_map in + if not onlyprint then begin + let () = + if String.Map.mem ntn sc.notations then + let which_scope = match scopt with + | None -> mt () + | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in + warn_notation_overridden (ntn,which_scope) + in + let notdata = { + not_interp = pat; + not_location = df; + } in + let sc = { sc with notations = String.Map.add ntn notdata sc.notations } in + scope_map := String.Map.add scope sc !scope_map + end; begin match scopt with | None -> scope_stack := SingleNotation ntn :: !scope_stack | Some _ -> () @@ -487,7 +487,6 @@ let rec find_interpretation ntn find = function let find_notation ntn sc = let n = String.Map.find ntn (find_scope sc).notations in - let () = if n.not_onlyprinting then raise Not_found in (n.not_interp, n.not_location) let notation_of_prim_token = function @@ -631,7 +630,6 @@ let exists_notation_in_scope scopt ntn onlyprint r = try let sc = String.Map.find scope !scope_map in let n = String.Map.find ntn sc.notations in - onlyprint = n.not_onlyprinting && interpretation_eq n.not_interp r with Not_found -> false diff --git a/test-suite/bugs/closed/7462.v b/test-suite/bugs/closed/7462.v new file mode 100644 index 000000000..37af64caa --- /dev/null +++ b/test-suite/bugs/closed/7462.v @@ -0,0 +1,6 @@ +(* Adding an only-printing notation should not override existing + interpretations for the same notation. *) + +Notation "$ x" := (@id nat x) (only parsing, at level 0). +Notation "$ x" := (@id bool x) (only printing, at level 0). +Check $1. (* Was: Error: Unknown interpretation for notation "$ _". *) |