package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type local_entry =
  1. | LocalDefEntry of Constr.constr
  2. | LocalAssumEntry of Constr.constr
type inductive_universes =
  1. | Monomorphic_ind_entry of Univ.ContextSet.t
  2. | Polymorphic_ind_entry of Univ.UContext.t
  3. | Cumulative_ind_entry of Univ.CumulativityInfo.t
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 : (Names.Id.t * local_entry) list;
  4. mind_entry_inds : one_inductive_entry list;
  5. mind_entry_universes : inductive_universes;
  6. mind_entry_private : bool option;
}
type !'a proof_output = Constr.constr Univ.in_universe_context_set * 'a
type 'a const_entry_body = 'a proof_output Future.computation
type constant_universes_entry =
  1. | Monomorphic_const_entry of Univ.ContextSet.t
  2. | Polymorphic_const_entry of Univ.UContext.t
type !'a in_constant_universes_entry = 'a * constant_universes_entry
type !'a definition_entry = {
  1. const_entry_body : 'a const_entry_body;
  2. const_entry_secctx : Constr.named_context option;
  3. const_entry_feedback : Stateid.t option;
  4. const_entry_type : Constr.types option;
  5. const_entry_universes : constant_universes_entry;
  6. const_entry_opaque : bool;
  7. const_entry_inline_code : bool;
}
type section_def_entry = {
  1. secdef_body : Constr.constr;
  2. secdef_secctx : Constr.named_context option;
  3. secdef_feedback : Stateid.t option;
  4. secdef_type : Constr.types option;
}
type inline = int option
type parameter_entry = Constr.named_context option * Constr.types in_constant_universes_entry * inline
type !'a constant_entry =
  1. | DefinitionEntry of 'a definition_entry
  2. | ParameterEntry of parameter_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
type module_entry =
  1. | MType of module_params_entry * module_struct_entry
  2. | MExpr of module_params_entry * module_struct_entry * module_struct_entry option
type seff_env = [
  1. | `Nothing
  2. | `Opaque of Constr.t * Univ.ContextSet.t
]
type side_effect_role =
  1. | Subproof
  2. | Schema of Names.inductive * string
type side_eff = {
  1. seff_constant : Names.Constant.t;
  2. seff_body : Declarations.constant_body;
  3. seff_env : seff_env;
  4. seff_role : side_effect_role;
}