package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type sort_name_expr =
  1. | CSProp
  2. | CProp
  3. | CSet
  4. | CType of Libnames.qualid
  5. | CRawType of Univ.Level.t
type sort_expr = (sort_name_expr * int) list Glob_term.glob_sort_gen
type instance_expr = univ_level_expr list
type univ_constraint_expr = sort_name_expr * Univ.constraint_type * sort_name_expr
type universe_decl_expr = (Names.lident list, univ_constraint_expr list) UState.gen_universe_decl
type cumul_univ_decl_expr = ((Names.lident * Univ.Variance.t option) list, univ_constraint_expr list) UState.gen_universe_decl
type ident_decl = Names.lident * universe_decl_expr option
type cumul_ident_decl = Names.lident * cumul_univ_decl_expr option
type name_decl = Names.lname * universe_decl_expr option
type notation_with_optional_scope =
  1. | LastLonelyNotation
  2. | NotationInScope of string
type entry_level = int
type entry_relative_level =
  1. | LevelLt of entry_level
  2. | LevelLe of entry_level
  3. | LevelSome
type notation_entry =
  1. | InConstrEntry
  2. | InCustomEntry of string
type notation_entry_level =
  1. | InConstrEntrySomeLevel
  2. | InCustomEntryLevel of string * entry_level
type notation_key = string
type notation = notation_entry * notation_key
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 Glob_term.binding_kind
  2. | Generalized of Glob_term.binding_kind * bool
type abstraction_kind =
  1. | AbsLambda
  2. | AbsPi
type proj_flag = int option
type prim_token =
  1. | Number of NumTok.Signed.t
  2. | String of string
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_with_optional_scope option * 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 kinded_cases_pattern_expr = cases_pattern_expr * Glob_term.binding_kind
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 CAst.t * (Names.lident * constr_expr) list
  16. | CSort of sort_expr
  17. | CCast of constr_expr * constr_expr Glob_term.cast_type
  18. | CNotation of notation_with_optional_scope option * notation * constr_notation_substitution
  19. | CGeneralization of Glob_term.binding_kind * abstraction_kind option * constr_expr
  20. | CPrim of prim_token
  21. | CDelimiters of string * constr_expr
  22. | CArray of instance_expr option * constr_expr array * constr_expr * 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
and constr_notation_substitution = constr_expr list * constr_expr list list * kinded_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