coq 8.9.1 · OCaml Package

coq

type set_predicativity =

| ImpredicativeSet
| PredicativeSet

type engagement = set_predicativity

type template_arity = {

template_param_levels : Univ.Level.t option list;
template_level : Univ.Universe.t;

}

type (!'a, !'b) declaration_arity =

| RegularArity of 'a
| TemplateArity of 'b

type inline = int option

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 typing_flags = {

check_guarded : bool;
check_universes : bool;
conv_oracle : Conv_oracle.oracle;
share_reduction : bool;

}

type constant_body = {

const_hyps : Constr.named_context;
const_body : constant_def;
const_type : Constr.types;
const_body_code : Cemitcodes.to_patch_substituted option;
const_universes : constant_universes;
const_inline_code : bool;
const_typing_flags : typing_flags;

}

type recarg =

| Norec
| Mrec of Names.inductive
| Imbr of Names.inductive

type wf_paths = recarg Rtree.t

type record_info =

| NotRecord
| FakeRecord
| PrimRecord of (Names.Id.t * Names.Label.t array * Constr.types array) array

type regular_inductive_arity = {

mind_user_arity : Constr.types;
mind_sort : Sorts.t;

}

type inductive_arity =
  (regular_inductive_arity, template_arity) declaration_arity

type one_inductive_body = {

mind_typename : Names.Id.t;
mind_arity_ctxt : Constr.rel_context;
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 : Vmvalues.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 recursivity_kind =

| Finite
| CoFinite
| BiFinite

type mutual_inductive_body = {

mind_packets : one_inductive_body array;
mind_record : record_info;
mind_finite : recursivity_kind;
mind_ntypes : int;
mind_hyps : Constr.named_context;
mind_nparams : int;
mind_nparams_rec : int;
mind_params_ctxt : Constr.rel_context;
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) list

and module_signature = (module_type_body, structure_body) functorize

and module_expression = (module_type_body, module_alg_expr) functorize

and 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_body

and module_type_body = unit generic_module_body

and !_ module_retroknowledge =

| ModBodyRK : Retroknowledge.action list -> module_implementation module_retroknowledge
| ModTypeRK : unit module_retroknowledge

package coq