Merge PR #8115: Support for custom entries in notations (take 2, feature part)

1 files changed, 4 insertions, 7 deletions

diff --git a/parsing/extend.ml b/parsing/extend.ml
index f57e32c884..6fe2956643 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -34,14 +34,12 @@ type production_level =
 (** User-level types used to tell how to parse or interpret of the non-terminal *)
 
 type 'a constr_entry_key_gen =
-  | ETName
-  | ETReference
+  | ETIdent
+  | ETGlobal
   | ETBigint
   | ETBinder of bool  (* open list of binders if true, closed list of binders otherwise *)
-  | ETConstr of 'a
-  | ETConstrAsBinder of Notation_term.constr_as_binder_kind * 'a
+  | ETConstr of Constrexpr.notation_entry * Notation_term.constr_as_binder_kind option * 'a
   | ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *)
-  | ETOther of string * string
 
 (** Entries level (left-hand side of grammar rules) *)
 
@@ -63,9 +61,8 @@ type constr_prod_entry_key =
   | ETProdName            (* Parsed as a name (ident or _) *)
   | ETProdReference       (* Parsed as a global reference *)
   | ETProdBigint          (* Parsed as an (unbounded) integer *)
-  | ETProdConstr of (production_level * production_position) (* Parsed as constr or pattern *)
+  | ETProdConstr of Constrexpr.notation_entry * (production_level * production_position) (* Parsed as constr or pattern, or a subentry of those *)
   | ETProdPattern of int  (* Parsed as pattern as a binder (as subpart of a constr) *)
-  | ETProdOther of string * string (* Intended for embedding custom entries in constr or pattern *)
   | ETProdConstrList of (production_level * production_position) * Tok.t list (* Parsed as non-empty list of constr *)
   | ETProdBinderList of binder_entry_kind  (* Parsed as non-empty list of local binders *)