aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-05-10 14:57:00 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-05-10 15:19:06 +0200
commitdfa99b152114271cf9fac4cab9d8663ac6ec078c (patch)
tree80e8af6b339a263580cf1ad4c70c0e3269b4f89c
parente559f7553030dc3a86936794d0f80f39b0131960 (diff)
Fixes part 1 of #7462 (only-printing not to override existing interp rule).
-rw-r--r--interp/notation.ml32
-rw-r--r--test-suite/bugs/closed/7462.v6
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 "$ _". *)