Module Extend

Entry keys for constr notations

type side =
| Left
| Right
type production_position =
| BorderProd of side * Gramlib.Gramext.g_assoc option
| InternalProd
type production_level =
| NextLevel
| NumLevel of int
| DefaultLevel

Interpreted differently at the border or inside a rule

type 'a constr_entry_key_gen =
| ETIdent
| ETGlobal
| ETBigint
| ETBinder of bool
| ETConstr of Constrexpr.notation_entry * Notation_term.constr_as_binder_kind option * 'a
| ETPattern of bool * int option
type constr_entry_key = (production_level * production_position) constr_entry_key_gen
type simple_constr_prod_entry_key = production_level constr_entry_key_gen
type binder_entry_kind =
| ETBinderOpen
| ETBinderClosed of string Tok.p list
type binder_target =
| ForBinder
| ForTerm
type constr_prod_entry_key =
| ETProdName
| ETProdReference
| ETProdBigint
| ETProdConstr of Constrexpr.notation_entry * production_level * production_position
| ETProdPattern of int
| ETProdConstrList of Constrexpr.notation_entry * production_level * production_position * string Tok.p list
| ETProdBinderList of binder_entry_kind
AST for user-provided entries
type 'a user_symbol =
| Ulist1 of 'a user_symbol
| Ulist1sep of 'a user_symbol * string
| Ulist0 of 'a user_symbol
| Ulist0sep of 'a user_symbol * string
| Uopt of 'a user_symbol
| Uentry of 'a
| Uentryl of 'a * int
type ('a, 'b, 'c) ty_user_symbol =
| TUlist1 : ('a, 'b, 'c) ty_user_symbol -> ('a list, 'b list, 'c list) ty_user_symbol
| TUlist1sep : ('a, 'b, 'c) ty_user_symbol * string -> ('a list, 'b list, 'c list) ty_user_symbol
| TUlist0 : ('a, 'b, 'c) ty_user_symbol -> ('a list, 'b list, 'c list) ty_user_symbol
| TUlist0sep : ('a, 'b, 'c) ty_user_symbol * string -> ('a list, 'b list, 'c list) ty_user_symbol
| TUopt : ('a, 'b, 'c) ty_user_symbol -> ('a option, 'b option, 'c option) ty_user_symbol
| TUentry : ('a, 'b, 'c) Genarg.ArgT.tag -> ('a, 'b, 'c) ty_user_symbol
| TUentryl : ('a, 'b, 'c) Genarg.ArgT.tag * int -> ('a, 'b, 'c) ty_user_symbol