package coq
type inductive_universes = | Monomorphic_ind_entry of Univ.universe_context| Polymorphic_ind_entry of Univ.universe_context| Cumulative_ind_entry of Univ.cumulativity_info
type one_inductive_entry = {mind_entry_typename : Names.Id.t;mind_entry_arity : Term.constr;mind_entry_template : bool;mind_entry_consnames : Names.Id.t list;mind_entry_lc : Term.constr list;
}type mutual_inductive_entry = {mind_entry_record : Names.Id.t option option;mind_entry_finite : Decl_kinds.recursivity_kind;mind_entry_params : (Names.Id.t * local_entry) list;mind_entry_inds : one_inductive_entry list;mind_entry_universes : inductive_universes;mind_entry_private : bool option;
}type !'a proof_output = Term.constr Univ.in_universe_context_set * 'atype 'a const_entry_body = 'a proof_output Future.computationtype !'a definition_entry = {const_entry_body : 'a const_entry_body;const_entry_secctx : Context.Named.t option;const_entry_feedback : Stateid.t option;const_entry_type : Term.types option;const_entry_polymorphic : bool;const_entry_universes : Univ.universe_context;const_entry_opaque : bool;const_entry_inline_code : bool;
}type parameter_entry =
Context.Named.t option * bool * Term.types Univ.in_universe_context * inlinetype !'a constant_entry = | DefinitionEntry of 'a definition_entry| ParameterEntry of parameter_entry| ProjectionEntry of projection_entry
type module_struct_entry = Declarations.module_alg_exprtype module_params_entry = (Names.MBId.t * module_struct_entry) listtype module_type_entry = module_params_entry * module_struct_entrytype module_entry = | MType of module_params_entry * module_struct_entry| MExpr of module_params_entry * module_struct_entry * module_struct_entry option
type side_eff = | SEsubproof of Names.constant * Declarations.constant_body * seff_env| SEscheme of (Names.inductive * Names.constant * Declarations.constant_body * seff_env) list * string