coq 8.7.2 · OCaml Package

type set_predicativity =

| ImpredicativeSet
| PredicativeSet

type engagement = set_predicativity

type template_arity = {

template_param_levels : Univ.universe_level option list;
template_level : Univ.universe;

}

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

| RegularArity of 'a
| TemplateArity of 'b

type constant_type =
  (Term.types, Context.Rel.t * template_arity) declaration_arity

type inline = int option

type projection_body = {

proj_ind : Names.mutual_inductive;
proj_npars : int;
proj_arg : int;
proj_type : Term.types;
proj_eta : Term.constr * Term.types;
proj_body : Term.constr;

}

type constant_def =

| Undef of inline
| Def of Term.constr Mod_subst.substituted
| OpaqueDef of Opaqueproof.opaque

type constant_universes =

| Monomorphic_const of Univ.universe_context
| Polymorphic_const of Univ.abstract_universe_context

type typing_flags = {

check_guarded : bool;
check_universes : bool;

}

type constant_body = {

const_hyps : Context.Named.t;
const_body : constant_def;
const_type : constant_type;
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 recarg =

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

type wf_paths = recarg Rtree.t

type record_body =
  (Names.Id.t * Names.constant array * projection_body array) option

type regular_inductive_arity = {

mind_user_arity : Term.types;
mind_sort : Term.sorts;

}

type inductive_arity =
  (regular_inductive_arity, template_arity) declaration_arity

type 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 : Term.types array;
mind_nrealargs : int;
mind_nrealdecls : int;
mind_kelim : Term.sorts_family list;
mind_nf_lc : Term.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.universe_context
| Polymorphic_ind of Univ.abstract_universe_context
| Cumulative_ind of Univ.abstract_cumulativity_info

type mutual_inductive_body = {

mind_packets : one_inductive_body array;
mind_record : record_body option;
mind_finite : Decl_kinds.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.module_path
| WithDef of Names.Id.t list * Term.constr Univ.in_universe_context

type module_alg_expr =

| MEident of Names.module_path
| MEapply of module_alg_expr * Names.module_path
| 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 module_body = {

mod_mp : Names.module_path;
mod_expr : module_implementation;
mod_type : module_signature;
mod_type_alg : module_expression option;
mod_constraints : Univ.ContextSet.t;
mod_delta : Mod_subst.delta_resolver;
mod_retroknowledge : Retroknowledge.action list;

}

and module_type_body = module_body

package coq