package coq
type engagement = set_predicativitytype template_arity = {template_param_levels : Univ.Level.t option list;template_level : Univ.Universe.t;
}type projection_body = {proj_ind : Names.MutInd.t;proj_npars : int;proj_arg : int;proj_type : Constr.types;proj_eta : Constr.constr * Constr.types;proj_body : Constr.constr;
}type constant_def = | Undef of inline| Def of Constr.constr Mod_subst.substituted| OpaqueDef of Opaqueproof.opaque
type constant_universes = | Monomorphic_const of Univ.ContextSet.t| Polymorphic_const of Univ.AUContext.t
type constant_body = {const_hyps : Context.Named.t;const_body : constant_def;const_type : Constr.types;const_body_code : Cemitcodes.to_patch_substituted option;const_universes : constant_universes;const_proj : projection_body option;const_inline_code : bool;const_typing_flags : typing_flags;
}type record_body =
(Names.Id.t * Names.Constant.t array * projection_body array) optiontype inductive_arity =
(regular_inductive_arity, template_arity) declaration_aritytype one_inductive_body = {mind_typename : Names.Id.t;mind_arity_ctxt : Context.Rel.t;mind_arity : inductive_arity;mind_consnames : Names.Id.t array;mind_user_lc : Constr.types array;mind_nrealargs : int;mind_nrealdecls : int;mind_kelim : Sorts.family list;mind_nf_lc : Constr.types array;mind_consnrealargs : int array;mind_consnrealdecls : int array;mind_recargs : wf_paths;mind_nb_constant : int;mind_nb_args : int;mind_reloc_tbl : Cbytecodes.reloc_table;
}type abstract_inductive_universes = | Monomorphic_ind of Univ.ContextSet.t| Polymorphic_ind of Univ.AUContext.t| Cumulative_ind of Univ.ACumulativityInfo.t
type mutual_inductive_body = {mind_packets : one_inductive_body array;mind_record : record_body option;mind_finite : recursivity_kind;mind_ntypes : int;mind_hyps : Context.Named.t;mind_nparams : int;mind_nparams_rec : int;mind_params_ctxt : Context.Rel.t;mind_universes : abstract_inductive_universes;mind_private : bool option;mind_typing_flags : typing_flags;
}type (!'ty, !'a) functorize = | NoFunctor of 'a| MoreFunctor of Names.MBId.t * 'ty * ('ty, 'a) functorize
type with_declaration = | WithMod of Names.Id.t list * Names.ModPath.t| WithDef of Names.Id.t list * Constr.constr * Univ.AUContext.t option
type module_alg_expr = | MEident of Names.ModPath.t| MEapply of module_alg_expr * Names.ModPath.t| MEwith of module_alg_expr * with_declaration
type structure_field_body = | SFBconst of constant_body| SFBmind of mutual_inductive_body| SFBmodule of module_body| SFBmodtype of module_type_body
and structure_body = (Names.Label.t * structure_field_body) listand module_signature = (module_type_body, structure_body) functorizeand module_expression = (module_type_body, module_alg_expr) functorizeand module_implementation = | Abstract| Algebraic of module_expression| Struct of module_signature| FullStruct
and !'a generic_module_body = {mod_mp : Names.ModPath.t;mod_expr : 'a;mod_type : module_signature;mod_type_alg : module_expression option;mod_constraints : Univ.ContextSet.t;mod_delta : Mod_subst.delta_resolver;mod_retroknowledge : 'a module_retroknowledge;
}and module_body = module_implementation generic_module_bodyand module_type_body = unit generic_module_bodyand !_ module_retroknowledge = | ModBodyRK : Retroknowledge.action list -> module_implementation module_retroknowledge| ModTypeRK : unit module_retroknowledge