package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type set_predicativity =
  1. | ImpredicativeSet
  2. | PredicativeSet
type engagement = set_predicativity
type template_arity = {
  1. template_param_levels : Univ.Level.t option list;
  2. template_level : Univ.Universe.t;
}
type (!'a, !'b) declaration_arity =
  1. | RegularArity of 'a
  2. | TemplateArity of 'b
type inline = int option
type constant_def =
  1. | Undef of inline
  2. | Def of Constr.constr Mod_subst.substituted
  3. | OpaqueDef of Opaqueproof.opaque
type constant_universes =
  1. | Monomorphic_const of Univ.ContextSet.t
  2. | Polymorphic_const of Univ.AUContext.t
type typing_flags = {
  1. check_guarded : bool;
  2. check_universes : bool;
  3. conv_oracle : Conv_oracle.oracle;
  4. share_reduction : bool;
}
type constant_body = {
  1. const_hyps : Constr.named_context;
  2. const_body : constant_def;
  3. const_type : Constr.types;
  4. const_body_code : Cemitcodes.to_patch_substituted option;
  5. const_universes : constant_universes;
  6. const_inline_code : bool;
  7. const_typing_flags : typing_flags;
}
type recarg =
  1. | Norec
  2. | Mrec of Names.inductive
  3. | Imbr of Names.inductive
type wf_paths = recarg Rtree.t
type record_info =
  1. | NotRecord
  2. | FakeRecord
  3. | PrimRecord of (Names.Id.t * Names.Label.t array * Constr.types array) array
type regular_inductive_arity = {
  1. mind_user_arity : Constr.types;
  2. mind_sort : Sorts.t;
}
type one_inductive_body = {
  1. mind_typename : Names.Id.t;
  2. mind_arity_ctxt : Constr.rel_context;
  3. mind_arity : inductive_arity;
  4. mind_consnames : Names.Id.t array;
  5. mind_user_lc : Constr.types array;
  6. mind_nrealargs : int;
  7. mind_nrealdecls : int;
  8. mind_kelim : Sorts.family list;
  9. mind_nf_lc : Constr.types array;
  10. mind_consnrealargs : int array;
  11. mind_consnrealdecls : int array;
  12. mind_recargs : wf_paths;
  13. mind_nb_constant : int;
  14. mind_nb_args : int;
  15. mind_reloc_tbl : Vmvalues.reloc_table;
}
type abstract_inductive_universes =
  1. | Monomorphic_ind of Univ.ContextSet.t
  2. | Polymorphic_ind of Univ.AUContext.t
  3. | Cumulative_ind of Univ.ACumulativityInfo.t
type recursivity_kind =
  1. | Finite
  2. | CoFinite
  3. | BiFinite
type mutual_inductive_body = {
  1. mind_packets : one_inductive_body array;
  2. mind_record : record_info;
  3. mind_finite : recursivity_kind;
  4. mind_ntypes : int;
  5. mind_hyps : Constr.named_context;
  6. mind_nparams : int;
  7. mind_nparams_rec : int;
  8. mind_params_ctxt : Constr.rel_context;
  9. mind_universes : abstract_inductive_universes;
  10. mind_private : bool option;
  11. mind_typing_flags : typing_flags;
}
type (!'ty, !'a) functorize =
  1. | NoFunctor of 'a
  2. | MoreFunctor of Names.MBId.t * 'ty * ('ty, 'a) functorize
type with_declaration =
  1. | WithMod of Names.Id.t list * Names.ModPath.t
  2. | WithDef of Names.Id.t list * Constr.constr * Univ.AUContext.t option
type module_alg_expr =
  1. | MEident of Names.ModPath.t
  2. | MEapply of module_alg_expr * Names.ModPath.t
  3. | MEwith of module_alg_expr * with_declaration
type structure_field_body =
  1. | SFBconst of constant_body
  2. | SFBmind of mutual_inductive_body
  3. | SFBmodule of module_body
  4. | 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 =
  1. | Abstract
  2. | Algebraic of module_expression
  3. | Struct of module_signature
  4. | FullStruct
and !'a generic_module_body = {
  1. mod_mp : Names.ModPath.t;
  2. mod_expr : 'a;
  3. mod_type : module_signature;
  4. mod_type_alg : module_expression option;
  5. mod_constraints : Univ.ContextSet.t;
  6. mod_delta : Mod_subst.delta_resolver;
  7. mod_retroknowledge : 'a module_retroknowledge;
}
and module_body = module_implementation generic_module_body
and module_type_body = unit generic_module_body
and !_ module_retroknowledge =
  1. | ModBodyRK : Retroknowledge.action list -> module_implementation module_retroknowledge
  2. | ModTypeRK : unit module_retroknowledge