From 99ed5732f576b3ebf68c83c84c8295df55b12e02 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Thu, 6 Jul 2023 21:26:00 +0200
Subject: [PATCH] A notation cleanup suggested in #17117: using records in
 place of tuples.

See comment at https://github.com/coq/coq/pull/17117#discussion_r1107287149.
---
 interp/constrexpr.mli     | 11 ++++++++--
 interp/constrextern.ml    | 42 ++++++++++++++++++++------------------
 interp/notation.ml        | 42 +++++++++++++++++++++++---------------
 interp/notation_ops.ml    | 16 ++++++++++-----
 interp/notation_ops.mli   |  8 ++++++++
 interp/notationextern.ml  | 15 ++++++++------
 interp/notationextern.mli |  4 ++--
 vernac/egramcoq.ml        | 43 +++++++++++++++++++++------------------
 vernac/metasyntax.ml      | 31 ++++++++++++++--------------
 9 files changed, 125 insertions(+), 87 deletions(-)

diff --git a/interp/constrexpr.mli b/interp/constrexpr.mli
index 25a4682f5c44..8a4ec8014466 100644
--- a/interp/constrexpr.mli
+++ b/interp/constrexpr.mli
@@ -45,10 +45,17 @@ type entry_relative_level = LevelLt of entry_level | LevelLe of entry_level | Le
 type notation_entry = InConstrEntry | InCustomEntry of string
 
 (* A notation entry with the level where the notation lives *)
-type notation_entry_level = notation_entry * entry_level
+type notation_entry_level = {
+  notation_entry : notation_entry;
+  notation_level : entry_level;
+}
 
 (* Notation subentries, to be associated to the variables of the notation *)
-type notation_entry_relative_level = notation_entry * (entry_relative_level * side option)
+type notation_entry_relative_level = {
+  notation_subentry : notation_entry;
+  notation_relative_level : entry_relative_level;
+  notation_position : side option;
+}
 
 type notation_key = string
 
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index de3b92545e4e..3d33cbbe1ae0 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -219,9 +219,11 @@ let rec fill_arg_scopes args subscopes (entry,(_,scopes) as all) =
   | a :: args, [] ->
     (a, (entry, ([], scopes))) :: fill_arg_scopes args [] all
 
-let update_with_subscope ((entry,(lev,side)),(scopt,scl)) scopes =
+let update_with_subscope (entry,(scopt,scl)) scopes =
+  let {notation_subentry = entry; notation_relative_level = lev; notation_position = side} = entry in
   let lev = if !print_parentheses && side <> None then LevelLe 0 (* min level *) else lev in
-  ((entry,(lev,side)),(scopt,scl@scopes))
+  let subentry' = {notation_subentry = entry; notation_relative_level = lev; notation_position = side} in
+  (subentry',(scopt,scl@scopes))
 
 (**********************************************************************)
 (* mapping patterns to cases_pattern_expr                                *)
@@ -334,12 +336,12 @@ let extern_record_pattern cstrsp args =
   with
     Not_found | No_match | Exit -> None
 
- (* Better to use extern_glob_constr composed with injection/retraction ?? *)
+(* Better to use extern_glob_constr composed with injection/retraction ?? *)
 let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
   try
     if !Flags.in_debugger || !Flags.raw_print || !print_raw_literal then raise No_match;
     let (na,p,key) = uninterp_prim_token_cases_pattern pat scopes in
-    match availability_of_entry_coercion custom (InConstrEntry,0) with
+    match availability_of_entry_coercion custom constr_lowest_level with
       | None -> raise No_match
       | Some coercion ->
         let loc = cases_pattern_loc pat in
@@ -356,10 +358,10 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
     | PatVar (Name id) when entry_has_global custom || entry_has_ident custom ->
       CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id)))
     | pat ->
-    match availability_of_entry_coercion custom (InConstrEntry,0) with
+    match availability_of_entry_coercion custom constr_lowest_level with
     | None -> raise No_match
     | Some coercion ->
-      let allscopes = ((InConstrEntry,(LevelSome,None)),scopes) in
+      let allscopes = (constr_some_level,scopes) in
       let pat = match pat with
         | PatVar (Name id) -> CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id)))
         | PatVar (Anonymous) -> CAst.make ?loc (CPatAtom None)
@@ -389,7 +391,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(no_implicit,nb_to_drop
   match rule with
     | NotationRule (_,ntn as specific_ntn) ->
       begin
-        let entry = (fst ntn, pi2 (Notation.level_of_notation ntn)) in
+        let entry = fst (Notation.level_of_notation ntn) in
         match availability_of_entry_coercion custom entry with
         | None -> raise No_match
         | Some coercion ->
@@ -425,7 +427,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(no_implicit,nb_to_drop
                  (make_pat_notation ?loc specific_ntn (l,ll) l2') key)
       end
     | AbbrevRule kn ->
-      match availability_of_entry_coercion custom (InConstrEntry, 0) with
+      match availability_of_entry_coercion custom constr_lowest_level with
       | None -> raise No_match
       | Some coercion ->
       let qid = Nametab.shortest_qualid_of_abbreviation ?loc vars kn in
@@ -493,7 +495,7 @@ let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args =
            |None           -> CAst.make @@ CPatCstr (c, Some args, [])
 
 let extern_cases_pattern vars p =
-  extern_cases_pattern_in_scope ((InConstrEntry,(LevelSome (*??*),None)),([],[])) vars p
+  extern_cases_pattern_in_scope (constr_some_level,([],[])) vars p
 
 (**********************************************************************)
 (* Externalising applications *)
@@ -749,7 +751,7 @@ let same_binder_type ty nal c =
 let extern_possible_prim_token (custom,scopes) r =
    if !print_raw_literal then raise No_match;
    let (n,key) = uninterp_prim_token r scopes in
-   match availability_of_entry_coercion custom (InConstrEntry,0) with
+   match availability_of_entry_coercion custom constr_lowest_level with
    | None -> raise No_match
    | Some coercion ->
       insert_entry_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
@@ -889,11 +891,11 @@ let rec extern inctx ?impargs scopes vars r =
 
   | c ->
 
-  match availability_of_entry_coercion (fst scopes) (InConstrEntry,0) with
+  match availability_of_entry_coercion (fst scopes) constr_lowest_level with
   | None -> raise No_match
   | Some coercion ->
 
-  let scopes = ((InConstrEntry,(LevelSome (*??*),None)), snd scopes) in
+  let scopes = (constr_some_level, snd scopes) in
   let c = match c with
 
   (* The remaining cases are only for the constr entry *)
@@ -1222,7 +1224,7 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules =
         (* Try availability of interpretation ... *)
         match keyrule with
           | NotationRule (_,ntn as specific_ntn) ->
-            let entry = (fst ntn, pi2 (Notation.level_of_notation ntn)) in
+            let entry = fst (Notation.level_of_notation ntn) in
              (match availability_of_entry_coercion custom entry with
              | None -> raise No_match
              | Some coercion ->
@@ -1275,7 +1277,7 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules =
               let args = extern_args (extern true) (vars,uvars) args in
               let c = CAst.make ?loc @@ extern_applied_abbreviation inctx nallargs argsimpls (a,cf) l args in
               if isCRef_no_univ c.CAst.v && entry_has_global custom then c
-             else match availability_of_entry_coercion custom (InConstrEntry,0) with
+             else match availability_of_entry_coercion custom constr_lowest_level with
              | None -> raise No_match
              | Some coercion -> insert_entry_coercion coercion c
       with
@@ -1294,10 +1296,10 @@ and extern_applied_proj inctx scopes vars (cst,us) params c extraargs =
   extern_projection inctx (f,us) nparams args imps
 
 let extern_glob_constr vars c =
-  extern false ((InConstrEntry,(LevelSome,None)),([],[])) vars c
+  extern false (constr_some_level,([],[])) vars c
 
 let extern_glob_type ?impargs vars c =
-  extern_typ ?impargs ((InConstrEntry,(LevelSome,None)),([],[])) vars c
+  extern_typ ?impargs (constr_some_level,([],[])) vars c
 
 (******************************************************************)
 (* Main translation function from constr -> constr_expr *)
@@ -1306,7 +1308,7 @@ let extern_constr ?(inctx=false) ?scope env sigma t =
   let r = Detyping.detype Detyping.Later Id.Set.empty env sigma t in
   let vars = extern_env env sigma in
   let scope = Option.cata (fun x -> [x]) [] scope in
-  extern inctx ((InConstrEntry,(LevelSome,None)),(scope,[])) vars r
+  extern inctx (constr_some_level,(scope,[])) vars r
 
 let extern_constr_in_scope ?inctx scope env sigma t =
   extern_constr ?inctx ~scope env sigma t
@@ -1332,7 +1334,7 @@ let extern_closed_glob ?(goal_concl_style=false) ?(inctx=false) ?scope env sigma
   in
   let vars = extern_env env sigma in
   let scope = Option.cata (fun x -> [x]) [] scope in
-  extern inctx ((InConstrEntry,(LevelSome,None)),(scope,[])) vars r
+  extern inctx (constr_some_level,(scope,[])) vars r
 
 (******************************************************************)
 (* Main translation function from pattern -> constr_expr *)
@@ -1474,7 +1476,7 @@ and glob_of_pat_under_context avoid env sigma (nas, pat) =
   (Array.rev_of_list nas, pat)
 
 let extern_constr_pattern env sigma pat =
-  extern true ((InConstrEntry,(LevelSome,None)),([],[]))
+  extern true (constr_some_level,([],[]))
     (* XXX no vars? *)
     (Id.Set.empty, Evd.universe_binders sigma)
     (glob_of_pat Id.Set.empty env sigma pat)
@@ -1483,4 +1485,4 @@ let extern_rel_context where env sigma sign =
   let a = detype_rel_context Detyping.Later where Id.Set.empty (names_of_rel_context env,env) sigma sign in
   let vars = extern_env env sigma in
   let a = List.map (extended_glob_local_binder_of_decl) a in
-  pi3 (extern_local_binder ((InConstrEntry,(LevelSome,None)),([],[])) vars a)
+  pi3 (extern_local_binder (constr_some_level,([],[])) vars a)
diff --git a/interp/notation.ml b/interp/notation.ml
index 1a1ca7f4821f..9712535c5ba4 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1543,13 +1543,17 @@ let sublevel_ord lev lev' =
   | LevelLt n, LevelLe n' -> n < n'
   | LevelLe n, LevelLt n' -> n <= n'-1
 
-let is_coercion (e1,n1) (e2,(n2,_)) =
+let is_coercion
+    { notation_entry = e1; notation_level = n1 }
+    { notation_subentry = e2; notation_relative_level = n2 } =
   not (notation_entry_eq e1 e2) ||
   match n2 with
   | LevelLt n2 | LevelLe n2 -> n1 < n2
   | LevelSome -> true (* unless n2 is the entry top level but we shall know it only dynamically *)
 
-let included (e1,n1) (e2,(n2,_)) =
+let included
+    { notation_entry = e1; notation_level = n1 }
+    { notation_subentry = e2; notation_relative_level = n2 } =
   notation_entry_eq e1 e2 && entry_relative_level_le n1 n2
 
 let rec search nfrom nto = function
@@ -1557,7 +1561,9 @@ let rec search nfrom nto = function
   | ((pfrom,pto),coe)::l ->
     if entry_relative_level_le pfrom nfrom && entry_relative_level_le nto pto then coe else search nfrom nto l
 
-let availability_of_entry_coercion (entry,(sublev,_) as entry_sublev) (entry',lev' as entry_lev) =
+let availability_of_entry_coercion
+    ({ notation_subentry = entry; notation_relative_level = sublev } as entry_sublev)
+    ({ notation_entry = entry'; notation_level = lev' } as entry_lev) =
   if included entry_lev entry_sublev then
     (* [entry] is by default included in [relative_entry] *)
     Some []
@@ -1578,21 +1584,23 @@ let rec insert_coercion_path path = function
       else path'::insert_coercion_path path paths
 
 let declare_entry_coercion ntn entry_level entry_relative_level' =
-  let entry, lev = entry_level in
-  let entry', (sublev',_) = entry_relative_level' in
+  let { notation_entry = entry; notation_level = lev } = entry_level in
+  let { notation_subentry = entry'; notation_relative_level = sublev' } = entry_relative_level' in
   (* Transitive closure *)
   let toaddleft =
     EntryCoercionMap.fold (fun (entry'',entry''') paths l ->
         List.fold_right (fun ((lev'',sublev'''),path) l ->
-        if included entry_level (entry''',(sublev''',None)) &&
-           not (included (entry'',lev'') entry_relative_level')
+            if included entry_level
+                { notation_subentry = entry'''; notation_relative_level = sublev'''; notation_position = None } &&
+               not (included { notation_entry = entry''; notation_level = lev'' } entry_relative_level')
         then ((entry'',entry'),((lev'',sublev'),path@[ntn]))::l else l) paths l)
       !entry_coercion_map [] in
   let toaddright =
     EntryCoercionMap.fold (fun (entry'',entry''') paths l ->
         List.fold_right (fun ((lev'',sublev'''),path) l ->
-        if included (entry'',lev'') entry_relative_level' &&
-           not (included entry_level (entry''',(sublev''',None)))
+        if included { notation_entry = entry''; notation_level = lev'' } entry_relative_level' &&
+           not (included entry_level
+                  { notation_subentry = entry'''; notation_relative_level = sublev'''; notation_position = None })
         then ((entry,entry'''),((lev,sublev'''),path@[ntn]))::l else l) paths l)
       !entry_coercion_map [] in
   entry_coercion_map :=
@@ -1615,9 +1623,10 @@ let declare_custom_entry_has_global s n =
   with Not_found ->
     entry_has_global_map := String.Map.add s n !entry_has_global_map
 
-let entry_has_global = function
-  | InConstrEntry, _ -> true
-  | InCustomEntry s, (n,_) ->
+let entry_has_global { notation_subentry = entry; notation_relative_level = n } =
+  match entry with
+  | InConstrEntry -> true
+  | InCustomEntry s ->
      try entry_relative_level_le (String.Map.find s !entry_has_global_map) n with Not_found -> false
 
 let entry_has_ident_map = ref String.Map.empty
@@ -1630,9 +1639,10 @@ let declare_custom_entry_has_ident s n =
   with Not_found ->
     entry_has_ident_map := String.Map.add s n !entry_has_ident_map
 
-let entry_has_ident = function
-  | InConstrEntry, _ -> true
-  | InCustomEntry s, (n,_) ->
+let entry_has_ident { notation_subentry = entry; notation_relative_level = n } =
+  match entry with
+  | InConstrEntry -> true
+  | InCustomEntry s ->
      try entry_relative_level_le (String.Map.find s !entry_has_ident_map) n with Not_found -> false
 
 type entry_coercion_kind =
@@ -2002,7 +2012,7 @@ let is_numeral_in_constr (entry,symbs) =
 let level_of_notation ntn =
   if is_numeral_in_constr (decompose_notation_key ntn) then
     (* A primitive notation *)
-    (fst ntn, 0, []) (* TODO: string notations*)
+    ({ notation_entry = fst ntn; notation_level = 0}, []) (* TODO: string notations*)
   else
     NotationMap.find ntn !notation_level_map
 
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 4a45dcddbd76..cf0d8bda59af 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -21,6 +21,14 @@ open Glob_ops
 open Mod_subst
 open Notation_term
 
+(** Constr default entry *)
+
+let constr_lowest_level =
+  Constrexpr.{notation_entry = InConstrEntry; notation_level = 0}
+
+let constr_some_level =
+  Constrexpr.{notation_subentry = InConstrEntry; notation_relative_level = LevelSome; notation_position = None}
+
 (**********************************************************************)
 (* Utilities                                                          *)
 
@@ -1309,11 +1317,9 @@ let remove_sigma x (terms,termlists,binders,binderlists) =
 let remove_bindinglist_sigma x (terms,termlists,binders,binderlists) =
   (terms,termlists,binders,Id.List.remove_assoc x binderlists)
 
-let default_constr_entry_relative_level = Constrexpr.(InConstrEntry,(LevelSome,None))
-
-let add_ldots_var metas = (ldots_var,((default_constr_entry_relative_level,([],[])),NtnTypeConstr))::metas
+let add_ldots_var metas = (ldots_var,((constr_some_level,([],[])),NtnTypeConstr))::metas
 
-let add_meta_bindinglist x metas = (x,((default_constr_entry_relative_level,([],[])),NtnTypeBinderList (*arbitrary:*) NtnBinderParsedAsBinder))::metas
+let add_meta_bindinglist x metas = (x,((constr_some_level,([],[])),NtnTypeBinderList (*arbitrary:*) NtnBinderParsedAsBinder))::metas
 
 (* This tells if letins in the middle of binders should be included in
    the sequence of binders *)
@@ -1359,7 +1365,7 @@ let match_binderlist match_iter_fun match_termin_fun alp metas sigma rest x y it
   let alp,sigma = bind_bindinglist_env alp sigma x bl in
   match_termin_fun alp metas sigma rest termin
 
-let add_meta_term x metas = (x,((default_constr_entry_relative_level,([],[])),NtnTypeConstr))::metas (* Should reuse the scope of the partner of x! *)
+let add_meta_term x metas = (x,((constr_some_level,([],[])),NtnTypeConstr))::metas (* Should reuse the scope of the partner of x! *)
 
 let match_termlist match_fun alp metas sigma rest x y iter termin revert =
   let rec aux alp sigma acc rest =
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 621eaec0dde9..e6bb0f041eae 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -12,6 +12,14 @@ open Names
 open Notation_term
 open Glob_term
 
+(** Constr default entries *)
+
+(* Equivalent to an entry "in constr at level 0"; used for coercion to constr *)
+val constr_lowest_level : Constrexpr.notation_entry_level
+
+(* Equivalent to "x constr" in a subentry, at highest level *)
+val constr_some_level : Constrexpr.notation_entry_relative_level
+
 (** {5 Utilities about [notation_constr]} *)
 
 val eq_notation_constr : Id.t list * Id.t list -> notation_constr -> notation_constr -> bool
diff --git a/interp/notationextern.ml b/interp/notationextern.ml
index e66faa71bde1..35227e098458 100644
--- a/interp/notationextern.ml
+++ b/interp/notationextern.ml
@@ -36,10 +36,14 @@ let notation_entry_eq s1 s2 = match (s1,s2) with
   | InCustomEntry s1, InCustomEntry s2 -> String.equal s1 s2
   | (InConstrEntry | InCustomEntry _), _ -> false
 
-let notation_entry_level_eq (e1,n1) (e2,n2) =
+let notation_entry_level_eq
+    { notation_entry = e1; notation_level = n1 }
+    { notation_entry = e2; notation_level = n2 } =
   notation_entry_eq e1 e2 && Int.equal n1 n2
 
-let notation_entry_relative_level_eq (e1,(n1,s1)) (e2,(n2,s2)) =
+let notation_entry_relative_level_eq
+    { notation_subentry = e1; notation_relative_level = n1; notation_position = s1 }
+    { notation_subentry = e2; notation_relative_level = n2; notation_position = s2 } =
   notation_entry_eq e1 e2 && entry_relative_level_eq n1 n2 && s1 = s2
 
 let notation_eq (from1,ntn1) (from2,ntn2) =
@@ -77,13 +81,12 @@ let interpretation_eq (vars1, t1 as x1) (vars2, t2 as x2) =
   List.equal var_attributes_eq vars1 vars2 &&
   Notation_ops.eq_notation_constr (List.map fst vars1, List.map fst vars2) t1 t2
 
-type level = notation_entry * entry_level * entry_relative_level list
-  (* first argument is InCustomEntry s for custom entries *)
+type level = notation_entry_level * entry_relative_level list
 
-let level_eq (s1, l1, t1) (s2, l2, t2) =
+let level_eq ({ notation_entry = s1; notation_level = l1}, t1) ({ notation_entry = s2; notation_level = l2}, t2) =
   notation_entry_eq s1 s2 && Int.equal l1 l2 && List.equal entry_relative_level_eq t1 t2
 
-(* Uninterpretation tables *)
+(** Uninterpretation tables *)
 
 type 'a interp_rule_gen =
   | NotationRule of Constrexpr.specific_notation
diff --git a/interp/notationextern.mli b/interp/notationextern.mli
index f17e9d658bf8..0311f5523077 100644
--- a/interp/notationextern.mli
+++ b/interp/notationextern.mli
@@ -30,8 +30,8 @@ val interpretation_eq : interpretation -> interpretation -> bool
 val notation_entry_level_eq : notation_entry_level -> notation_entry_level -> bool
 (** Equality on [notation_entry_level]. *)
 
-type level = notation_entry * entry_level * entry_relative_level list
-  (* first argument is InCustomEntry s for custom entries *)
+type level = notation_entry_level * entry_relative_level list
+(** The "signature" of a rule: its level together with the levels of its subentries *)
 
 val level_eq : level -> level -> bool
 (** Equality on [level]. *)
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index e1a65fb992a7..d61da35794b7 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -206,14 +206,15 @@ let assoc_eq al ar =
   | LeftA, LeftA -> true
   | _, _ -> false
 
-(** [adjust_level assoc from prod] where [assoc] and [from] are the name
+(** [adjust_level assoc fromlev prod] where [assoc] and [fromlev] are the name
    and associativity of the level where to add the rule; the meaning of
    the result is
 
      DefaultLevel = entry name
      NextLevel = NEXT
      NumLevel n = constr LEVEL n *)
-let adjust_level custom assoc (custom',from) p = let open Gramlib.Gramext in match p with
+let adjust_level custom assoc {notation_entry = custom'; notation_level = fromlev} p =
+  let open Gramlib.Gramext in match p with
 (* If a level in a different grammar, no other choice than denoting it by absolute level *)
   | (NumLevel n,_) when not (notation_entry_eq custom custom') -> NumLevel n
 (* If a default level in a different grammar, the entry name is ok *)
@@ -229,7 +230,7 @@ let adjust_level custom assoc (custom',from) p = let open Gramlib.Gramext in mat
   | ((NumLevel _ | DefaultLevel),BorderProd (Right,Some (NonA|LeftA))) -> NextLevel
   (* If RightA on the right-hand side, set to the explicit (current) level *)
   | (NumLevel n,BorderProd (Right,Some RightA)) -> NumLevel n
-  | (DefaultLevel,BorderProd (Right,Some RightA)) -> NumLevel from
+  | (DefaultLevel,BorderProd (Right,Some RightA)) -> NumLevel fromlev
 (* Compute production name on the left side *)
   (* If NonA on the left-hand side, adopt the current assoc ?? *)
   | ((NumLevel _ | DefaultLevel),BorderProd (Left,Some NonA)) -> DefaultLevel
@@ -243,7 +244,7 @@ let adjust_level custom assoc (custom',from) p = let open Gramlib.Gramext in mat
   | (NextLevel,_) -> assert (notation_entry_eq custom custom'); NextLevel
 (* Compute production name elsewhere *)
   | (NumLevel n,InternalProd) ->
-    if from = n + 1 then NextLevel else NumLevel n
+    if fromlev = n + 1 then NextLevel else NumLevel n
 
 type _ target =
 | ForConstr : constr_expr target
@@ -296,9 +297,9 @@ let exists_custom_entry s = match find_custom_entry s with
 
 let locality_of_custom_entry s = String.Set.mem s !custom_entry_locality
 
-(* This computes the name of the level where to add a new rule *)
-let interp_constr_entry_key : type r. _ -> r target -> int -> r Entry.t * int option =
-  fun custom forpat level ->
+(** This computes the name of the level where to add a new rule *)
+let interp_constr_entry_key : type r. _ -> r target -> r Entry.t * int option =
+  fun {notation_entry = custom; notation_level = level} forpat ->
   match custom with
   | InCustomEntry s ->
      (let (entry_for_constr, entry_for_patttern) = find_custom_entry s in
@@ -323,15 +324,17 @@ let target_entry : type s. notation_entry -> s target -> s Entry.t = function
    | ForConstr -> entry_for_constr
    | ForPattern -> entry_for_patttern
 
-let is_self custom (custom',from) e = notation_entry_eq custom custom' && match e with
-| (NumLevel n, BorderProd (Right, _ (* Some(NonA|LeftA) *))) -> false
-| (NumLevel n, BorderProd (Left, _)) -> Int.equal from n
-| _ -> false
+let is_self custom {notation_entry = custom'; notation_level = fromlev} e =
+  notation_entry_eq custom custom' && match e with
+  | (NumLevel n, BorderProd (Right, _ (* Some(NonA|LeftA) *))) -> false
+  | (NumLevel n, BorderProd (Left, _)) -> Int.equal fromlev n
+  | _ -> false
 
-let is_binder_level custom (custom',from) e = match e with
-| (NumLevel 200, (BorderProd (Right, _) | InternalProd)) ->
-  custom = InConstrEntry && custom' = InConstrEntry && from = 200
-| _ -> false
+let is_binder_level custom {notation_entry = custom'; notation_level = fromlev} e =
+  match e with
+  | (NumLevel 200, (BorderProd (Right, _) | InternalProd)) ->
+    custom = InConstrEntry && custom' = InConstrEntry && fromlev = 200
+  | _ -> false
 
 let make_pattern (keyword,s) =
    if keyword then TPattern (Tok.PKEYWORD s) else
@@ -570,7 +573,7 @@ let rec pure_sublevels' assoc from forpat level = function
        (match Pcoq.level_of_nonterm sym with
         | None -> rem
         | Some i ->
-          if different_levels (fst from,level) (where,i) then
+          if different_levels (from.notation_entry,level) (where,i) then
             (where,int_of_string i) :: rem
           else rem)
      | _ -> rem in
@@ -589,12 +592,12 @@ 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 {notation_entry = custom; notation_level = _} as fromlev,_ = ng.notgram_level in
   let assoc = ng.notgram_assoc in
-  let (entry, level) = interp_constr_entry_key custom forpat n in
+  let (entry, level) = interp_constr_entry_key fromlev forpat in
   let fold (accu, state) pt =
-    let AnyTyRule r = make_ty_rule assoc (custom,n) forpat pt in
-    let pure_sublevels = pure_sublevels' assoc (custom,n) forpat level pt in
+    let AnyTyRule r = make_ty_rule assoc fromlev forpat pt in
+    let pure_sublevels = pure_sublevels' assoc fromlev forpat level pt in
     let isforpat = target_to_bool forpat in
     let needed_levels, state = register_empty_levels state isforpat pure_sublevels in
     let (pos,p4assoc,name,reinit), state = find_position state custom isforpat assoc level in
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 38a144139c0f..836f83488479 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -320,7 +320,7 @@ let precedence_of_position_and_level from_level = function
   | DefaultLevel, _ -> LevelSome, None
 
 (** Computing precedences of non-terminals for parsing *)
-let precedence_of_entry_type (from_custom,from_level) = function
+let precedence_of_entry_type { notation_entry = from_custom; notation_level = from_level } = function
   | ETConstr (custom,_,x) when notation_entry_eq custom from_custom ->
     fst (precedence_of_position_and_level from_level x)
   | ETConstr (custom,_,(NumLevel n,_)) -> LevelLe n
@@ -644,7 +644,7 @@ let hunks_of_format (from_level,(vars,typs)) symfmt =
 (**********************************************************************)
 (* Build parsing rules                                                *)
 
-let assoc_of_type from n (_,typ) = precedence_of_entry_type (from,n) typ
+let assoc_of_type from n (_,typ) = precedence_of_entry_type {notation_entry = from; notation_level = n} typ
 
 let is_not_small_constr = function
     ETProdConstr _ -> true
@@ -721,7 +721,7 @@ let keyword_needed need s =
     need
   | _ -> true
 
-let make_production (_,lev,_) etyps symbols =
+let make_production ({notation_level = lev}, _) etyps symbols =
   let rec aux need = function
     | [] -> [[]]
     | NonTerminal m :: l ->
@@ -793,7 +793,7 @@ 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 ({notation_entry = from; notation_level = 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)
@@ -1189,12 +1189,12 @@ let make_interpretation_type isrec isbinding default_if_binding typ =
 let entry_relative_level_of_constr_prod_entry from_level = function
   | ETConstr (entry,_,(_,y)) as x ->
      let side = match y with BorderProd (side,_) -> Some side | _ -> None in
-     (entry,(precedence_of_entry_type from_level x,side))
-  | _ -> InConstrEntry,(LevelSome,None) (*??*)
+     { notation_subentry = entry; notation_relative_level = precedence_of_entry_type from_level x; notation_position = side }
+  | _ -> constr_some_level
 
 let make_interpretation_vars
   (* For binders, default is to parse only as an ident *) ?(default_if_binding=AsName)
-   recvars allvars (from,level,_) typs =
+   recvars allvars (entry,_) typs =
   let eq_subscope (sc1, l1) (sc2, l2) =
     List.equal String.equal sc1 sc2 &&
     List.equal String.equal l1 l2
@@ -1210,7 +1210,7 @@ let make_interpretation_vars
     Id.Map.filter (fun x _ -> not (Id.List.mem x useless_recvars)) allvars in
   Id.Map.mapi (fun x (isonlybinding, sc) ->
     let typ = Id.List.assoc x typs in
-    ((entry_relative_level_of_constr_prod_entry (from,level) typ,sc),
+    ((entry_relative_level_of_constr_prod_entry entry typ,sc),
      make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding default_if_binding typ)) mainvars
 
 let check_rule_productivity l =
@@ -1239,10 +1239,9 @@ let warn_non_reversible_notation =
 
 let is_coercion level typs =
   match level, typs with
-  | Some (custom,n,_), [_,e] ->
+  | Some ({notation_entry = custom; notation_level = n} as entry,_), [_,e] ->
      (match e, custom with
      | ETConstr _, _ ->
-         let entry = (custom,n) in
          let entry_relative = entry_relative_level_of_constr_prod_entry entry e in
          if is_coercion entry entry_relative then
            Some (IsEntryCoercion (entry,entry_relative))
@@ -1435,7 +1434,7 @@ let compute_syntax_data ~local main_data notation_symbols ntn mods =
   let pp_sy_data = (sy_typs,symbols) in
   let sy_fulldata = {
       ntn_for_grammar;
-      prec_for_grammar = (main_data.entry,n,prec_for_grammar);
+      prec_for_grammar = ({notation_entry = main_data.entry; notation_level = n}, prec_for_grammar);
       typs_for_grammar = List.map snd sy_typs_for_grammar;
       need_squash
     } in
@@ -1443,7 +1442,7 @@ let compute_syntax_data ~local main_data notation_symbols ntn mods =
   (* Return relevant data for interpretation and for parsing/printing *)
   {
     msgs;
-    level  = (main_data.entry,n,prec);
+    level = ({notation_entry = main_data.entry; notation_level = n}, prec);
     subentries = sy_typs;
     pa_syntax_data = pa_sy_data;
     pp_syntax_data = pp_sy_data;
@@ -1624,7 +1623,7 @@ let make_parsing_rules main_data (sd : SynData.syn_data) =
 
 let make_generic_printing_rules reserved main_data ntn sd =
   let open SynData in
-  let custom,level,_ = sd.level in
+  let {notation_entry = custom; notation_level = level},_ = sd.level in
   let make_rule rule =
     {
       notation_printing_reserved = reserved;
@@ -1666,7 +1665,7 @@ let make_syntax_rules reserved main_data ntn sd =
 let make_specific_printing_rules etyps symbols level pp_rule format =
   match level with
   | None -> None
-  | Some (_,level,_) ->
+  | Some ({ notation_level = level},_) ->
   match format, pp_rule with
     | None, Some _ when not (has_implicit_format symbols) -> None
     | _ ->
@@ -1717,7 +1716,7 @@ let make_notation_interpretation ~local main_data notation_symbols ntn syntax_ru
     ninterp_rec_vars = Id.Map.of_list recvars;
   } in
   let (acvars, ac, reversibility) = interp_notation_constr env ~impls nenv c in
-  let plevel = match level with Some (from,level,l) -> (from,level,l) | None (* numeral: irrelevant )*) -> (InConstrEntry,0,[]) in
+  let plevel = match level with Some (entry,l) -> (entry,l) | None (* numeral: irrelevant )*) -> (constr_lowest_level,[]) in
   let interp = make_interpretation_vars recvars acvars plevel i_typs in
   let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
   let vars = List.map_filter map i_vars in (* Order of elements is important here! *)
@@ -1922,7 +1921,7 @@ let add_abbreviation ~local deprecation env ident (vars,c) modl =
   in
   let level_arg = NumLevel 9 (* level of arguments of an application *) in
   let in_pat (id,_) = (id,ETConstr (Constrexpr.InConstrEntry,None,(level_arg,InternalProd))) in
-  let level = (InConstrEntry,0,[]) in
+  let level = (* not relevant *) (constr_lowest_level,[]) in
   let interp = make_interpretation_vars ~default_if_binding:AsAnyPattern [] acvars level (List.map in_pat vars) in
   let vars = List.map (fun (x,_) -> (x, Id.Map.find x interp)) vars in
   let also_in_cases_pattern = has_no_binders_type vars in