Module Constrexpr

Concrete syntax for terms
type universe_decl_expr = (Names.lident list, Glob_term.glob_constraint list) UState.gen_universe_decl

constr_expr is the abstract syntax tree produced by the parser

type ident_decl = Names.lident * universe_decl_expr option
type name_decl = Names.lname * universe_decl_expr option
type notation_with_optional_scope =
| LastLonelyNotation
| NotationInScope of string
type entry_level = int
type entry_relative_level =
| LevelLt of entry_level
| LevelLe of entry_level
| LevelSome
type notation_entry =
| InConstrEntry
| InCustomEntry of string
type notation_entry_level =
| InConstrEntrySomeLevel
| InCustomEntryLevel of string * entry_level
type notation_key = string
type notation = notation_entry * notation_key
type specific_notation = notation_with_optional_scope * (notation_entry * notation_key)
type 'a or_by_notation_r =
| AN of 'a
| ByNotation of string * string option
type 'a or_by_notation = 'a or_by_notation_r CAst.t
type explicitation =
| ExplByPos of int * Names.Id.t option
| ExplByName of Names.Id.t
type binder_kind =
| Default of Glob_term.binding_kind
| Generalized of Glob_term.binding_kind * bool

(Inner binding always Implicit) Outer bindings, typeclass-specific flag for implicit generalization of superclasses

type abstraction_kind =
| AbsLambda
| AbsPi
type proj_flag = int option

Some n = proj of the n-th visible argument

type prim_token =
| Numeral of NumTok.Signed.t
| String of string
type instance_expr = Glob_term.glob_level list
type cases_pattern_expr_r =
| CPatAlias of cases_pattern_expr * Names.lname
| CPatCstr of Libnames.qualid * cases_pattern_expr list option * cases_pattern_expr list

CPatCstr (_, c, Some l1, l2) represents (@ c l1) l2

| CPatAtom of Libnames.qualid option
| CPatOr of cases_pattern_expr list
| CPatNotation of notation_with_optional_scope option * notation * cases_pattern_notation_substitution * cases_pattern_expr list

CPatNotation (_, n, l1 ,l2) represents (notation n applied with substitution l1) applied to arguments l2

| CPatPrim of prim_token
| CPatRecord of (Libnames.qualid * cases_pattern_expr) list
| CPatDelimiters of string * cases_pattern_expr
| CPatCast of cases_pattern_expr * constr_expr
and cases_pattern_expr = cases_pattern_expr_r CAst.t
and cases_pattern_notation_substitution = cases_pattern_expr list * cases_pattern_expr list list
and constr_expr_r =
| CRef of Libnames.qualid * instance_expr option
| CFix of Names.lident * fix_expr list
| CCoFix of Names.lident * cofix_expr list
| CProdN of local_binder_expr list * constr_expr
| CLambdaN of local_binder_expr list * constr_expr
| CLetIn of Names.lname * constr_expr * constr_expr option * constr_expr
| CAppExpl of proj_flag * Libnames.qualid * instance_expr option * constr_expr list
| CApp of proj_flag * constr_expr * (constr_expr * explicitation CAst.t option) list
| CRecord of (Libnames.qualid * constr_expr) list
| CCases of Constr.case_style * constr_expr option * case_expr list * branch_expr list
| CLetTuple of Names.lname list * Names.lname option * constr_expr option * constr_expr * constr_expr
| CIf of constr_expr * Names.lname option * constr_expr option * constr_expr * constr_expr
| CHole of Evar_kinds.t option * Namegen.intro_pattern_naming_expr * Genarg.raw_generic_argument option
| CPatVar of Pattern.patvar
| CEvar of Glob_term.existential_name * (Names.Id.t * constr_expr) list
| CSort of Glob_term.glob_sort
| CCast of constr_expr * constr_expr Glob_term.cast_type
| CNotation of notation_with_optional_scope option * notation * constr_notation_substitution
| CGeneralization of Glob_term.binding_kind * abstraction_kind option * constr_expr
| CPrim of prim_token
| CDelimiters of string * constr_expr
and constr_expr = constr_expr_r CAst.t
and case_expr = constr_expr * Names.lname option * cases_pattern_expr option
and branch_expr = (cases_pattern_expr list list * constr_expr) CAst.t
and fix_expr = Names.lident * recursion_order_expr option * local_binder_expr list * constr_expr * constr_expr
and cofix_expr = Names.lident * local_binder_expr list * constr_expr * constr_expr
and recursion_order_expr_r =
| CStructRec of Names.lident
| CWfRec of Names.lident * constr_expr
| CMeasureRec of Names.lident option * constr_expr * constr_expr option

argument, measure, relation

and recursion_order_expr = recursion_order_expr_r CAst.t
and local_binder_expr =
| CLocalAssum of Names.lname list * binder_kind * constr_expr
| CLocalDef of Names.lname * constr_expr * constr_expr option
| CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t
and constr_notation_substitution = constr_expr list * constr_expr list list * cases_pattern_expr list * local_binder_expr list list
type constr_pattern_expr = constr_expr
type with_declaration_ast =
| CWith_Module of Names.Id.t list CAst.t * Libnames.qualid
| CWith_Definition of Names.Id.t list CAst.t * universe_decl_expr option * constr_expr
type module_ast_r =
| CMident of Libnames.qualid
| CMapply of module_ast * module_ast
| CMwith of module_ast * with_declaration_ast
and module_ast = module_ast_r CAst.t