package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type universes_entry =
  1. | Monomorphic_entry of Univ.ContextSet.t
  2. | Polymorphic_entry of Names.Name.t array * Univ.UContext.t
type !'a in_universes_entry = 'a * universes_entry
type one_inductive_entry = {
  1. mind_entry_typename : Names.Id.t;
  2. mind_entry_arity : Constr.constr;
  3. mind_entry_template : bool;
  4. mind_entry_consnames : Names.Id.t list;
  5. mind_entry_lc : Constr.constr list;
}
type mutual_inductive_entry = {
  1. mind_entry_record : Names.Id.t array option option;
  2. mind_entry_finite : Declarations.recursivity_kind;
  3. mind_entry_params : Constr.rel_context;
  4. mind_entry_inds : one_inductive_entry list;
  5. mind_entry_universes : universes_entry;
  6. mind_entry_variance : Univ.Variance.t array option;
  7. mind_entry_private : bool option;
}
type definition_entry = {
  1. const_entry_body : Constr.constr;
  2. const_entry_secctx : Names.Id.Set.t option;
  3. const_entry_feedback : Stateid.t option;
  4. const_entry_type : Constr.types option;
  5. const_entry_universes : universes_entry;
  6. const_entry_inline_code : bool;
}
type section_def_entry = {
  1. secdef_body : Constr.constr;
  2. secdef_secctx : Names.Id.Set.t option;
  3. secdef_feedback : Stateid.t option;
  4. secdef_type : Constr.types option;
}
type !'a opaque_entry = {
  1. opaque_entry_body : 'a;
  2. opaque_entry_secctx : Names.Id.Set.t;
  3. opaque_entry_feedback : Stateid.t option;
  4. opaque_entry_type : Constr.types;
  5. opaque_entry_universes : universes_entry;
}
type inline = int option
type parameter_entry = Names.Id.Set.t option * Constr.types in_universes_entry * inline
type primitive_entry = {
  1. prim_entry_type : Constr.types option;
  2. prim_entry_univs : Univ.ContextSet.t;
  3. prim_entry_content : CPrimitives.op_or_type;
}
type !'a proof_output = Constr.constr Univ.in_universe_context_set * 'a
type 'a const_entry_body = 'a proof_output Future.computation
type constant_entry =
  1. | DefinitionEntry : definition_entry -> constant_entry
  2. | ParameterEntry : parameter_entry -> constant_entry
  3. | PrimitiveEntry : primitive_entry -> constant_entry
type module_struct_entry = Declarations.module_alg_expr
type module_params_entry = (Names.MBId.t * module_struct_entry) list
type module_type_entry = module_params_entry * module_struct_entry
OCaml

Innovation. Community. Security.