Fixes part 1 of #7462 (only-printing not to override existing interp rule).

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 "$ _". *)