Module Extend

Entry keys for constr notations

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

Interpreted differently at the border or inside a rule

*)
val production_level_eq : production_level -> production_level -> bool

User-level types used to tell how to parse or interpret of the non-terminal

type 'a constr_entry_key_gen =
| ETIdent
| ETName
| ETGlobal
| ETBigint
| ETBinder of bool
| ETConstr of Constrexpr.notation_entry * Notation_term.notation_binder_kind option * 'a
| ETPattern of bool * int option

Entries level (left-hand side of grammar rules)

type constr_entry_key = (production_level * production_position) constr_entry_key_gen
val constr_entry_key_eq : constr_entry_key -> constr_entry_key -> bool
val constr_entry_key_eq_ignore_binder_kind : constr_entry_key -> constr_entry_key -> bool

Entries used in productions, vernac side (e.g. "x bigint" or "x ident")

type simple_constr_prod_entry_key = production_level constr_entry_key_gen

Entries used in productions (in right-hand-side of grammar rules), to parse non-terminals

type binder_target =
| ForBinder
| ForTerm
type binder_entry_kind =
| ETBinderOpen
| ETBinderClosed of constr_prod_entry_key option * (bool * string) list
and constr_prod_entry_key =
| ETProdIdent
| ETProdName
| ETProdGlobal
| ETProdBigint
| ETProdOneBinder of bool
| ETProdConstr of Constrexpr.notation_entry * production_level * production_position
| ETProdPattern of int
| ETProdConstrList of Constrexpr.notation_entry * production_level * production_position * (bool * string) 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