Merge PR #12523: Fix #11121: Simultaneous definition of term and notation in custom gr…

Reviewed-by: SkySkimmer
Ack-by: ejgallego
Ack-by: herbelin

5 files changed, 146 insertions, 105 deletions

diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index fdc8b1ba4c..cbd83e88b6 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -542,7 +542,7 @@ let make_act : type r. r target -> _ -> r gen_eval = function
   CAst.make ~loc @@ CPatNotation (None, notation, env, [])
 
 let extend_constr state forpat ng =
-  let custom,n,_,_ = ng.notgram_level in
+  let custom,n,_ = ng.notgram_level in
   let assoc = ng.notgram_assoc in
   let (entry, level) = interp_constr_entry_key custom forpat n in
   let fold (accu, state) pt =
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 45bf61d79e..e1f1affb2f 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -51,6 +51,7 @@ let record_field = Entry.create "vernac:record_field"
 let of_type_with_opt_coercion = Entry.create "vernac:of_type_with_opt_coercion"
 let section_subset_expr = Entry.create "vernac:section_subset_expr"
 let scope_delimiter = Entry.create "vernac:scope_delimiter"
+let syntax_modifiers = Entry.create "vernac:syntax_modifiers"
 let only_parsing = Entry.create "vernac:only_parsing"
 
 let make_bullet s =
@@ -321,10 +322,13 @@ GRAMMAR EXTEND Gram
       | -> { None } ] ]
   ;
   decl_notation:
-    [ [ ntn = ne_lstring; ":="; c = constr; b = only_parsing;
+    [ [ ntn = ne_lstring; ":="; c = constr;
+        modl = syntax_modifiers;
         scopt = OPT [ ":"; sc = IDENT -> { sc } ] ->
       { { decl_ntn_string = ntn; decl_ntn_interp = c;
-          decl_ntn_only_parsing = b; decl_ntn_scope = scopt } } ] ]
+          decl_ntn_scope = scopt;
+          decl_ntn_modifiers = modl;
+      } } ] ]
   ;
   decl_sep:
     [ [ IDENT "and" -> { () } ] ]
@@ -1118,7 +1122,7 @@ GRAMMAR EXTEND Gram
 (* Grammar extensions *)
 
 GRAMMAR EXTEND Gram
-  GLOBAL: syntax only_parsing;
+  GLOBAL: syntax only_parsing syntax_modifiers;
 
   syntax:
    [ [ IDENT "Open"; IDENT "Scope"; sc = IDENT ->
@@ -1136,7 +1140,7 @@ GRAMMAR EXTEND Gram
        refl = LIST1 class_rawexpr -> { VernacBindScope (sc,refl) }
 
      | IDENT "Infix"; op = ne_lstring; ":="; p = constr;
-         modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ];
+         modl = syntax_modifiers;
          sc = OPT [ ":"; sc = IDENT -> { sc } ] ->
          { VernacInfix ((op,modl),p,sc) }
      | IDENT "Notation"; id = identref;
@@ -1145,20 +1149,20 @@ GRAMMAR EXTEND Gram
              (id,(idl,c),{ onlyparsing = b }) }
      | IDENT "Notation"; s = lstring; ":=";
          c = constr;
-         modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ];
+         modl = syntax_modifiers;
          sc = OPT [ ":"; sc = IDENT -> { sc } ] ->
            { VernacNotation (c,(s,modl),sc) }
      | IDENT "Format"; IDENT "Notation"; n = STRING; s = STRING; fmt = STRING ->
            { VernacNotationAddFormat (n,s,fmt) }
 
      | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring;
-         l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ] ->
+         l = syntax_modifiers ->
            { let s = CAst.map (fun s -> "x '"^s^"' y") s in
            VernacSyntaxExtension (true,(s,l)) }
 
      | IDENT "Reserved"; IDENT "Notation";
          s = ne_lstring;
-         l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ]
+         l = syntax_modifiers
          -> { VernacSyntaxExtension (false, (s,l)) }
 
      (* "Print" "Grammar" and "Declare" "Scope" should be here but are in "command" entry in order
@@ -1196,6 +1200,11 @@ GRAMMAR EXTEND Gram
       | x = IDENT; typ = syntax_extension_type -> { SetEntryType (x,typ) }
     ] ]
   ;
+  syntax_modifiers:
+    [ [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l }
+      | -> { [] }
+    ] ]
+  ;
   syntax_extension_type:
     [ [ IDENT "ident" -> { ETIdent } | IDENT "global" -> { ETGlobal }
       | IDENT "bigint" -> { ETBigint }
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 8435612abd..e9b86f323b 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -249,9 +249,9 @@ let quote_notation_token x =
   if (n > 0 && norm) || (n > 2 && x.[0] == '\'') then "'"^x^"'"
   else x
 
-let is_numeral symbs =
-  match List.filter (function Break _ -> false | _ -> true) symbs with
-  | ([Terminal "-"; Terminal x] | [Terminal x]) ->
+let is_numeral_in_constr entry symbs =
+  match entry, List.filter (function Break _ -> false | _ -> true) symbs with
+  | InConstrEntry, ([Terminal "-"; Terminal x] | [Terminal x]) ->
       NumTok.Unsigned.parse_string x <> None
   | _ ->
       false
@@ -749,25 +749,25 @@ let pr_arg_level from (lev,typ) =
   | LevelSome -> mt () in
   Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++ pplev lev
 
-let pr_level ntn (from,fromlevel,args,typs) =
+let pr_level ntn (from,fromlevel,args) typs =
   (match from with InConstrEntry -> mt () | InCustomEntry s -> str "in " ++ str s ++ spc()) ++
   str "at level " ++ int fromlevel ++ spc () ++ str "with arguments" ++ spc() ++
   prlist_with_sep pr_comma (pr_arg_level fromlevel) (List.combine args typs)
 
-let error_incompatible_level ntn oldprec prec =
+let error_incompatible_level ntn oldprec oldtyps prec typs =
   user_err
     (str "Notation " ++ pr_notation ntn ++ str " is already defined" ++ spc() ++
-    pr_level ntn oldprec ++
+    pr_level ntn oldprec oldtyps ++
     spc() ++ str "while it is now required to be" ++ spc() ++
-    pr_level ntn prec ++ str ".")
+    pr_level ntn prec typs ++ str ".")
 
-let error_parsing_incompatible_level ntn ntn' oldprec prec =
+let error_parsing_incompatible_level ntn ntn' oldprec oldtyps prec typs =
   user_err
     (str "Notation " ++ pr_notation ntn ++ str " relies on a parsing rule for " ++ pr_notation ntn' ++ spc() ++
     str " which is already defined" ++ spc() ++
-    pr_level ntn oldprec ++
+    pr_level ntn oldprec oldtyps ++
     spc() ++ str "while it is now required to be" ++ spc() ++
-    pr_level ntn prec ++ str ".")
+    pr_level ntn prec typs ++ str ".")
 
 let warn_incompatible_format =
   CWarnings.create ~name:"notation-incompatible-format" ~category:"parsing"
@@ -780,9 +780,10 @@ let warn_incompatible_format =
        strbrk " was already defined with a different format" ++ scope ++ str ".")
 
 type syntax_parsing_extension = {
-  synext_level : Notation_gram.level;
+  synext_level : Notation.level;
   synext_notation : notation;
   synext_notgram : notation_grammar option;
+  synext_nottyps : Extend.constr_entry_key list;
 }
 
 type syntax_printing_extension = {
@@ -827,8 +828,16 @@ let check_and_extend_constr_grammar ntn rule =
     let ntn_for_grammar = rule.notgram_notation in
     if notation_eq ntn ntn_for_grammar then raise Not_found;
     let prec = rule.notgram_level in
-    let oldparsing,oldprec = Notgram_ops.level_of_notation ntn_for_grammar in
-    if not (Notgram_ops.level_eq prec oldprec) && oldparsing <> None then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec;
+    let typs = rule.notgram_typs in
+    let oldprec = Notation.level_of_notation ntn_for_grammar in
+    let oldparsing =
+      try
+        Some (Notgram_ops.grammar_of_notation ntn_for_grammar)
+      with Not_found -> None
+    in
+    let oldtyps = Notgram_ops.subentries_of_notation ntn_for_grammar in
+    if not (Notation.level_eq prec oldprec) && oldparsing <> None then
+      error_parsing_incompatible_level ntn ntn_for_grammar oldprec oldtyps prec typs;
     if oldparsing = None then raise Not_found
   with Not_found ->
     Egramcoq.extend_constr_grammar rule
@@ -839,12 +848,21 @@ let cache_one_syntax_extension (pa_se,pp_se) =
   (* Check and ensure that the level and the precomputed parsing rule is declared *)
   let oldparsing =
     try
-      let oldparsing,oldprec = Notgram_ops.level_of_notation ntn in
-      if not (Notgram_ops.level_eq prec oldprec) && (oldparsing <> None || pa_se.synext_notgram = None) then error_incompatible_level ntn oldprec prec;
+      let oldprec = Notation.level_of_notation ntn in
+      let oldparsing =
+        try
+          Some (Notgram_ops.grammar_of_notation ntn)
+        with Not_found -> None
+      in
+      let oldtyps = Notgram_ops.subentries_of_notation ntn in
+      if not (Notation.level_eq prec oldprec) && (oldparsing <> None || pa_se.synext_notgram = None) then
+        error_incompatible_level ntn oldprec oldtyps prec pa_se.synext_nottyps;
       oldparsing
     with Not_found ->
       (* Declare the level and the precomputed parsing rule *)
-      let _ = Notgram_ops.declare_notation_level ntn pa_se.synext_notgram prec in
+      let () = Notation.declare_notation_level ntn prec in
+      let () = Notgram_ops.declare_notation_subentries ntn pa_se.synext_nottyps in
+      let () = Option.iter (Notgram_ops.declare_notation_grammar ntn) pa_se.synext_notgram in
       None in
   (* Declare the parsing rule *)
   begin match oldparsing, pa_se.synext_notgram with
@@ -1009,20 +1027,14 @@ let check_binder_type recvars etyps =
                  strbrk " is only for use in recursive notations for binders.")
     | _ -> ()) etyps
 
-let not_a_syntax_modifier = function
-| SetOnlyParsing -> true
-| SetOnlyPrinting -> true
-| _ -> false
-
-let no_syntax_modifiers mods = List.for_all not_a_syntax_modifier mods
-
-let is_only_parsing mods =
-  let test = function SetOnlyParsing -> true | _ -> false in
-  List.exists test mods
-
-let is_only_printing mods =
-  let test = function SetOnlyPrinting -> true | _ -> false in
-  List.exists test mods
+let interp_non_syntax_modifiers mods =
+  let set modif (only_parsing,only_printing,entry) = match modif with
+    | SetOnlyParsing -> Some (true,only_printing,entry)
+    | SetOnlyPrinting -> Some (only_parsing,true,entry)
+    | SetCustomEntry(entry,None) -> Some (only_parsing,only_printing,InCustomEntry entry)
+    | _ -> None
+  in
+  List.fold_left (fun st modif -> Option.bind st @@ set modif) (Some (false,false,InConstrEntry)) mods
 
 (* Compute precedences from modifiers (or find default ones) *)
 
@@ -1141,33 +1153,29 @@ 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.")
 
-let make_custom_entry custom level =
-  match custom with
-  | InConstrEntry -> InConstrEntrySomeLevel
-  | InCustomEntry s -> InCustomEntryLevel (s,level)
-
 type entry_coercion_kind =
   | IsEntryCoercion of notation_entry_level
   | IsEntryGlobal of string * int
   | IsEntryIdent of string * int
 
-let is_coercion = function
-  | Some (custom,n,_,[e]) ->
+let is_coercion level typs =
+  match level, typs with
+  | Some (custom,n,_), [e] ->
      (match e, custom with
      | ETConstr _, _ ->
-         let customkey = make_custom_entry custom n in
+         let customkey = make_notation_entry_level custom n in
          let subentry = subentry_of_constr_prod_entry e in
          if notation_entry_level_eq subentry customkey then None
          else Some (IsEntryCoercion subentry)
      | ETGlobal, InCustomEntry s -> Some (IsEntryGlobal (s,n))
      | ETIdent, InCustomEntry s -> Some (IsEntryIdent (s,n))
      | _ -> None)
-  | Some _ -> assert false
-  | None -> None
+  | Some _, _ -> assert false
+  | None, _ -> None
 
-let printability level onlyparse reversibility = function
+let printability level typs onlyparse reversibility = function
 | NVar _ when reversibility = APrioriReversible ->
-  let coe = is_coercion level in
+  let coe = is_coercion level typs in
   if not onlyparse && coe = None then
     warn_notation_bound_to_variable ();
   true, coe
@@ -1229,7 +1237,7 @@ let find_precedence custom lev etyps symbols onlyprint =
       [],Option.get lev
 
 let check_curly_brackets_notation_exists () =
-  try let _ = Notgram_ops.level_of_notation (InConstrEntrySomeLevel,"{ _ }") in ()
+  try let _ = Notation.level_of_notation (InConstrEntry,"{ _ }") in ()
   with Not_found ->
     user_err Pp.(str "Notations involving patterns of the form \"{ _ }\" are treated \n\
 specially and require that the notation \"{ _ }\" is already reserved.")
@@ -1284,10 +1292,12 @@ module SynData = struct
 
     (* Notation data for parsing *)
     level         : level;
+    subentries    : constr_entry_key list;
     pa_syntax_data : subentry_types * symbol list;
     pp_syntax_data : subentry_types * symbol list;
     not_data      : notation *                   (* notation *)
-                    level *                      (* level, precedence, types *)
+                    level *                      (* level, precedence *)
+                    constr_entry_key list *
                     bool;                        (* needs_squash *)
   }
 
@@ -1328,12 +1338,11 @@ let compute_syntax_data ~local deprecation df modifiers =
 
   (* Notations for interp and grammar  *)
   let msgs,n = find_precedence mods.custom mods.level mods.etyps symbols onlyprint in
-  let custom = make_custom_entry mods.custom n in
-  let ntn_for_interp = make_notation_key custom symbols in
+  let ntn_for_interp = make_notation_key mods.custom symbols in
   let symbols_for_grammar =
-    if custom = InConstrEntrySomeLevel then remove_curly_brackets symbols else symbols in
+    if mods.custom = InConstrEntry then remove_curly_brackets symbols else symbols in
   let need_squash = not (List.equal Notation.symbol_eq symbols symbols_for_grammar) in
-  let ntn_for_grammar = if need_squash then make_notation_key custom symbols_for_grammar else ntn_for_interp in
+  let ntn_for_grammar = if need_squash then make_notation_key mods.custom symbols_for_grammar else ntn_for_interp in
   if mods.custom = InConstrEntry && not onlyprint then check_rule_productivity symbols_for_grammar;
   (* To globalize... *)
   let etyps = join_auxiliary_recursive_types recvars mods.etyps in
@@ -1348,7 +1357,7 @@ let compute_syntax_data ~local deprecation df modifiers =
   check_locality_compatibility local mods.custom sy_typs;
   let pa_sy_data = (sy_typs_for_grammar,symbols_for_grammar) in
   let pp_sy_data = (sy_typs,symbols) in
-  let sy_fulldata = (ntn_for_grammar,(mods.custom,n,prec_for_grammar,List.map snd sy_typs_for_grammar),need_squash) in
+  let sy_fulldata = (ntn_for_grammar,(mods.custom,n,prec_for_grammar),List.map snd sy_typs_for_grammar,need_squash) in
   let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in
   let i_data = ntn_for_interp, df' in
 
@@ -1367,7 +1376,8 @@ let compute_syntax_data ~local deprecation df modifiers =
     mainvars;
     intern_typs = i_typs;
 
-    level  = (mods.custom,n,prec,List.map snd sy_typs);
+    level  = (mods.custom,n,prec);
+    subentries = List.map snd sy_typs;
     pa_syntax_data = pa_sy_data;
     pp_syntax_data = pp_sy_data;
     not_data    = sy_fulldata;
@@ -1433,7 +1443,13 @@ let open_notation i (_, nobj) =
         Notation.declare_uninterpretation (NotationRule specific_ntn) pat;
       (* Declare a possible coercion *)
       (match nobj.notobj_coercion with
-      | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion specific_ntn entry
+      | 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 -> ())
@@ -1488,10 +1504,14 @@ exception NoSyntaxRule
 let recover_notation_syntax ntn =
   let pa =
     try
-      let pa_rule,prec = Notgram_ops.level_of_notation ntn in
+      let prec = Notation.level_of_notation ntn in
+      let pa_typs = Notgram_ops.subentries_of_notation ntn in
+      let pa_rule = try Some (Notgram_ops.grammar_of_notation ntn) with Not_found -> None in
       { synext_level = prec;
         synext_notation = ntn;
-        synext_notgram = pa_rule }
+        synext_notgram = pa_rule;
+        synext_nottyps = pa_typs;
+      }
     with Not_found ->
       raise NoSyntaxRule in
   let pp =
@@ -1506,7 +1526,7 @@ let recover_notation_syntax ntn =
   pa,pp
 
 let recover_squash_syntax sy =
-  let sq,_ = recover_notation_syntax (InConstrEntrySomeLevel,"{ _ }") in
+  let sq,_ = recover_notation_syntax (InConstrEntry,"{ _ }") in
   match sq.synext_notgram with
   | Some gram -> sy :: gram
   | None -> raise NoSyntaxRule
@@ -1514,7 +1534,7 @@ let recover_squash_syntax sy =
 (**********************************************************************)
 (* Main entry point for building parsing and printing rules           *)
 
-let make_pa_rule level (typs,symbols) ntn need_squash =
+let make_pa_rule level entries (typs,symbols) ntn need_squash =
   let assoc = recompute_assoc typs in
   let prod = make_production typs symbols in
   let sy = {
@@ -1522,6 +1542,7 @@ let make_pa_rule level (typs,symbols) ntn need_squash =
     notgram_assoc = assoc;
     notgram_notation = ntn;
     notgram_prods = prod;
+    notgram_typs = entries;
   } in
   (* By construction, the rule for "{ _ }" is declared, but we need to
      redeclare it because the file where it is declared needs not be open
@@ -1541,14 +1562,15 @@ let make_pp_rule level (typs,symbols) fmt =
      hunks_of_format (level, List.split typs) (symbols, parse_format fmt)
 
 let make_parsing_rules (sd : SynData.syn_data) = let open SynData in
-  let ntn_for_grammar, prec_for_grammar, need_squash = sd.not_data in
+  let ntn_for_grammar, prec_for_grammar, typs_for_grammar, need_squash = sd.not_data in
   let pa_rule =
     if sd.only_printing then None
-    else Some (make_pa_rule prec_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash)
+    else Some (make_pa_rule prec_for_grammar typs_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash)
   in {
     synext_level    = sd.level;
     synext_notation = fst sd.info;
     synext_notgram  = pa_rule;
+    synext_nottyps = typs_for_grammar;
   }
 
 let warn_irrelevant_format =
@@ -1556,7 +1578,7 @@ let warn_irrelevant_format =
     (fun () -> str "The format modifier is irrelevant for only parsing rules.")
 
 let make_printing_rules reserved (sd : SynData.syn_data) = let open SynData in
-  let custom,level,_,_ = sd.level in
+  let custom,level,_ = sd.level in
   let pp_rule = make_pp_rule level sd.pp_syntax_data sd.format in
   if sd.only_parsing then (if sd.format <> None then warn_irrelevant_format (); None)
   else Some {
@@ -1587,7 +1609,8 @@ let add_notation_in_scope ~local deprecation df env c mods scope =
   let (acvars, ac, reversibility) = interp_notation_constr env nenv c in
   let interp = make_interpretation_vars sd.recvars acvars (fst sd.pa_syntax_data) in
   let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
-  let onlyparse,coe = printability (Some sd.level) sd.only_parsing reversibility ac in
+  let onlyparse,coe = printability (Some sd.level) sd.subentries sd.only_parsing reversibility ac in
+  let notation, location = sd.info in
   let notation = {
     notobj_local = local;
     notobj_scope = scope;
@@ -1597,7 +1620,7 @@ let add_notation_in_scope ~local deprecation df env c mods scope =
     notobj_coercion = coe;
     notobj_onlyprint = sd.only_printing;
     notobj_deprecation = sd.deprecation;
-    notobj_notation = sd.info;
+    notobj_notation = (notation, location);
     notobj_specific_pp_rules = sy_pp_rules;
   } in
   let gen_sy_pp_rules =
@@ -1610,20 +1633,21 @@ let add_notation_in_scope ~local deprecation df env c mods scope =
   Lib.add_anonymous_leaf (inNotation notation);
   sd.info
 
-let add_notation_interpretation_core ~local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint deprecation =
+let add_notation_interpretation_core ~local df env ?(impls=empty_internalization_env) entry c scope onlyparse onlyprint deprecation =
   let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint df in
   (* Recover types of variables and pa/pp rules; redeclare them if needed *)
-  let level, i_typs, onlyprint, pp_sy = if not (is_numeral symbs) then begin
-    let (pa_sy,pp_sy as sy) = recover_notation_syntax (make_notation_key InConstrEntrySomeLevel symbs) in
+  let notation_key = make_notation_key entry symbs in
+  let level, i_typs, onlyprint, pp_sy = if not (is_numeral_in_constr entry symbs) then begin
+    let (pa_sy,pp_sy as sy) = recover_notation_syntax notation_key in
     let () = Lib.add_anonymous_leaf (inSyntaxExtension (local,sy)) in
     (* If the only printing flag has been explicitly requested, put it back *)
     let onlyprint = onlyprint || pa_sy.synext_notgram = None in
-    let _,_,_,typs = pa_sy.synext_level in
+    let typs = pa_sy.synext_nottyps in
     Some pa_sy.synext_level, typs, onlyprint, pp_sy
   end else None, [], false, None in
   (* Declare interpretation *)
   let path = (Lib.library_dp(), Lib.current_dirpath true) in
-  let df'  = (make_notation_key InConstrEntrySomeLevel symbs, (path,df)) in
+  let df'  = notation_key, (path,df) in
   let i_vars = make_internalization_vars recvars mainvars (List.map internalization_type_of_entry_type i_typs) in
   let nenv = {
     ninterp_var_type = to_map i_vars;
@@ -1632,7 +1656,7 @@ let add_notation_interpretation_core ~local df env ?(impls=empty_internalization
   let (acvars, ac, reversibility) = interp_notation_constr env ~impls nenv c in
   let interp = make_interpretation_vars recvars 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 onlyparse reversibility ac in
+  let onlyparse,coe = printability level i_typs onlyparse reversibility ac in
   let notation = {
     notobj_local = local;
     notobj_scope = scope;
@@ -1663,36 +1687,44 @@ let add_notation_interpretation env decl_ntn =
   let
     { decl_ntn_string = { CAst.loc ; v = df };
       decl_ntn_interp = c;
-      decl_ntn_only_parsing = onlyparse;
-      decl_ntn_scope = sc } = decl_ntn in
-  let df' = add_notation_interpretation_core ~local:false df env c sc onlyparse false None in
-  Dumpglob.dump_notation (loc,df') sc true
+      decl_ntn_modifiers = modifiers;
+      decl_ntn_scope = sc;
+    } = decl_ntn in
+  match interp_non_syntax_modifiers modifiers with
+  | None -> CErrors.user_err (str"Only modifiers not affecting parsing are supported here")
+  | Some (only_parsing,only_printing,entry) ->
+    let df' = add_notation_interpretation_core ~local:false df env entry c sc only_parsing false None in
+    Dumpglob.dump_notation (loc,df') sc true
 
 let set_notation_for_interpretation env impls decl_ntn =
   let
     { decl_ntn_string = { CAst.v = df };
       decl_ntn_interp = c;
-      decl_ntn_only_parsing = onlyparse;
-      decl_ntn_scope = sc } = decl_ntn in
-  (try ignore
-    (Flags.silently (fun () -> add_notation_interpretation_core ~local:false df env ~impls c sc onlyparse false None) ());
-  with NoSyntaxRule ->
-    user_err Pp.(str "Parsing rule for this notation has to be previously declared."));
-  Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc
+      decl_ntn_modifiers = modifiers;
+      decl_ntn_scope = sc;
+    } = decl_ntn in
+  match interp_non_syntax_modifiers modifiers with
+  | None -> CErrors.user_err (str"Only modifiers not affecting parsing are supported here")
+  | Some (only_parsing,only_printing,entry) ->
+    (try ignore
+      (Flags.silently (fun () -> add_notation_interpretation_core ~local:false df env ~impls entry c sc only_parsing false None) ());
+    with NoSyntaxRule ->
+      user_err Pp.(str "Parsing rule for this notation has to be previously declared."));
+    Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc
 
 (* Main entry point *)
 
 let add_notation ~local deprecation env c ({CAst.loc;v=df},modifiers) sc =
   let df' =
-   if no_syntax_modifiers modifiers then
+   match interp_non_syntax_modifiers modifiers with
+   | Some (only_parsing,only_printing,entry) ->
     (* No syntax data: try to rely on a previously declared rule *)
-    let onlyparse = is_only_parsing modifiers in
-    let onlyprint = is_only_printing modifiers in
-    try add_notation_interpretation_core ~local df env c sc onlyparse onlyprint deprecation
+    begin try add_notation_interpretation_core ~local df env entry c sc only_parsing only_printing deprecation
     with NoSyntaxRule ->
       (* Try to determine a default syntax rule *)
       add_notation_in_scope ~local deprecation df env c modifiers sc
-   else
+    end
+   | None ->
     (* Declare both syntax and interpretation *)
     add_notation_in_scope ~local deprecation df env c modifiers sc
   in
@@ -1701,7 +1733,7 @@ let add_notation ~local deprecation env c ({CAst.loc;v=df},modifiers) sc =
 let add_notation_extra_printing_rule df k v =
   let notk =
     let _,_, symbs = analyze_notation_tokens ~onlyprint:true df in
-    make_notation_key InConstrEntrySomeLevel symbs in
+    make_notation_key InConstrEntry symbs in
   add_notation_extra_printing_rule notk k v
 
 (* Infix notations *)
@@ -1809,7 +1841,7 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing
   let in_pat id = (id,ETConstr (Constrexpr.InConstrEntry,None,(NextLevel,0))) in
   let interp = make_interpretation_vars ~default_if_binding:AsIdentOrPattern [] acvars (List.map in_pat vars) in
   let vars = List.map (fun x -> (x, Id.Map.find x interp)) vars in
-  let onlyparsing = onlyparsing || fst (printability None false reversibility pat) in
+  let onlyparsing = onlyparsing || fst (printability None [] false reversibility pat) in
   Syntax_def.declare_syntactic_definition ~local deprecation ident ~onlyparsing (vars,pat)
 
 (**********************************************************************)
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 2c52c605b5..7af6a6a405 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -462,11 +462,11 @@ open Pputils
     let
       { decl_ntn_string = {CAst.loc;v=ntn};
         decl_ntn_interp = c;
-        decl_ntn_only_parsing = onlyparsing;
+        decl_ntn_modifiers = modifiers;
         decl_ntn_scope = scopt } = decl_ntn in
     fnl () ++ keyword "where " ++ qs ntn ++ str " := "
     ++ Flags.without_option Flags.beautify prc c
-    ++ pr_only_parsing_clause onlyparsing
+    ++ pr_syntax_modifiers modifiers
     ++ pr_opt (fun sc -> str ": " ++ str sc) scopt
 
   let pr_rec_definition { fname; univs; rec_order; binders; rtype; body_def; notations } =
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 0fdf9e2a7b..06ac7f8d48 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -137,11 +137,21 @@ type definition_expr =
   | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr
       * constr_expr option
 
+type syntax_modifier =
+  | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level
+  | SetLevel of int
+  | SetCustomEntry of string * int option
+  | SetAssoc of Gramlib.Gramext.g_assoc
+  | SetEntryType of string * Extend.simple_constr_prod_entry_key
+  | SetOnlyParsing
+  | SetOnlyPrinting
+  | SetFormat of string * lstring
+
 type decl_notation =
   { decl_ntn_string : lstring
   ; decl_ntn_interp : constr_expr
-  ; decl_ntn_only_parsing : bool
   ; decl_ntn_scope : scope_name option
+  ; decl_ntn_modifiers : syntax_modifier list
   }
 
 type 'a fix_expr_gen =
@@ -192,16 +202,6 @@ and typeclass_context = typeclass_constraint list
 type proof_expr =
   ident_decl * (local_binder_expr list * constr_expr)
 
-type syntax_modifier =
-  | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level
-  | SetLevel of int
-  | SetCustomEntry of string * int option
-  | SetAssoc of Gramlib.Gramext.g_assoc
-  | SetEntryType of string * Extend.simple_constr_prod_entry_key
-  | SetOnlyParsing
-  | SetOnlyPrinting
-  | SetFormat of string * lstring
-
 type opacity_flag = Opaque | Transparent
 
 type proof_end =