package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type universe_decl_expr = (Names.lident list, Glob_term.glob_constraint list) UState.gen_universe_decl
type ident_decl = Names.lident * universe_decl_expr option
type name_decl = Names.lname * universe_decl_expr option
type notation_entry =
  1. | InConstrEntry
  2. | InCustomEntry of string
type notation_entry_level =
  1. | InConstrEntrySomeLevel
  2. | InCustomEntryLevel of string * int
type notation_key = string
type !'a or_by_notation_r =
  1. | AN of 'a
  2. | ByNotation of string * string option
type !'a or_by_notation = 'a or_by_notation_r CAst.t
type explicitation =
  1. | ExplByPos of int * Names.Id.t option
  2. | ExplByName of Names.Id.t
type binder_kind =
  1. | Default of Decl_kinds.binding_kind
  2. | Generalized of Decl_kinds.binding_kind * bool
type abstraction_kind =
  1. | AbsLambda
  2. | AbsPi
type proj_flag = int option
type sign =
  1. | SPlus
  2. | SMinus
type raw_numeral = NumTok.t
type prim_token =
  1. | Numeral of sign * raw_numeral
  2. | String of string
type instance_expr = Glob_term.glob_level list
type cases_pattern_expr_r =
  1. | CPatAlias of cases_pattern_expr * Names.lname
  2. | CPatCstr of Libnames.qualid * cases_pattern_expr list option * cases_pattern_expr list
  3. | CPatAtom of Libnames.qualid option
  4. | CPatOr of cases_pattern_expr list
  5. | CPatNotation of notation * cases_pattern_notation_substitution * cases_pattern_expr list
  6. | CPatPrim of prim_token
  7. | CPatRecord of (Libnames.qualid * cases_pattern_expr) list
  8. | CPatDelimiters of string * cases_pattern_expr
  9. | 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 =
  1. | CRef of Libnames.qualid * instance_expr option
  2. | CFix of Names.lident * fix_expr list
  3. | CCoFix of Names.lident * cofix_expr list
  4. | CProdN of local_binder_expr list * constr_expr
  5. | CLambdaN of local_binder_expr list * constr_expr
  6. | CLetIn of Names.lname * constr_expr * constr_expr option * constr_expr
  7. | CAppExpl of proj_flag * Libnames.qualid * instance_expr option * constr_expr list
  8. | CApp of proj_flag * constr_expr * (constr_expr * explicitation CAst.t option) list
  9. | CRecord of (Libnames.qualid * constr_expr) list
  10. | CCases of Constr.case_style * constr_expr option * case_expr list * branch_expr list
  11. | CLetTuple of Names.lname list * Names.lname option * constr_expr option * constr_expr * constr_expr
  12. | CIf of constr_expr * Names.lname option * constr_expr option * constr_expr * constr_expr
  13. | CHole of Evar_kinds.t option * Namegen.intro_pattern_naming_expr * Genarg.raw_generic_argument option
  14. | CPatVar of Pattern.patvar
  15. | CEvar of Glob_term.existential_name * (Names.Id.t * constr_expr) list
  16. | CSort of Glob_term.glob_sort
  17. | CCast of constr_expr * constr_expr Glob_term.cast_type
  18. | CNotation of notation * constr_notation_substitution
  19. | CGeneralization of Decl_kinds.binding_kind * abstraction_kind option * constr_expr
  20. | CPrim of prim_token
  21. | 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 recursion_order_expr_r =
  1. | CStructRec of Names.lident
  2. | CWfRec of Names.lident * constr_expr
  3. | CMeasureRec of Names.lident option * constr_expr * constr_expr option
and recursion_order_expr = recursion_order_expr_r CAst.t
and local_binder_expr =
  1. | CLocalAssum of Names.lname list * binder_kind * constr_expr
  2. | CLocalDef of Names.lname * constr_expr * constr_expr option
  3. | 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 =
  1. | CWith_Module of Names.Id.t list CAst.t * Libnames.qualid
  2. | CWith_Definition of Names.Id.t list CAst.t * universe_decl_expr option * constr_expr
type module_ast_r =
  1. | CMident of Libnames.qualid
  2. | CMapply of module_ast * module_ast
  3. | CMwith of module_ast * with_declaration_ast
and module_ast = module_ast_r CAst.t
OCaml

Innovation. Community. Security.