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

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

23 files changed, 314 insertions, 218 deletions

diff --git a/dev/ci/user-overlays/12523-term-notation-custom.sh b/dev/ci/user-overlays/12523-term-notation-custom.sh
new file mode 100644
index 0000000000..6217312a2a
--- /dev/null
+++ b/dev/ci/user-overlays/12523-term-notation-custom.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12523" ] || [ "$CI_BRANCH" = "fix-11121" ]; then
+
+    equations_CI_REF=fix-11121
+    equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
+
+fi
diff --git a/doc/changelog/03-notations/12523-term-notation-custom.rst b/doc/changelog/03-notations/12523-term-notation-custom.rst
new file mode 100644
index 0000000000..1a611f3fb1
--- /dev/null
+++ b/doc/changelog/03-notations/12523-term-notation-custom.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  Simultaneous definition of terms and notations now support custom entries.
+  Fixes `#11121 <https://github.com/coq/coq/pull/11121>`_.
+  (`#12523 <https://github.com/coq/coq/pull/11523>`_, by Maxime Dénès).
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 3c92206fd2..fcd5ecc070 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -368,13 +368,14 @@ a :token:`decl_notations` clause after the definition of the (co)inductive type
 (co)recursive term (or after the definition of each of them in case of mutual
 definitions). The exact syntax is given by :n:`@decl_notation` for inductive,
 co-inductive, recursive and corecursive definitions and in :ref:`record-types`
-for records.
+for records. Note that only syntax modifiers that do not require to add or
+change a parsing rule are accepted.
 
    .. insertprodn decl_notations decl_notation
 
    .. prodn::
       decl_notations ::= where @decl_notation {* and @decl_notation }
-      decl_notation ::= @string := @one_term {? ( only parsing ) } {? : @scope_name }
+      decl_notation ::= @string := @one_term {? ( {+, @syntax_modifier } ) } {? : @scope_name }
 
 Here are examples:
 
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 21f682ac0e..9c4b78f4ed 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -29,10 +29,10 @@ type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of strin
 type notation_key = string
 
 (* A notation associated to a given parsing rule *)
-type notation = notation_entry_level * notation_key
+type notation = notation_entry * notation_key
 
 (* A notation associated to a given interpretation *)
-type specific_notation = notation_with_optional_scope * notation
+type specific_notation = notation_with_optional_scope * (notation_entry * notation_key)
 
 type 'a or_by_notation_r =
   | AN of 'a
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 63079993c8..b087431e85 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -359,14 +359,14 @@ let make_notation_gen loc ntn mknot mkprim destprim l bl =
     (* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *)
     | "- _", [Some (Numeral p)] when not (NumTok.Signed.is_zero p) ->
         assert (bl=[]);
-        mknot (loc,ntn,([mknot (loc,(InConstrEntrySomeLevel,"( _ )"),l,[])]),[])
+        mknot (loc,ntn,([mknot (loc,(InConstrEntry,"( _ )"),l,[])]),[])
     | _ ->
         match decompose_notation_key ntn, l with
-        | (InConstrEntrySomeLevel,[Terminal "-"; Terminal x]), [] ->
+        | (InConstrEntry,[Terminal "-"; Terminal x]), [] ->
            begin match NumTok.Unsigned.parse_string x with
            | Some n -> mkprim (loc, Numeral (NumTok.SMinus,n))
            | None -> mknot (loc,ntn,l,bl) end
-        | (InConstrEntrySomeLevel,[Terminal x]), [] ->
+        | (InConstrEntry,[Terminal x]), [] ->
            begin match NumTok.Unsigned.parse_string x with
            | Some n -> mkprim (loc, Numeral (NumTok.SPlus,n))
            | None -> mknot (loc,ntn,l,bl) end
@@ -486,7 +486,13 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(no_implicit,nb_to_drop
   function
     | NotationRule (_,ntn as specific_ntn) ->
       begin
-        match availability_of_entry_coercion custom (fst ntn) with
+        let notation_entry_level = match (fst ntn) with
+          | InConstrEntry -> InConstrEntrySomeLevel
+          | InCustomEntry s ->
+            let (_,level,_) = Notation.level_of_notation ntn in
+            InCustomEntryLevel (s, level)
+        in
+        match availability_of_entry_coercion custom notation_entry_level with
         | None -> raise No_match
         | Some coercion ->
         match availability_of_notation specific_ntn (tmp_scope,scopes) with
@@ -1260,7 +1266,13 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
         (* Try availability of interpretation ... *)
         match keyrule with
           | NotationRule (_,ntn as specific_ntn) ->
-             (match availability_of_entry_coercion custom (fst ntn) with
+            let notation_entry_level = match (fst ntn) with
+              | InConstrEntry -> InConstrEntrySomeLevel
+              | InCustomEntry s ->
+                let (_,level,_) = Notation.level_of_notation ntn in
+                InCustomEntryLevel (s, level)
+             in
+             (match availability_of_entry_coercion custom notation_entry_level with
              | None -> raise No_match
              | Some coercion ->
                match availability_of_notation specific_ntn scopes with
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ee041ed088..d95554de56 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -224,35 +224,35 @@ let expand_notation_string ntn n =
 (* Remark: expansion of squash at definition is done in metasyntax.ml *)
 let contract_curly_brackets ntn (l,ll,bl,bll) =
   match ntn with
-  | InCustomEntryLevel _,_ -> ntn,(l,ll,bl,bll)
-  | InConstrEntrySomeLevel, ntn ->
+  | InCustomEntry _,_ -> ntn,(l,ll,bl,bll)
+  | InConstrEntry, ntn ->
   let ntn' = ref ntn in
   let rec contract_squash n = function
     | [] -> []
-    | { CAst.v = CNotation (None,(InConstrEntrySomeLevel,"{ _ }"),([a],[],[],[])) } :: l ->
+    | { CAst.v = CNotation (None,(InConstrEntry,"{ _ }"),([a],[],[],[])) } :: l ->
         ntn' := expand_notation_string !ntn' n;
         contract_squash n (a::l)
     | a :: l ->
         a::contract_squash (n+1) l in
   let l = contract_squash 0 l in
   (* side effect; don't inline *)
-  (InConstrEntrySomeLevel,!ntn'),(l,ll,bl,bll)
+  (InConstrEntry,!ntn'),(l,ll,bl,bll)
 
 let contract_curly_brackets_pat ntn (l,ll) =
   match ntn with
-  | InCustomEntryLevel _,_ -> ntn,(l,ll)
-  | InConstrEntrySomeLevel, ntn ->
+  | InCustomEntry _,_ -> ntn,(l,ll)
+  | InConstrEntry, ntn ->
   let ntn' = ref ntn in
   let rec contract_squash n = function
     | [] -> []
-    | { CAst.v = CPatNotation (None,(InConstrEntrySomeLevel,"{ _ }"),([a],[]),[]) } :: l ->
+    | { CAst.v = CPatNotation (None,(InConstrEntry,"{ _ }"),([a],[]),[]) } :: l ->
         ntn' := expand_notation_string !ntn' n;
         contract_squash n (a::l)
     | a :: l ->
         a::contract_squash (n+1) l in
   let l = contract_squash 0 l in
   (* side effect; don't inline *)
-  (InConstrEntrySomeLevel,!ntn'),(l,ll)
+  (InConstrEntry,!ntn'),(l,ll)
 
 type intern_env = {
   ids: Names.Id.Set.t;
@@ -1688,11 +1688,11 @@ let drop_notations_pattern looked_for genv =
         (* but not scopes in expl_pl *)
         let (argscs1,_) = find_remaining_scopes expl_pl pl g in
         DAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
-    | CPatNotation (_,(InConstrEntrySomeLevel,"- _"),([a],[]),[]) when is_non_zero_pat a ->
+    | CPatNotation (_,(InConstrEntry,"- _"),([a],[]),[]) when is_non_zero_pat a ->
       let p = match a.CAst.v with CPatPrim (Numeral (_, p)) -> p | _ -> assert false in
       let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (SMinus,p)) scopes in
       rcp_of_glob scopes pat
-    | CPatNotation (_,(InConstrEntrySomeLevel,"( _ )"),([a],[]),[]) ->
+    | CPatNotation (_,(InConstrEntry,"( _ )"),([a],[]),[]) ->
       in_pat top scopes a
     | CPatNotation (_,ntn,fullargs,extrargs) ->
       let ntn,(terms,termlists) = contract_curly_brackets_pat ntn fullargs in
@@ -2006,10 +2006,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         DAst.make ?loc @@
         GLetIn (na.CAst.v, inc1, int,
           intern_restart_binders (push_name_env ntnvars (impls_term_list 1 inc1) env na) c2)
-    | CNotation (_,(InConstrEntrySomeLevel,"- _"), ([a],[],[],[])) when is_non_zero a ->
+    | CNotation (_,(InConstrEntry,"- _"), ([a],[],[],[])) when is_non_zero a ->
       let p = match a.CAst.v with CPrim (Numeral (_, p)) -> p | _ -> assert false in
        intern env (CAst.make ?loc @@ CPrim (Numeral (SMinus,p)))
-    | CNotation (_,(InConstrEntrySomeLevel,"( _ )"),([a],[],[],[])) -> intern env a
+    | CNotation (_,(InConstrEntry,"( _ )"),([a],[],[],[])) -> intern env a
     | CNotation (_,ntn,args) ->
         let c = intern_notation intern env ntnvars loc ntn args in
         let x, impl, scopes = find_appl_head_data c in
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 57ec708b07..d57c05788d 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -207,7 +207,7 @@ let cook_notation (from,df) sc =
   done;
   let df = Bytes.sub_string ntn 0 !j in
   let df_sc = match sc with Some sc -> ":" ^ sc ^ ":" ^ df | _ -> "::" ^ df in
-  let from_df_sc = match from with Constrexpr.InCustomEntryLevel (from,_) -> ":" ^ from ^ df_sc | Constrexpr.InConstrEntrySomeLevel -> ":" ^ df_sc in
+  let from_df_sc = match from with Constrexpr.InCustomEntry from -> ":" ^ from ^ df_sc | Constrexpr.InConstrEntry -> ":" ^ df_sc in
   from_df_sc
 
 let dump_notation_location posl df (((path,secpath),_),sc) =
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 3d29da025e..4016a3600e 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -92,7 +92,7 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
   let rec aux bdvars l c = match CAst.(c.v) with
     | CRef (qid,_) when qualid_is_ident qid ->
       found c.CAst.loc (qualid_basename qid) bdvars l
-    | CNotation (_,(InConstrEntrySomeLevel,"{ _ : _ | _ }"), ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when
+    | CNotation (_,(InConstrEntry,"{ _ : _ | _ }"), ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when
         qualid_is_ident qid && not (Id.Set.mem (qualid_basename qid) bdvars) ->
         Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add (qualid_basename qid) bdvars) l c
     | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c
diff --git a/interp/notation.ml b/interp/notation.ml
index d4a44d9622..e282d62396 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -56,9 +56,9 @@ let notation_with_optional_scope_eq inscope1 inscope2 = match (inscope1,inscope2
  | (LastLonelyNotation | NotationInScope _), _ -> false
 
 let notation_eq (from1,ntn1) (from2,ntn2) =
-  notation_entry_level_eq from1 from2 && String.equal ntn1 ntn2
+  notation_entry_eq from1 from2 && String.equal ntn1 ntn2
 
-let pr_notation (from,ntn) = qstring ntn ++ match from with InConstrEntrySomeLevel -> mt () | InCustomEntryLevel (s,n) -> str " in custom " ++ str s
+let pr_notation (from,ntn) = qstring ntn ++ match from with InConstrEntry -> mt () | InCustomEntry s -> str " in custom " ++ str s
 
 module NotationOrd =
   struct
@@ -337,6 +337,33 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
   | NApp (_,args) -> Oth, Some (List.length args)
   | _ -> Oth, None
 
+(** Dealing with precedences *)
+
+type level = notation_entry * entry_level * entry_relative_level list
+  (* first argument is InCustomEntry s for custom entries *)
+
+let entry_relative_level_eq t1 t2 = match t1, t2 with
+| LevelLt n1, LevelLt n2 -> Int.equal n1 n2
+| LevelLe n1, LevelLe n2 -> Int.equal n1 n2
+| LevelSome, LevelSome -> true
+| (LevelLt _ | LevelLe _ | LevelSome), _ -> false
+
+let level_eq (s1, l1, t1) (s2, l2, t2) =
+  notation_entry_eq s1 s2 && Int.equal l1 l2 && List.equal entry_relative_level_eq t1 t2
+
+let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty
+
+let declare_notation_level ntn level =
+  try
+    let _ = NotationMap.find ntn !notation_level_map in
+    anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.")
+  with Not_found ->
+  notation_level_map := NotationMap.add ntn level !notation_level_map
+
+let level_of_notation ntn =
+  NotationMap.find ntn !notation_level_map
+
+
 (**********************************************************************)
 (* Interpreting numbers (not in summary because functional objects)   *)
 
@@ -1228,8 +1255,8 @@ let find_notation ntn sc =
   NotationMap.find ntn (find_scope sc).notations
 
 let notation_of_prim_token = function
-  | Constrexpr.Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.Unsigned.sprint n
-  | Constrexpr.Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^NumTok.Unsigned.sprint n
+  | Constrexpr.Numeral (SPlus,n) -> InConstrEntry, NumTok.Unsigned.sprint n
+  | Constrexpr.Numeral (SMinus,n) -> InConstrEntry, "- "^NumTok.Unsigned.sprint n
   | String _ -> raise Not_found
 
 let find_prim_token check_allowed ?loc p sc =
@@ -1256,7 +1283,7 @@ let find_prim_token check_allowed ?loc p sc =
 
 let interp_prim_token_gen ?loc g p local_scopes =
   let scopes = make_current_scopes local_scopes in
-  let p_as_ntn = try notation_of_prim_token p with Not_found -> InConstrEntrySomeLevel,"" in
+  let p_as_ntn = try notation_of_prim_token p with Not_found -> InConstrEntry,"" in
   try
     let (pat,loc), sc = find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes in
     pat, (loc,sc)
@@ -1336,7 +1363,8 @@ module EntryCoercionOrd =
 
 module EntryCoercionMap = Map.Make(EntryCoercionOrd)
 
-let entry_coercion_map = ref EntryCoercionMap.empty
+let entry_coercion_map : (((entry_level option * entry_level option) * entry_coercion) list EntryCoercionMap.t) ref =
+  ref EntryCoercionMap.empty
 
 let level_ord lev lev' =
   match lev, lev' with
@@ -1349,13 +1377,18 @@ let rec search nfrom nto = function
   | ((pfrom,pto),coe)::l ->
     if level_ord pfrom nfrom && level_ord nto pto then coe else search nfrom nto l
 
-let decompose_custom_entry = function
+let make_notation_entry_level entry level =
+  match entry with
+  | InConstrEntry -> InConstrEntrySomeLevel
+  | InCustomEntry s -> InCustomEntryLevel (s,level)
+
+let decompose_notation_entry_level = function
   | InConstrEntrySomeLevel -> InConstrEntry, None
   | InCustomEntryLevel (s,n) -> InCustomEntry s, Some n
 
 let availability_of_entry_coercion entry entry' =
-  let entry, lev = decompose_custom_entry entry in
-  let entry', lev' = decompose_custom_entry entry' in
+  let entry, lev = decompose_notation_entry_level entry in
+  let entry', lev' = decompose_notation_entry_level entry' in
   if notation_entry_eq entry entry' && level_ord lev' lev then Some []
   else
     try Some (search lev lev' (EntryCoercionMap.find (entry,entry') !entry_coercion_map))
@@ -1377,28 +1410,27 @@ let rec insert_coercion_path path = function
       else if shorter_path path path' then path::allpaths
       else path'::insert_coercion_path path paths
 
-let declare_entry_coercion (scope,(entry,_) as specific_ntn) entry' =
-  let entry, lev = decompose_custom_entry entry in
-  let entry', lev' = decompose_custom_entry entry' in
+let declare_entry_coercion (scope,(entry,key)) lev entry' =
+  let entry', lev' = decompose_notation_entry_level entry' in
   (* Transitive closure *)
   let toaddleft =
     EntryCoercionMap.fold (fun (entry'',entry''') paths l ->
         List.fold_right (fun ((lev'',lev'''),path) l ->
         if notation_entry_eq entry entry''' && level_ord lev lev''' &&
            not (notation_entry_eq entry' entry'')
-        then ((entry'',entry'),((lev'',lev'),path@[specific_ntn]))::l else l) paths l)
+        then ((entry'',entry'),((lev'',lev'),path@[(scope,(entry,key))]))::l else l) paths l)
       !entry_coercion_map [] in
   let toaddright =
     EntryCoercionMap.fold (fun (entry'',entry''') paths l ->
         List.fold_right (fun ((lev'',lev'''),path) l ->
         if entry' = entry'' && level_ord lev' lev'' && entry <> entry'''
-        then ((entry,entry'''),((lev,lev'''),path@[specific_ntn]))::l else l) paths l)
+        then ((entry,entry'''),((lev,lev'''),path@[(scope,(entry,key))]))::l else l) paths l)
       !entry_coercion_map [] in
   entry_coercion_map :=
     List.fold_right (fun (pair,path) ->
         let olds = try EntryCoercionMap.find pair !entry_coercion_map with Not_found -> [] in
         EntryCoercionMap.add pair (insert_coercion_path path olds))
-      (((entry,entry'),((lev,lev'),[specific_ntn]))::toaddright@toaddleft)
+      (((entry,entry'),((lev,lev'),[(scope,(entry,key))]))::toaddright@toaddleft)
       !entry_coercion_map
 
 let entry_has_global_map = ref String.Map.empty
diff --git a/interp/notation.mli b/interp/notation.mli
index e7e917463b..c39bfa6e28 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -298,8 +298,8 @@ type symbol =
 val symbol_eq : symbol -> symbol -> bool
 
 (** Make/decompose a notation of the form "_ U _" *)
-val make_notation_key : notation_entry_level -> symbol list -> notation
-val decompose_notation_key : notation -> notation_entry_level * symbol list
+val make_notation_key : notation_entry -> symbol list -> notation
+val decompose_notation_key : notation -> notation_entry * symbol list
 
 (** Decompose a notation of the form "a 'U' b" *)
 val decompose_raw_notation : string -> symbol list
@@ -313,8 +313,10 @@ val locate_notation : (glob_constr -> Pp.t) -> notation_key ->
 
 val pr_visibility: (glob_constr -> Pp.t) -> scope_name option -> Pp.t
 
+val make_notation_entry_level : notation_entry -> entry_level -> notation_entry_level
+
 type entry_coercion = (notation_with_optional_scope * notation) list
-val declare_entry_coercion : specific_notation -> notation_entry_level -> unit
+val declare_entry_coercion : specific_notation -> entry_level option -> notation_entry_level -> unit
 val availability_of_entry_coercion : notation_entry_level -> notation_entry_level -> entry_coercion option
 
 val declare_custom_entry_has_global : string -> int -> unit
@@ -323,6 +325,20 @@ val declare_custom_entry_has_ident : string -> int -> unit
 val entry_has_global : notation_entry_level -> bool
 val entry_has_ident : notation_entry_level -> bool
 
+(** Dealing with precedences *)
+
+type level = notation_entry * entry_level * entry_relative_level list
+  (* first argument is InCustomEntry s for custom entries *)
+
+val level_eq : level -> level -> bool
+val entry_relative_level_eq : entry_relative_level -> entry_relative_level -> bool
+
+(** {6 Declare and test the level of a (possibly uninterpreted) notation } *)
+
+val declare_notation_level : notation -> level -> unit
+val level_of_notation : notation -> level
+  (** raise [Not_found] if not declared *)
+
 (** Rem: printing rules for primitive token are canonical *)
 
 val with_notation_protection : ('a -> 'b) -> 'a -> 'b
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index c19dd00b38..429e740403 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -165,11 +165,11 @@ GRAMMAR EXTEND Gram
              collapse -(3) into the numeral -3. *)
           (match c.CAst.v with
             | CPrim (Numeral (NumTok.SPlus,n)) ->
-                CAst.make ~loc @@ CNotation(None,(InConstrEntrySomeLevel,"( _ )"),([c],[],[],[]))
+                CAst.make ~loc @@ CNotation(None,(InConstrEntry,"( _ )"),([c],[],[],[]))
             | _ -> c) }
       | "{|"; c = record_declaration; bar_cbrace -> { c }
       | "{"; c = binder_constr ; "}" ->
-        { CAst.make ~loc @@ CNotation(None,(InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) }
+        { CAst.make ~loc @@ CNotation(None,(InConstrEntry,"{ _ }"),([c],[],[],[])) }
       | "`{"; c = operconstr LEVEL "200"; "}" ->
         { CAst.make ~loc @@ CGeneralization (MaxImplicit, None, c) }
       | "`("; c = operconstr LEVEL "200"; ")" ->
@@ -346,7 +346,7 @@ GRAMMAR EXTEND Gram
              collapse -(3) into the numeral -3. *)
           match p.CAst.v with
           | CPatPrim (Numeral (NumTok.SPlus,n)) ->
-              CAst.make ~loc @@ CPatNotation(None,(InConstrEntrySomeLevel,"( _ )"),([p],[]),[])
+              CAst.make ~loc @@ CPatNotation(None,(InConstrEntry,"( _ )"),([p],[]),[])
           | _ -> p }
       | "("; p = pattern LEVEL "200"; "|" ; pl = LIST1 pattern LEVEL "200" SEP "|"; ")" ->
         { CAst.make ~loc @@ CPatOr (p::pl) }
diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml
index 7940931dfc..045f497070 100644
--- a/parsing/notation_gram.ml
+++ b/parsing/notation_gram.ml
@@ -9,13 +9,6 @@
 (************************************************************************)
 
 open Names
-open Extend
-open Constrexpr
-
-(** Dealing with precedences *)
-
-type level = notation_entry * entry_level * entry_relative_level list * constr_entry_key list
-  (* first argument is InCustomEntry s for custom entries *)
 
 type grammar_constr_prod_item =
   | GramConstrTerminal of string Tok.p
@@ -28,10 +21,11 @@ type grammar_constr_prod_item =
 (** Grammar rules for a notation *)
 
 type one_notation_grammar = {
-  notgram_level : level;
+  notgram_level : Notation.level;
   notgram_assoc : Gramlib.Gramext.g_assoc option;
   notgram_notation : Constrexpr.notation;
   notgram_prods : grammar_constr_prod_item list list;
+  notgram_typs : Extend.constr_entry_key list;
 }
 
 type notation_grammar = one_notation_grammar list
diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
index 1d18e7dcfa..74ced431c9 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -12,63 +12,33 @@ open Pp
 open CErrors
 open Util
 open Notation
-open Constrexpr
 
-(* Register the level of notation for parsing and printing
+(* Register the grammar of notation for parsing and printing
    (also register the parsing rule if not onlyprinting) *)
 
-let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty
+let notation_grammar_map = Summary.ref ~name:"notation_grammar_map" NotationMap.empty
 
-let declare_notation_level ntn parsing_rule level =
+let declare_notation_grammar ntn rule =
   try
-    let _ = NotationMap.find ntn !notation_level_map in
-    anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.")
+    let _ = NotationMap.find ntn !notation_grammar_map in
+    anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a grammar.")
   with Not_found ->
-  notation_level_map := NotationMap.add ntn (parsing_rule,level) !notation_level_map
+  notation_grammar_map := NotationMap.add ntn rule !notation_grammar_map
 
-let level_of_notation ntn =
-  NotationMap.find ntn !notation_level_map
+let grammar_of_notation ntn =
+  NotationMap.find ntn !notation_grammar_map
 
-let get_defined_notations () =
-  NotationSet.elements @@ NotationMap.domain !notation_level_map
-
-(**********************************************************************)
-(* Equality *)
-
-open Extend
-
-let entry_relative_level_eq t1 t2 = match t1, t2 with
-| LevelLt n1, LevelLt n2 -> Int.equal n1 n2
-| LevelLe n1, LevelLe n2 -> Int.equal n1 n2
-| LevelSome, LevelSome -> true
-| (LevelLt _ | LevelLe _ | LevelSome), _ -> false
-
-let production_position_eq pp1 pp2 = match (pp1,pp2) with
-| BorderProd (side1,assoc1), BorderProd (side2,assoc2) -> side1 = side2 && assoc1 = assoc2
-| InternalProd, InternalProd -> true
-| (BorderProd _ | InternalProd), _ -> false
+let notation_subentries_map = Summary.ref ~name:"notation_subentries_map" NotationMap.empty
 
-let production_level_eq l1 l2 = match (l1,l2) with
-| NextLevel, NextLevel -> true
-| NumLevel n1, NumLevel n2 -> Int.equal n1 n2
-| DefaultLevel, DefaultLevel -> true
-| (NextLevel | NumLevel _ | DefaultLevel), _ -> false
-
-let constr_entry_key_eq eq v1 v2 = match v1, v2 with
-| ETIdent, ETIdent -> true
-| ETGlobal, ETGlobal -> true
-| ETBigint, ETBigint -> true
-| ETBinder b1, ETBinder b2 -> b1 == b2
-| ETConstr (s1,bko1,lev1), ETConstr (s2,bko2,lev2) ->
-   notation_entry_eq s1 s2 && eq lev1 lev2 && Option.equal (=) bko1 bko2
-| ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2
-| (ETIdent | ETGlobal | ETBigint | ETBinder _ | ETConstr _ | ETPattern _), _ -> false
+let declare_notation_subentries ntn entries =
+  try
+    let _ = NotationMap.find ntn !notation_grammar_map in
+    anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a grammar.")
+  with Not_found ->
+  notation_subentries_map := NotationMap.add ntn entries !notation_subentries_map
 
-let level_eq_gen strict (s1, l1, t1, u1) (s2, l2, t2, u2) =
-  let prod_eq (l1,pp1) (l2,pp2) =
-    not strict ||
-    (production_level_eq l1 l2 && production_position_eq pp1 pp2) in
-  notation_entry_eq s1 s2 && Int.equal l1 l2 && List.equal entry_relative_level_eq t1 t2
-  && List.equal (constr_entry_key_eq prod_eq) u1 u2
+let subentries_of_notation ntn =
+  NotationMap.find ntn !notation_subentries_map
 
-let level_eq = level_eq_gen false
+let get_defined_notations () =
+  NotationSet.elements @@ NotationMap.domain !notation_grammar_map
diff --git a/parsing/notgram_ops.mli b/parsing/notgram_ops.mli
index dd1375a1f1..15b8717705 100644
--- a/parsing/notgram_ops.mli
+++ b/parsing/notgram_ops.mli
@@ -12,14 +12,14 @@
 open Constrexpr
 open Notation_gram
 
-val level_eq : level -> level -> bool
-val entry_relative_level_eq : entry_relative_level -> entry_relative_level -> bool
+(** {6 Declare the parsing rules and entries of a (possibly uninterpreted) notation } *)
 
-(** {6 Declare and test the level of a (possibly uninterpreted) notation } *)
-
-val declare_notation_level : notation -> notation_grammar option -> level -> unit
-val level_of_notation : notation -> notation_grammar option * level
+val declare_notation_grammar : notation -> notation_grammar -> unit
+val grammar_of_notation : notation -> notation_grammar
   (** raise [Not_found] if not declared *)
 
+val declare_notation_subentries : notation -> Extend.constr_entry_key list -> unit
+val subentries_of_notation : notation -> Extend.constr_entry_key list
+
 (** Returns notations with defined parsing/printing rules *)
 val get_defined_notations : unit -> notation list
diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml
index b888614ecb..fe6e8360c1 100644
--- a/parsing/ppextend.ml
+++ b/parsing/ppextend.ml
@@ -13,7 +13,6 @@ open Pp
 open CErrors
 open Notation
 open Constrexpr
-open Notgram_ops
 
 (*s Pretty-print. *)
 
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 162013c556..1ed632f03f 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -859,7 +859,7 @@ let glob_cpattern gs p =
   | k, (v, Some t), _ as orig ->
      if k = 'x' then glob_ssrterm gs ('(', (v, Some t), None) else
      match t.CAst.v with
-     | CNotation(_,(InConstrEntrySomeLevel,"( _ in _ )"), ([t1; t2], [], [], [])) ->
+     | CNotation(_,(InConstrEntry,"( _ in _ )"), ([t1; t2], [], [], [])) ->
          (try match glob t1, glob t2 with
          | (r1, None), (r2, None) -> encode k "In" [r1;r2]
          | (r1, Some _), (r2, Some _) when isCVar t1 ->
@@ -867,11 +867,11 @@ let glob_cpattern gs p =
          | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2]
          | _ -> CErrors.anomaly (str"where are we?.")
          with _ when isCVar t1 -> encode k "In" [bind_in t1 t2])
-     | CNotation(_,(InConstrEntrySomeLevel,"( _ in _ in _ )"), ([t1; t2; t3], [], [], [])) ->
+     | CNotation(_,(InConstrEntry,"( _ in _ in _ )"), ([t1; t2; t3], [], [], [])) ->
          check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3]
-     | CNotation(_,(InConstrEntrySomeLevel,"( _ as _ )"), ([t1; t2], [], [], [])) ->
+     | CNotation(_,(InConstrEntry,"( _ as _ )"), ([t1; t2], [], [], [])) ->
          encode k "As" [fst (glob t1); fst (glob t2)]
-     | CNotation(_,(InConstrEntrySomeLevel,"( _ as _ in _ )"), ([t1; t2; t3], [], [], [])) ->
+     | CNotation(_,(InConstrEntry,"( _ as _ in _ )"), ([t1; t2; t3], [], [], [])) ->
          check_var t2; encode k "As" [fst (glob t1); bind_in t2 t3]
      | _ -> glob_ssrterm gs orig
 ;;
diff --git a/plugins/ssrsearch/g_search.mlg b/plugins/ssrsearch/g_search.mlg
index f5cbf2005b..5e002e09cc 100644
--- a/plugins/ssrsearch/g_search.mlg
+++ b/plugins/ssrsearch/g_search.mlg
@@ -59,7 +59,7 @@ let interp_search_notation ?loc tag okey =
          (Bytes.set s' i' '_'; loop (j + 1) (i' + 2))
       else (String.blit s i s' i' m; loop (j + 1) (i' + m + 1)) in
     loop 0 1 in
-  let trim_ntn (pntn, m) = (InConstrEntrySomeLevel,Bytes.sub_string pntn 1 (max 0 m)) in
+  let trim_ntn (pntn, m) = (InConstrEntry,Bytes.sub_string pntn 1 (max 0 m)) in
   let pr_ntn ntn = str "(" ++ Notation.pr_notation ntn ++ str ")" in
   let pr_and_list pr = function
     | [x] -> pr x
diff --git a/test-suite/bugs/closed/bug_11121.v b/test-suite/bugs/closed/bug_11121.v
new file mode 100644
index 0000000000..6112a443ab
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11121.v
@@ -0,0 +1,21 @@
+Declare Custom Entry example.
+
+Module M1.
+Fixpoint stupid (x : nat) : nat := 1.
+Reserved Notation " x '==' 1 " (in custom example at level 0, x constr).
+Notation " x '==' 1" := (stupid x) (in custom example).
+End M1.
+
+Module M2.
+Fixpoint stupid (x : nat) : nat := 1.
+Notation " x '==' 1" := (stupid x) (in custom example at level 0).
+Fail Notation " x '==' 1" := (stupid x) (in custom example at level 1).
+End M2.
+
+Module M3.
+Reserved Notation " x '==' 1 " (in custom example at level 55, x constr).
+
+Fixpoint stupid (x : nat) : nat := 1
+where " x '==' 1" := (stupid x) (in custom example).
+
+End M3.
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 =