Merge PR #12950: Notations: reworking the treatment of only-parsing and only-printing notations

Reviewed-by: SkySkimmer

18 files changed, 421 insertions, 191 deletions

diff --git a/doc/changelog/03-notations/12950-master+reorganization-notations-only-parsing-only-printing.rst b/doc/changelog/03-notations/12950-master+reorganization-notations-only-parsing-only-printing.rst
new file mode 100644
index 0000000000..16fc91f911
--- /dev/null
+++ b/doc/changelog/03-notations/12950-master+reorganization-notations-only-parsing-only-printing.rst
@@ -0,0 +1,10 @@
+- **Changed:**
+  New model for ``only parsing`` and ``only printing`` notations with
+  support for at most one parsing-and-printing or only-parsing
+  notation per notation and scope, but an arbitrary number of
+  only-printing notations
+  (`#12950 <https://github.com/coq/coq/pull/12950>`_,
+  fixes `#4738 <https://github.com/coq/coq/issues/4738>`_
+  and `#9682 <https://github.com/coq/coq/issues/9682>`_
+  and part 2 of `#12908 <https://github.com/coq/coq/issues/12908>`_,
+  by Hugo Herbelin).
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 5148fa84c9..d6db305300 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -57,15 +57,14 @@ to represent :g:`(and A B)`:
 Notations must be in double quotes, except when the
 abbreviation has the form of an ordinary applicative expression;
 see :ref:`Abbreviations`. The notation consists of *tokens* separated by
-spaces. Alphanumeric strings (such as ``A`` and ``B``) are the *parameters*
+spaces. Tokens which are identifiers (such as ``A``, ``x0'``, etc.) are the *parameters*
 of the notation. Each of them must occur at least once in the abbreviated term. The
 other elements of the string (such as ``/\``) are the *symbols*.
 
-Substrings enclosed in single quotes are treated as literals.  This is necessary
-for substrings that would otherwise be interpreted as :n:`@ident`\s.  Similarly,
-every symbol of at least 3 characters and starting with a simple quote
-must be quoted (then it starts by two single quotes). Here is an
-example.
+Identifiers enclosed in single quotes are treated as symbols and thus
+lose their role of parameters. In the same vein, every symbol of at
+least 3 characters and starting with a simple quote must be quoted
+(then it starts with two single quotes). Here is an example.
 
 .. coqtop:: in
 
@@ -82,7 +81,8 @@ associativity rules have to be given.
    The right-hand side of a notation is interpreted at the time the notation is
    given. In particular, disambiguation of constants, :ref:`implicit arguments
    <ImplicitArguments>` and other notations are resolved at the
-   time of the declaration of the notation.
+   time of the declaration of the notation. The right-hand side is
+   currently typed only at use time but this may change in the future.
 
 Precedences and associativity
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -299,12 +299,29 @@ Notations disappear when a section is closed. No typing of the denoted
 expression is performed at definition time. Type checking is done only
 at the time of use of the notation.
 
-.. note:: Sometimes, a notation is expected only for the parser. To do
-          so, the option ``only parsing`` is allowed in the list of :n:`@syntax_modifier`\s
-          in :cmd:`Notation`. Conversely, the ``only printing`` :n:`@syntax_modifier` can be
-          used to declare that a notation should only be used for printing and
-          should not declare a parsing rule. In particular, such notations do
-          not modify the parser.
+.. note::
+
+   The default for a notation is to be used both for parsing and
+   printing. It is possible to declare a notation only for parsing by
+   adding the option ``only parsing`` to the list of
+   :n:`@syntax_modifier`\s of :cmd:`Notation`. Symmetrically, the
+   ``only printing`` :n:`@syntax_modifier` can be used to declare that
+   a notation should only be used for printing.
+
+   If a notation to be used both for parsing and printing is
+   overriden, both the parsing and printing are invalided, even if the
+   overriding rule is only parsing.
+
+   If a given notation string occurs only in ``only printing`` rules,
+   the parser is not modified at all.
+
+   To a given notation string and scope can be attached at most one
+   notation with both parsing and printing or with only
+   parsing. Contrastingly, an arbitrary number of ``only printing``
+   notations differing in their right-hand sides but only a unique
+   right-hand side can be attached to a given string and
+   scope. Obviously, expressions printed by means of such extra
+   printing rules will not be reparsed to the same form.
 
 The Infix command
 ~~~~~~~~~~~~~~~~~~
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 43fef8685d..167ea3ecdf 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -551,7 +551,7 @@ and extern_notation_pattern allscopes vars t = function
   | [] -> raise No_match
   | (keyrule,pat,n as _rule)::rules ->
     try
-      if is_inactive_rule keyrule then raise No_match;
+      if is_inactive_rule keyrule || is_printing_inactive_rule keyrule pat then raise No_match;
       let loc = t.loc in
       match DAst.get t with
         | PatCstr (cstr,args,na) ->
@@ -568,7 +568,7 @@ let rec extern_notation_ind_pattern allscopes vars ind args = function
   | [] -> raise No_match
   | (keyrule,pat,n as _rule)::rules ->
     try
-      if is_inactive_rule keyrule then raise No_match;
+      if is_inactive_rule keyrule || is_printing_inactive_rule keyrule pat then raise No_match;
       apply_notation_to_pattern (GlobRef.IndRef ind)
         (match_notation_constr_ind_pattern ind args pat) allscopes vars keyrule
     with
@@ -1238,7 +1238,7 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules =
   | (keyrule,pat,n as _rule)::rules ->
       let loc = Glob_ops.loc_of_glob_constr t in
       try
-        if is_inactive_rule keyrule then raise No_match;
+        if is_inactive_rule keyrule || is_printing_inactive_rule keyrule pat then raise No_match;
         let f,args =
           match DAst.get t with
           | GApp (f,args) -> f,args
diff --git a/interp/notation.ml b/interp/notation.ml
index 7e90e15b72..d57c4f3abf 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -58,6 +58,31 @@ let notation_with_optional_scope_eq inscope1 inscope2 = match (inscope1,inscope2
 let notation_eq (from1,ntn1) (from2,ntn2) =
   notation_entry_eq from1 from2 && String.equal ntn1 ntn2
 
+let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2
+
+let notation_binder_source_eq s1 s2 = match s1, s2 with
+| NtnParsedAsIdent,  NtnParsedAsIdent -> true
+| NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2
+| NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2
+| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _), _ -> false
+
+let ntpe_eq t1 t2 = match t1, t2 with
+| NtnTypeConstr, NtnTypeConstr -> true
+| NtnTypeBinder s1, NtnTypeBinder s2 -> notation_binder_source_eq s1 s2
+| NtnTypeConstrList, NtnTypeConstrList -> true
+| NtnTypeBinderList, NtnTypeBinderList -> true
+| (NtnTypeConstr | NtnTypeBinder _ | NtnTypeConstrList | NtnTypeBinderList), _ -> false
+
+let var_attributes_eq (_, ((entry1, sc1), tp1)) (_, ((entry2, sc2), tp2)) =
+  notation_entry_level_eq entry1 entry2 &&
+  pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 &&
+  ntpe_eq tp1 tp2
+
+let interpretation_eq (vars1, t1 as x1) (vars2, t2 as x2) =
+  x1 == x2 ||
+  List.equal var_attributes_eq vars1 vars2 &&
+  Notation_ops.eq_notation_constr (List.map fst vars1, List.map fst vars2) t1 t2
+
 let pr_notation (from,ntn) = qstring ntn ++ match from with InConstrEntry -> mt () | InCustomEntry s -> str " in custom " ++ str s
 
 module NotationOrd =
@@ -90,8 +115,21 @@ type notation_data = {
   not_deprecation : Deprecation.t option;
 }
 
+type activation = bool
+
+type extra_printing_notation_data =
+  (activation * notation_data) list
+
+type parsing_notation_data =
+  | NoParsingData
+  | OnlyParsingData of activation * notation_data
+  | ParsingAndPrintingData of
+      activation (* for parsing*) *
+      activation (* for printing *) *
+      notation_data (* common data for both *)
+
 type scope = {
-  notations: notation_data NotationMap.t;
+  notations: (parsing_notation_data * extra_printing_notation_data) NotationMap.t;
   delimiters: delimiters option
 }
 
@@ -300,10 +338,19 @@ type notation_applicative_status =
 
 type notation_rule = interp_rule * interpretation * notation_applicative_status
 
+let notation_rule_eq (rule1,pat1,s1 as x1) (rule2,pat2,s2 as x2) =
+  x1 == x2 || (rule1 = rule2 && interpretation_eq pat1 pat2 && s1 = s2)
+
 let keymap_add key interp map =
   let old = try KeyMap.find key map with Not_found -> [] in
+  (* In case of re-import, no need to keep the previous copy *)
+  let old = try List.remove_first (notation_rule_eq interp) old with Not_found -> old in
   KeyMap.add key (interp :: old) map
 
+let keymap_remove key interp map =
+  let old = try KeyMap.find key map with Not_found -> [] in
+  KeyMap.add key (List.remove_first (notation_rule_eq interp) old) map
+
 let keymap_find key map =
   try KeyMap.find key map
   with Not_found -> []
@@ -1225,40 +1272,90 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
 
 (* The mapping between notations and their interpretation *)
 
+let pr_optional_scope = function
+  | LastLonelyNotation -> mt ()
+  | NotationInScope scope -> spc () ++ strbrk "in scope" ++ spc () ++ str scope
+
 let warn_notation_overridden =
   CWarnings.create ~name:"notation-overridden" ~category:"parsing"
-                   (fun (ntn,which_scope) ->
+                   (fun (scope,ntn) ->
                     str "Notation" ++ spc () ++ pr_notation ntn ++ spc ()
-                    ++ strbrk "was already used" ++ which_scope ++ str ".")
+                    ++ strbrk "was already used" ++ pr_optional_scope scope ++ str ".")
 
-let declare_notation_interpretation ntn scopt pat df ~onlyprint deprecation =
-  let scope = match scopt with Some s -> s | None -> default_scope in
-  let sc = find_scope scope in
-  if not onlyprint then begin
-    let () =
-      if NotationMap.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_deprecation = deprecation;
-    } in
-    let sc = { sc with notations = NotationMap.add ntn notdata sc.notations } in
-    scope_map := String.Map.add scope sc !scope_map
-  end;
-  begin match scopt with
-  | None -> scope_stack := LonelyNotationItem ntn :: !scope_stack
-  | Some _ -> ()
-  end
+let warn_deprecation_overridden =
+  CWarnings.create ~name:"notation-overridden" ~category:"parsing"
+                 (fun ((scope,ntn),old,now) ->
+                  match old, now with
+                  | None, None -> assert false
+                  | None, Some _ ->
+                    (str "Notation" ++ spc () ++ pr_notation ntn ++ pr_optional_scope scope ++ spc ()
+                    ++ strbrk "is now marked as deprecated" ++ str ".")
+                  | Some _, None ->
+                    (str "Cancelling previous deprecation of notation" ++ spc () ++
+                     pr_notation ntn ++ pr_optional_scope scope ++ str ".")
+                  | Some _, Some _ ->
+                    (str "Amending deprecation of notation" ++ spc () ++
+                     pr_notation ntn ++ pr_optional_scope scope ++ str "."))
+
+type notation_use =
+  | OnlyPrinting
+  | OnlyParsing
+  | ParsingAndPrinting
+
+let warn_override_if_needed (scopt,ntn) overridden data old_data =
+  if overridden then warn_notation_overridden (scopt,ntn)
+  else
+    if data.not_deprecation <> old_data.not_deprecation then
+      warn_deprecation_overridden ((scopt,ntn),old_data.not_deprecation,data.not_deprecation)
+
+let check_parsing_override (scopt,ntn) data = function
+  | OnlyParsingData (_,old_data) ->
+    let overridden = not (interpretation_eq data.not_interp old_data.not_interp) in
+    warn_override_if_needed (scopt,ntn) overridden data old_data;
+    None, not overridden
+  | ParsingAndPrintingData (_,on_printing,old_data) ->
+    let overridden = not (interpretation_eq data.not_interp old_data.not_interp) in
+    warn_override_if_needed (scopt,ntn) overridden data old_data;
+    (if on_printing then Some old_data.not_interp else None), not overridden
+  | NoParsingData -> None, false
+
+let check_printing_override (scopt,ntn) data parsingdata printingdata =
+  let parsing_update = match parsingdata with
+  | OnlyParsingData _ | NoParsingData -> parsingdata
+  | ParsingAndPrintingData (_,on_printing,old_data) ->
+    let overridden = not (interpretation_eq data.not_interp old_data.not_interp) in
+    warn_override_if_needed (scopt,ntn) overridden data old_data;
+    if overridden then NoParsingData else parsingdata in
+  let exists = List.exists (fun (on_printing,old_data) ->
+    let exists = interpretation_eq data.not_interp old_data.not_interp in
+    if exists && data.not_deprecation <> old_data.not_deprecation then
+      warn_deprecation_overridden ((scopt,ntn),old_data.not_deprecation,data.not_deprecation);
+    exists) printingdata in
+  parsing_update, exists
+
+let remove_uninterpretation rule (metas,c as pat) =
+  let (key,n) = notation_constr_key c in
+  notations_key_table := keymap_remove key (rule,pat,n) !notations_key_table
 
 let declare_uninterpretation rule (metas,c as pat) =
   let (key,n) = notation_constr_key c in
   notations_key_table := keymap_add key (rule,pat,n) !notations_key_table
 
+let update_notation_data (scopt,ntn) use data table =
+  let (parsingdata,printingdata) =
+    try NotationMap.find ntn table with Not_found -> (NoParsingData, []) in
+  match use with
+  | OnlyParsing ->
+    let printing_update, exists = check_parsing_override (scopt,ntn) data parsingdata in
+    NotationMap.add ntn (OnlyParsingData (true,data), printingdata) table, printing_update, exists
+  | ParsingAndPrinting ->
+    let printing_update, exists = check_parsing_override (scopt,ntn) data parsingdata in
+    NotationMap.add ntn (ParsingAndPrintingData (true,true,data), printingdata) table, printing_update, exists
+  | OnlyPrinting ->
+    let parsingdata, exists = check_printing_override (scopt,ntn) data parsingdata printingdata in
+    let printingdata = if exists then printingdata else (true,data) :: printingdata in
+    NotationMap.add ntn (parsingdata, printingdata) table, None, exists
+
 let rec find_interpretation ntn find = function
   | [] -> raise Not_found
   | OpenScopeItem scope :: scopes ->
@@ -1273,7 +1370,9 @@ let rec find_interpretation ntn find = function
       find_interpretation ntn find scopes
 
 let find_notation ntn sc =
-  NotationMap.find ntn (find_scope sc).notations
+  match fst (NotationMap.find ntn (find_scope sc).notations) with
+  | OnlyParsingData (true,data) | ParsingAndPrintingData (true,_,data) -> data
+  | _ -> raise Not_found
 
 let notation_of_prim_token = function
   | Constrexpr.Numeral (SPlus,n) -> InConstrEntry, NumTok.Unsigned.sprint n
@@ -1358,10 +1457,37 @@ let uninterp_cases_pattern_notations c =
 let uninterp_ind_pattern_notations ind =
   keymap_find (RefKey (canonical_gr (GlobRef.IndRef ind))) !notations_key_table
 
+let has_active_parsing_rule_in_scope ntn sc =
+  try
+    match NotationMap.find ntn (String.Map.find sc !scope_map).notations with
+    | OnlyParsingData (active,_),_ | ParsingAndPrintingData (active,_,_),_ -> active
+    | _ -> false
+  with Not_found -> false
+
+let is_printing_active_in_scope (scope,ntn) pat =
+  let sc = match scope with NotationInScope sc -> sc | LastLonelyNotation -> default_scope in
+  let is_active extra =
+    try
+      let (_,(active,_)) = List.extract_first (fun (active,d) -> interpretation_eq d.not_interp pat) extra in
+      active
+    with Not_found -> false in
+  try
+    match NotationMap.find ntn (String.Map.find sc !scope_map).notations with
+    | ParsingAndPrintingData (_,active,d), extra ->
+       if interpretation_eq d.not_interp pat then active
+       else is_active extra
+    | _, extra -> is_active extra
+  with Not_found -> false
+
+let is_printing_inactive_rule rule pat =
+  match rule with
+  | NotationRule (scope,ntn) ->
+    not (is_printing_active_in_scope (scope,ntn) pat)
+  | SynDefRule kn ->
+    try let _ = Nametab.path_of_syndef kn in false with Not_found -> true
+
 let availability_of_notation (ntn_scope,ntn) scopes =
-  let f scope =
-    NotationMap.mem ntn (String.Map.find scope !scope_map).notations in
-  find_without_delimiters f (ntn_scope,Some ntn) (make_current_scopes scopes)
+  find_without_delimiters (has_active_parsing_rule_in_scope ntn) (ntn_scope,Some ntn) (make_current_scopes scopes)
 
 (* We support coercions from a custom entry at some level to an entry
    at some level (possibly the same), and from and to the constr entry. E.g.:
@@ -1484,6 +1610,49 @@ let entry_has_ident = function
   | InCustomEntryLevel (s,n) ->
      try String.Map.find s !entry_has_ident_map <= n with Not_found -> false
 
+type entry_coercion_kind =
+  | IsEntryCoercion of notation_entry_level
+  | IsEntryGlobal of string * int
+  | IsEntryIdent of string * int
+
+let declare_notation (scopt,ntn) pat df ~use coe deprecation =
+  (* Register the interpretation *)
+  let scope = match scopt with NotationInScope s -> s | LastLonelyNotation -> default_scope in
+  let sc = find_scope scope in
+  let notdata = {
+    not_interp = pat;
+    not_location = df;
+    not_deprecation = deprecation;
+  } in
+  let notation_update,printing_update, exists = update_notation_data (scopt,ntn) use notdata sc.notations in
+  if not exists then
+    let sc = { sc with notations = notation_update } in
+    scope_map := String.Map.add scope sc !scope_map;
+  (* Update the uninterpretation cache *)
+  begin match printing_update with
+  | Some pat -> remove_uninterpretation (NotationRule (scopt,ntn)) pat
+  | None -> ()
+  end;
+  if not exists && use <> OnlyParsing then declare_uninterpretation (NotationRule (scopt,ntn)) pat;
+  (* Register visibility of lonely notations *)
+  if not exists then begin match scopt with
+  | LastLonelyNotation -> scope_stack := LonelyNotationItem ntn :: !scope_stack
+  | NotationInScope _ -> ()
+  end;
+  (* Declare a possible coercion *)
+  if not exists then begin match coe with
+   | Some (IsEntryCoercion entry) ->
+     let (_,level,_) = level_of_notation ntn in
+     let level = match fst ntn with
+       | InConstrEntry -> None
+       | InCustomEntry _ -> Some level
+     in
+     declare_entry_coercion (scopt,ntn) level entry
+   | Some (IsEntryGlobal (entry,n)) -> declare_custom_entry_has_global entry n
+   | Some (IsEntryIdent (entry,n)) -> declare_custom_entry_has_ident entry n
+   | None -> ()
+  end
+
 let availability_of_prim_token n printer_scope local_scopes =
   let f scope =
     try
@@ -1561,38 +1730,6 @@ let uninterp_prim_token_cases_pattern c local_scopes =
 
 (* Miscellaneous *)
 
-let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2
-
-let notation_binder_source_eq s1 s2 = match s1, s2 with
-| NtnParsedAsIdent,  NtnParsedAsIdent -> true
-| NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2
-| NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2
-| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _), _ -> false
-
-let ntpe_eq t1 t2 = match t1, t2 with
-| NtnTypeConstr, NtnTypeConstr -> true
-| NtnTypeBinder s1, NtnTypeBinder s2 -> notation_binder_source_eq s1 s2
-| NtnTypeConstrList, NtnTypeConstrList -> true
-| NtnTypeBinderList, NtnTypeBinderList -> true
-| (NtnTypeConstr | NtnTypeBinder _ | NtnTypeConstrList | NtnTypeBinderList), _ -> false
-
-let var_attributes_eq (_, ((entry1, sc1), tp1)) (_, ((entry2, sc2), tp2)) =
-  notation_entry_level_eq entry1 entry2 &&
-  pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 &&
-  ntpe_eq tp1 tp2
-
-let interpretation_eq (vars1, t1) (vars2, t2) =
-  List.equal var_attributes_eq vars1 vars2 &&
-  Notation_ops.eq_notation_constr (List.map fst vars1, List.map fst vars2) t1 t2
-
-let exists_notation_in_scope scopt ntn onlyprint r =
-  let scope = match scopt with Some s -> s | None -> default_scope in
-  try
-    let sc = String.Map.find scope !scope_map in
-    let n = NotationMap.find ntn sc.notations in
-    interpretation_eq n.not_interp r
-  with Not_found -> false
-
 let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false
 
 (**********************************************************************)
@@ -1846,38 +1983,63 @@ let pr_scope_classes sc =
   | _ :: ll ->
     let opt_s = match ll with [] -> mt () | _ -> str "es" in
     hov 0 (str "Bound to class" ++ opt_s ++
-      spc() ++ prlist_with_sep spc pr_scope_class l) ++ fnl()
+      spc() ++ prlist_with_sep spc pr_scope_class l)
 
 let pr_notation_info prglob ntn c =
-  str "\"" ++ str ntn ++ str "\" := " ++
+  str "\"" ++ str ntn ++ str "\" :=" ++ brk (1,2) ++
   prglob (Notation_ops.glob_constr_of_notation_constr c)
 
-let pr_named_scope prglob scope sc =
+let pr_notation_status on_parsing on_printing =
+  let deactivated b = if b then [] else ["deactivated"] in
+  let l = match on_parsing, on_printing with
+  | Some on, None -> "only parsing" :: deactivated on
+  | None, Some on -> "only printing" :: deactivated on
+  | Some false, Some false -> ["deactivated"]
+  | Some true, Some false -> ["deactivated for printing"]
+  | Some false, Some true -> ["deactivated for parsing"]
+  | Some true, Some true -> []
+  | None, None -> assert false in
+  match l with
+  | [] -> mt ()
+  | l -> str "(" ++ prlist_with_sep pr_comma str l ++ str ")"
+
+let pr_non_empty spc pp =
+  if pp = mt () then mt () else spc ++ pp
+
+let pr_notation_data prglob (on_parsing,on_printing,{ not_interp  = (_, r); not_location = (_, df) }) =
+  hov 0 (pr_notation_info prglob df r ++ pr_non_empty (brk(1,2)) (pr_notation_status on_parsing on_printing))
+
+let extract_notation_data (main,extra) =
+  let main = match main with
+  | NoParsingData -> []
+  | ParsingAndPrintingData (on_parsing, on_printing, d) ->
+    [Some on_parsing, Some on_printing, d]
+  | OnlyParsingData (on_parsing, d) ->
+    [Some on_parsing, None, d] in
+  let extra = List.map (fun (on_printing, d) -> (None, Some on_printing, d)) extra in
+  main @ extra
+
+let pr_named_scope prglob (scope,sc) =
  (if String.equal scope default_scope then
    match NotationMap.cardinal sc.notations with
      | 0 -> str "No lonely notation"
      | n -> str "Lonely notation" ++ (if Int.equal n 1 then mt() else str"s")
   else
     str "Scope " ++ str scope ++ fnl () ++ pr_delimiters_info sc.delimiters)
-  ++ fnl ()
-  ++ pr_scope_classes scope
-  ++ NotationMap.fold
-       (fun ntn { not_interp  = (_, r); not_location = (_, df) } strm ->
-         pr_notation_info prglob df r ++ fnl () ++ strm)
-       sc.notations (mt ())
+  ++ pr_non_empty (fnl ()) (pr_scope_classes scope)
+  ++ prlist (fun a -> fnl () ++ pr_notation_data prglob a)
+       (NotationMap.fold (fun ntn data l -> extract_notation_data data @ l) sc.notations [])
 
-let pr_scope prglob scope = pr_named_scope prglob scope (find_scope scope)
+let pr_scope prglob scope = pr_named_scope prglob (scope, find_scope scope)
 
 let pr_scopes prglob =
- String.Map.fold
-   (fun scope sc strm -> pr_named_scope prglob scope sc ++ fnl () ++ strm)
-   !scope_map (mt ())
+ let l = String.Map.bindings !scope_map in
+ prlist_with_sep (fun () -> fnl () ++ fnl ()) (pr_named_scope prglob) l
 
 let rec find_default ntn = function
   | [] -> None
   | OpenScopeItem scope :: scopes ->
-    if NotationMap.mem ntn (find_scope scope).notations then
-      Some scope
+    if has_active_parsing_rule_in_scope ntn scope then Some scope
     else find_default ntn scopes
   | LonelyNotationItem ntn' :: scopes ->
     if notation_eq ntn ntn' then Some default_scope
@@ -1885,12 +2047,12 @@ let rec find_default ntn = function
 
 let factorize_entries = function
   | [] -> []
-  | (ntn,c)::l ->
+  | (ntn,sc',c)::l ->
       let (ntn,l_of_ntn,rest) =
         List.fold_left
-          (fun (a',l,rest) (a,c) ->
-            if notation_eq a a' then (a',c::l,rest) else (a,[c],(a',l)::rest))
-          (ntn,[c],[]) l in
+          (fun (a',l,rest) (a,sc,c) ->
+            if notation_eq a a' then (a',(sc,c)::l,rest) else (a,[sc,c],(a',l)::rest))
+          (ntn,[sc',c],[]) l in
       (ntn,l_of_ntn)::rest
 
 type symbol_token = WhiteSpace of int | String of string
@@ -1961,16 +2123,18 @@ let browse_notation strict ntn map =
   let l =
     String.Map.fold
       (fun scope_name sc ->
-        NotationMap.fold (fun ntn { not_interp  = (_, r); not_location = df } l ->
-          if List.exists (find ntn) ntns then (ntn,(scope_name,r,df))::l else l) sc.notations)
+        NotationMap.fold (fun ntn data l ->
+          if List.exists (find ntn) ntns
+          then List.map (fun d -> (ntn,scope_name,d)) (extract_notation_data data) @ l
+          else l) sc.notations)
       map [] in
-  List.sort (fun x y -> String.compare (snd (fst x)) (snd (fst y))) l
+  List.sort (fun x y -> String.compare (snd (pi1 x)) (snd (pi1 y))) l
 
-let global_reference_of_notation ~head test (ntn,(sc,c,_)) =
+let global_reference_of_notation ~head test (ntn,sc,(on_parsing,on_printing,{not_interp = (_,c)})) =
   match c with
-  | NRef ref when test ref -> Some (ntn,sc,ref)
+  | NRef ref when test ref -> Some (on_parsing,on_printing,ntn,sc,ref)
   | NApp (NRef ref, l) when head || List.for_all isNVar_or_NHole l && test ref ->
-      Some (ntn,sc,ref)
+      Some (on_parsing,on_printing,ntn,sc,ref)
   | _ -> None
 
 let error_ambiguous_notation ?loc _ntn =
@@ -1990,17 +2154,17 @@ let interp_notation_as_global_reference ?loc ~head test ntn sc =
   let ntns = browse_notation true ntn scopes in
   let refs = List.map (global_reference_of_notation ~head test) ntns in
   match Option.List.flatten refs with
-  | [_,_,ref] -> ref
+  | [Some true,_ (* why not if the only one? *),_,_,ref] -> ref
   | [] -> error_notation_not_reference ?loc ntn
   | refs ->
-      let f (ntn,sc,ref) =
+      let f (on_parsing,_,ntn,sc,ref) =
         let def = find_default ntn !scope_stack in
         match def with
         | None -> false
-        | Some sc' -> String.equal sc sc'
+        | Some sc' -> on_parsing = Some true && String.equal sc sc'
       in
       match List.filter f refs with
-      | [_,_,ref] -> ref
+      | [_,_,_,_,ref] -> ref
       | [] -> error_notation_not_reference ?loc ntn
       | _ -> error_ambiguous_notation ?loc ntn
 
@@ -2010,24 +2174,25 @@ let locate_notation prglob ntn scope =
   match ntns with
   | [] -> str "Unknown notation"
   | _ ->
-    str "Notation" ++ fnl () ++
     prlist_with_sep fnl (fun (ntn,l) ->
       let scope = find_default ntn scopes in
       prlist_with_sep fnl
-        (fun (sc,r,(_,df)) ->
+        (fun (sc,(on_parsing,on_printing,{ not_interp  = (_, r); not_location = (_, df) })) ->
           hov 0 (
+            str "Notation" ++ brk (1,2) ++
             pr_notation_info prglob df r ++
             (if String.equal sc default_scope then mt ()
-             else (spc () ++ str ": " ++ str sc)) ++
+             else (brk (1,2) ++ str ": " ++ str sc)) ++
             (if Option.equal String.equal (Some sc) scope
-             then spc () ++ str "(default interpretation)" else mt ())))
+             then brk (1,2) ++ str "(default interpretation)" else mt ()) ++
+            pr_non_empty (brk (1,2)) (pr_notation_status on_parsing on_printing)))
         l) ntns
 
 let collect_notation_in_scope scope sc known =
   assert (not (String.equal scope default_scope));
   NotationMap.fold
-    (fun ntn { not_interp  = (_, r); not_location = (_, df) } (l,known as acc) ->
-      if List.mem_f notation_eq ntn known then acc else ((df,r)::l,ntn::known))
+    (fun ntn d (l,known as acc) ->
+      if List.mem_f notation_eq ntn known then acc else (extract_notation_data d @ l,ntn::known))
     sc.notations ([],known)
 
 let collect_notations stack =
@@ -2043,13 +2208,13 @@ let collect_notations stack =
           if List.mem_f notation_eq ntn knownntn then (all,knownntn)
           else
           try
-            let { not_interp  = (_, r); not_location = (_, df) } =
-              NotationMap.find ntn (find_scope default_scope).notations in
+            let datas = extract_notation_data
+              (NotationMap.find ntn (find_scope default_scope).notations) in
             let all' = match all with
               | (s,lonelyntn)::rest when String.equal s default_scope ->
-                  (s,(df,r)::lonelyntn)::rest
+                  (s,datas@lonelyntn)::rest
               | _ ->
-                  (default_scope,[df,r])::all in
+                  (default_scope,datas)::all in
             (all',ntn::knownntn)
           with Not_found -> (* e.g. if only printing *) (all,knownntn))
     ([],[]) stack)
@@ -2057,7 +2222,7 @@ let collect_notations stack =
 let pr_visible_in_scope prglob (scope,ntns) =
   let strm =
     List.fold_right
-      (fun (df,r) strm -> pr_notation_info prglob df r ++ fnl () ++ strm)
+      (fun d strm -> pr_notation_data prglob d ++ fnl () ++ strm)
       ntns (mt ()) in
   (if String.equal scope default_scope then
      str "Lonely notation" ++ (match ntns with [_] -> mt () | _ -> str "s")
@@ -2066,9 +2231,7 @@ let pr_visible_in_scope prglob (scope,ntns) =
   ++ fnl () ++ strm
 
 let pr_scope_stack prglob stack =
-  List.fold_left
-    (fun strm scntns -> strm ++ pr_visible_in_scope prglob scntns ++ fnl ())
-    (mt ()) (collect_notations stack)
+  prlist_with_sep fnl (pr_visible_in_scope prglob) (collect_notations stack)
 
 let pr_visibility prglob = function
   | Some scope -> pr_scope_stack prglob (push_scope scope !scope_stack)
diff --git a/interp/notation.mli b/interp/notation.mli
index 948831b317..d744ff41d9 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -229,12 +229,24 @@ type interp_rule =
   | NotationRule of specific_notation
   | SynDefRule of KerName.t
 
-val declare_notation_interpretation : notation -> scope_name option ->
-  interpretation -> notation_location -> onlyprint:bool ->
-  Deprecation.t option -> unit
+type notation_use =
+  | OnlyPrinting
+  | OnlyParsing
+  | ParsingAndPrinting
 
 val declare_uninterpretation : interp_rule -> interpretation -> unit
 
+type entry_coercion_kind =
+  | IsEntryCoercion of notation_entry_level
+  | IsEntryGlobal of string * int
+  | IsEntryIdent of string * int
+
+val declare_notation : notation_with_optional_scope * notation ->
+  interpretation -> notation_location -> use:notation_use ->
+  entry_coercion_kind option ->
+  Deprecation.t option -> unit
+
+
 (** Return the interpretation bound to a notation *)
 val interp_notation : ?loc:Loc.t -> notation -> subscopes ->
       interpretation * (notation_location * scope_name option)
@@ -257,16 +269,14 @@ val uninterp_ind_pattern_notations : inductive -> notation_rule list
 val availability_of_notation : specific_notation -> subscopes ->
   (scope_name option * delimiters option) option
 
+val is_printing_inactive_rule : interp_rule -> interpretation -> bool
+
 (** {6 Miscellaneous} *)
 
 (** If head is true, also allows applied global references. *)
 val interp_notation_as_global_reference : ?loc:Loc.t -> head:bool -> (GlobRef.t -> bool) ->
       notation_key -> delimiters option -> GlobRef.t
 
-(** Checks for already existing notations *)
-val exists_notation_in_scope : scope_name option -> notation ->
-      bool -> interpretation -> bool
-
 (** Declares and looks for scopes associated to arguments of a global ref *)
 val declare_arguments_scope :
   bool (** true=local *) -> GlobRef.t -> scope_name option list -> unit
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 22531b0016..354809252e 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -27,7 +27,9 @@ open Notation_term
 (* helper for NVar, NVar case in eq_notation_constr *)
 let get_var_ndx id vs = try Some (List.index Id.equal id vs) with Not_found -> None
 
-let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
+let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 =
+(vars1 == vars2 && t1 == t2) ||
+match t1, t2 with
 | NRef gr1, NRef gr2 -> GlobRef.equal gr1 gr2
 | NVar id1, NVar id2 -> (
    match (get_var_ndx id1 vars1,get_var_ndx id2 vars2) with
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index abada44da7..bd22d45059 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -231,16 +231,13 @@ fun l : list nat => match l with
      : list nat -> list nat
 
 Arguments foo _%list_scope
-Notation
-"'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope
-(default interpretation)
-"'exists' ! x .. y , p" := ex
-                             (unique
-                                (fun x => .. (ex (unique (fun y => p))) ..))
-: type_scope (default interpretation)
-Notation
-"( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope
-(default interpretation)
+Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..))
+  : type_scope (default interpretation)
+Notation "'exists' ! x .. y , p" :=
+  (ex (unique (fun x => .. (ex (unique (fun y => p))) ..))) : type_scope
+  (default interpretation)
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope
+  (default interpretation)
 1 subgoal
   
   ============================
diff --git a/test-suite/output/bug_12908.out b/test-suite/output/bug_12908.out
index fca6dde704..54c4f98422 100644
--- a/test-suite/output/bug_12908.out
+++ b/test-suite/output/bug_12908.out
@@ -1,2 +1,7 @@
 forall m n : nat, m * n = (2 * m * n)%nat
      : Prop
+File "stdin", line 11, characters 0-31:
+Warning: Notation "_ * _" was already used in scope nat_scope.
+[notation-overridden,parsing]
+forall m n : nat, m * n = Nat.mul (Nat.mul 2 m) n
+     : Prop
diff --git a/test-suite/output/bug_12908.v b/test-suite/output/bug_12908.v
index 558c9f9f6a..6f7be22fa0 100644
--- a/test-suite/output/bug_12908.v
+++ b/test-suite/output/bug_12908.v
@@ -1,6 +1,13 @@
 Definition mult' m n := 2 * m * n.
+
 Module A.
 (* Test hiding of a scoped notation by a lonely notation *)
 Infix "*" := mult'.
 Check forall m n, mult' m n = Nat.mul (Nat.mul 2 m) n.
 End A.
+
+Module B.
+(* Test that an overriden scoped notation is deactivated *)
+Infix "*" := mult' : nat_scope.
+Check forall m n, mult' m n = Nat.mul (Nat.mul 2 m) n.
+End B.
diff --git a/test-suite/output/bug_13112.out b/test-suite/output/bug_13112.out
new file mode 100644
index 0000000000..a8a98d6b68
--- /dev/null
+++ b/test-suite/output/bug_13112.out
@@ -0,0 +1,4 @@
+0 + 0
+     : nat
+HI
+     : nat
diff --git a/test-suite/output/bug_13112.v b/test-suite/output/bug_13112.v
new file mode 100644
index 0000000000..9fee5e09d8
--- /dev/null
+++ b/test-suite/output/bug_13112.v
@@ -0,0 +1,5 @@
+Reserved Notation "'HI'".
+Notation "'HI'" := (O + O) (only parsing).
+Check HI. (* 0 + 0 : nat *)
+Notation "'HI'" := (O + O) (only printing).
+Check HI. (* 0 + 0 : nat *)
diff --git a/test-suite/output/bug_9180.out b/test-suite/output/bug_9180.out
index ed4892b389..f035d0252a 100644
--- a/test-suite/output/bug_9180.out
+++ b/test-suite/output/bug_9180.out
@@ -1,4 +1,3 @@
-Notation
-"n .+1" := S n : nat_scope (default interpretation)
+Notation "n .+1" := (S n) : nat_scope (default interpretation)
 forall x : nat, x.+1 = x.+1
      : Prop
diff --git a/test-suite/output/bug_9682.out b/test-suite/output/bug_9682.out
index e69de29bb2..45d9e4cad1 100644
--- a/test-suite/output/bug_9682.out
+++ b/test-suite/output/bug_9682.out
@@ -0,0 +1,9 @@
+mmatch 1 + 2 + 3 + 4 + 5 + 6 in nat as x
+return M (x = x) with
+| 1
+end
+     : unit
+#
+     : True
+##
+     : True
diff --git a/test-suite/output/bug_9682.v b/test-suite/output/bug_9682.v
index 3630142126..fa30d323ef 100644
--- a/test-suite/output/bug_9682.v
+++ b/test-suite/output/bug_9682.v
@@ -16,3 +16,13 @@ Notation "'mmatch' x 'in' T 'as' y 'return' 'M' p 'with' ls 'end'" :=
     (at level 200, ls at level 91, p at level 10, only printing,
      format "'[  ' mmatch  '/' x ']'  '/' '[  ' in  '/' T ']'  '/' '[  ' as  '/' y ']'  '/' '[  ' return  M  p ']'  with  '//' '[' ls ']'  '//' end"
      ).
+(* Check use of "mmatch" *)
+Check (mmatch 1 + 2 + 3 + 4 + 5 + 6 in nat as x return M (x = x) with | 1 end).
+
+(* 2nd example *)
+Notation "#" := I (at level 0, only parsing).
+Notation "#" := I (at level 0, only printing).
+Check #.
+Notation "##" := I (at level 0, only printing).
+Notation "##" := I (at level 0, only parsing).
+Check ##.
diff --git a/test-suite/output/locate.out b/test-suite/output/locate.out
index 473db2d312..93d9d6cf7b 100644
--- a/test-suite/output/locate.out
+++ b/test-suite/output/locate.out
@@ -1,3 +1,2 @@
-Notation
-"b1 && b2" := if b1 then b2 else false (default interpretation)
-"x && y" := andb x y : bool_scope
+Notation "b1 && b2" := (if b1 then b2 else false) (default interpretation)
+Notation "x && y" := (andb x y) : bool_scope
diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v
index f35da63fd6..e8a036bbb0 100644
--- a/theories/ssr/ssrbool.v
+++ b/theories/ssr/ssrbool.v
@@ -1401,8 +1401,8 @@ Definition mem T (pT : predType T) : pT -> mem_pred T :=
   let: PredType toP := pT in fun A => Mem [eta toP A].
 Arguments mem {T pT} A : rename, simpl never.
 
-Notation "x \in A" := (in_mem x (mem A)) : bool_scope.
-Notation "x \in A" := (in_mem x (mem A)) : bool_scope.
+Notation "x \in A" := (in_mem x (mem A)) (only parsing) : bool_scope.
+Notation "x \in A" := (in_mem x (mem A)) (only printing) : bool_scope.
 Notation "x \notin A" := (~~ (x \in A)) : bool_scope.
 Notation "A =i B" := (eq_mem (mem A) (mem B)) : type_scope.
 Notation "{ 'subset' A <= B }" := (sub_mem (mem A) (mem B)) : type_scope.
@@ -1573,9 +1573,12 @@ Arguments has_quality n {T}.
 
 Lemma qualifE n T p x : (x \in @Qualifier n T p) = p x. Proof. by []. Qed.
 
-Notation "x \is A" := (x \in has_quality 0 A) : bool_scope.
-Notation "x \is 'a' A" := (x \in has_quality 1 A) : bool_scope.
-Notation "x \is 'an' A" := (x \in has_quality 2 A) : bool_scope.
+Notation "x \is A" := (x \in has_quality 0 A) (only parsing) : bool_scope.
+Notation "x \is A" := (x \in has_quality 0 A) (only printing) : bool_scope.
+Notation "x \is 'a' A" := (x \in has_quality 1 A) (only parsing) : bool_scope.
+Notation "x \is 'a' A" := (x \in has_quality 1 A) (only printing) : bool_scope.
+Notation "x \is 'an' A" := (x \in has_quality 2 A) (only parsing) : bool_scope.
+Notation "x \is 'an' A" := (x \in has_quality 2 A) (only printing) : bool_scope.
 Notation "x \isn't A" := (x \notin has_quality 0 A) : bool_scope.
 Notation "x \isn't 'a' A" := (x \notin has_quality 1 A) : bool_scope.
 Notation "x \isn't 'an' A" := (x \notin has_quality 2 A) : bool_scope.
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 58b1698848..8ce59c40c3 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1165,11 +1165,6 @@ let warn_non_reversible_notation =
              str " not occur in the right-hand side." ++ spc() ++
              strbrk "The notation will not be used for printing as it is not reversible.")
 
-type entry_coercion_kind =
-  | IsEntryCoercion of notation_entry_level
-  | IsEntryGlobal of string * int
-  | IsEntryIdent of string * int
-
 let is_coercion level typs =
   match level, typs with
   | Some (custom,n,_), [e] ->
@@ -1417,8 +1412,7 @@ type notation_obj = {
   notobj_scope : scope_name option;
   notobj_interp : interpretation;
   notobj_coercion : entry_coercion_kind option;
-  notobj_onlyparse : bool;
-  notobj_onlyprint : bool;
+  notobj_use : notation_use option;
   notobj_deprecation : Deprecation.t option;
   notobj_notation : notation * notation_location;
   notobj_specific_pp_rules : syntax_printing_extension option;
@@ -1442,37 +1436,19 @@ let open_notation i (_, nobj) =
     let scope = nobj.notobj_scope in
     let (ntn, df) = nobj.notobj_notation in
     let pat = nobj.notobj_interp in
-    let onlyprint = nobj.notobj_onlyprint  in
     let deprecation = nobj.notobj_deprecation in
-    let specific = match scope with None -> LastLonelyNotation | Some sc -> NotationInScope sc in
-    let specific_ntn = (specific,ntn) in
-    let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in
-    if fresh then begin
-      (* Declare the interpretation *)
-      let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint deprecation in
-      (* Declare the uninterpretation *)
-      if not nobj.notobj_onlyparse then
-        Notation.declare_uninterpretation (NotationRule specific_ntn) pat;
-      (* Declare a possible coercion *)
-      (match nobj.notobj_coercion with
-      | Some (IsEntryCoercion entry) ->
-        let (_,level,_) = Notation.level_of_notation ntn in
-        let level = match fst ntn with
-          | InConstrEntry -> None
-          | InCustomEntry _ -> Some level
-        in
-        Notation.declare_entry_coercion specific_ntn level entry
-      | Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n
-      | Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n
-      | None -> ())
-      end;
+    let scope = match scope with None -> LastLonelyNotation | Some sc -> NotationInScope sc in
+    (* Declare the notation *)
+    (match nobj.notobj_use with
+    | Some use -> Notation.declare_notation (scope,ntn) pat df ~use nobj.notobj_coercion deprecation
+    | None -> ());
     (* Declare specific format if any *)
-    match nobj.notobj_specific_pp_rules with
+    (match nobj.notobj_specific_pp_rules with
     | Some pp_sy ->
-      if specific_format_to_declare specific_ntn pp_sy then
+      if specific_format_to_declare (scope,ntn) pp_sy then
         Ppextend.declare_specific_notation_printing_rules
-          specific_ntn ~extra:pp_sy.synext_extra pp_sy.synext_unparsing
-    | None -> ()
+          (scope,ntn) ~extra:pp_sy.synext_extra pp_sy.synext_unparsing
+    | None -> ())
   end
 
 let cache_notation o =
@@ -1602,6 +1578,20 @@ let make_printing_rules reserved (sd : SynData.syn_data) = let open SynData in
     synext_extra  = sd.extra;
   }
 
+let warn_unused_interpretation =
+  CWarnings.create ~name:"unused-notation" ~category:"parsing"
+         (fun b ->
+          strbrk "interpretation is used neither for printing nor for parsing, " ++
+          (if b then strbrk "the declaration could be replaced by \"Reserved Notation\"."
+          else strbrk "the declaration could be removed."))
+
+let make_use reserved onlyparse onlyprint =
+  match onlyparse, onlyprint with
+  | false, false -> Some ParsingAndPrinting
+  | true, false -> Some OnlyParsing
+  | false, true -> Some OnlyPrinting
+  | true, true -> warn_unused_interpretation reserved; None
+
 (**********************************************************************)
 (* Main functions about notations                                     *)
 
@@ -1633,14 +1623,14 @@ let add_notation_in_scope ~local deprecation df env c mods scope =
   let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
   let onlyparse,coe = printability (Some sd.level) sd.subentries sd.only_parsing reversibility ac in
   let notation, location = sd.info in
+  let use = make_use true onlyparse sd.only_printing in
   let notation = {
     notobj_local = local;
     notobj_scope = scope;
     notobj_interp = (List.map_filter map i_vars, ac);
     (* Order is important here! *)
-    notobj_onlyparse = onlyparse;
+    notobj_use = use;
     notobj_coercion = coe;
-    notobj_onlyprint = sd.only_printing;
     notobj_deprecation = sd.deprecation;
     notobj_notation = (notation, location);
     notobj_specific_pp_rules = sy_pp_rules;
@@ -1676,14 +1666,14 @@ let add_notation_interpretation_core ~local df env ?(impls=empty_internalization
   let interp = make_interpretation_vars recvars plevel acvars (List.combine mainvars i_typs) in
   let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
   let onlyparse,coe = printability level i_typs onlyparse reversibility ac in
+  let use = make_use false onlyparse onlyprint in
   let notation = {
     notobj_local = local;
     notobj_scope = scope;
     notobj_interp = (List.map_filter map i_vars, ac);
     (* Order is important here! *)
-    notobj_onlyparse = onlyparse;
+    notobj_use = use;
     notobj_coercion = coe;
-    notobj_onlyprint = onlyprint;
     notobj_deprecation = deprecation;
     notobj_notation = df';
     notobj_specific_pp_rules = pp_sy;
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index fe27d9ac8a..0d3f38d139 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1790,11 +1790,11 @@ let vernac_print ~pstate =
   | PrintHintDbName s -> Hints.pr_hint_db_by_name env sigma s
   | PrintHintDb -> Hints.pr_searchtable env sigma
   | PrintScopes ->
-    Notation.pr_scopes (Constrextern.without_symbols (pr_lglob_constr_env env))
+    Notation.pr_scopes (Constrextern.without_symbols (pr_glob_constr_env env))
   | PrintScope s ->
-    Notation.pr_scope (Constrextern.without_symbols (pr_lglob_constr_env env)) s
+    Notation.pr_scope (Constrextern.without_symbols (pr_glob_constr_env env)) s
   | PrintVisibility s ->
-    Notation.pr_visibility (Constrextern.without_symbols (pr_lglob_constr_env env)) s
+    Notation.pr_visibility (Constrextern.without_symbols (pr_glob_constr_env env)) s
   | PrintAbout (ref_or_by_not,udecl,glnumopt) ->
     print_about_hyp_globs ~pstate ref_or_by_not udecl glnumopt
   | PrintImplicit qid ->
@@ -1830,7 +1830,7 @@ let vernac_locate ~pstate = let open Constrexpr in function
   | LocateTerm {v=ByNotation (ntn, sc)} ->
     let _, env = get_current_or_global_context ~pstate in
     Notation.locate_notation
-      (Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc
+      (Constrextern.without_symbols (pr_glob_constr_env env)) ntn sc
   | LocateLibrary qid -> print_located_library qid
   | LocateModule qid -> Prettyp.print_located_module qid
   | LocateOther (s, qid) -> Prettyp.print_located_other s qid