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_level : Univ.Universe.t;
}
type template_universes = {
  1. template_param_levels : Univ.Level.t option list;
  2. template_context : Univ.ContextSet.t;
}
type (!'a, !'b) declaration_arity =
  1. | RegularArity of 'a
  2. | TemplateArity of 'b
type inline = int option
type (!'a, !'opaque) constant_def =
  1. | Undef of inline
  2. | Def of 'a
  3. | OpaqueDef of 'opaque
  4. | Primitive of CPrimitives.t
type universes =
  1. | Monomorphic of Univ.ContextSet.t
  2. | Polymorphic of Univ.AUContext.t
type typing_flags = {
  1. check_guarded : bool;
  2. check_positive : bool;
  3. check_universes : bool;
  4. conv_oracle : Conv_oracle.oracle;
  5. share_reduction : bool;
  6. enable_VM : bool;
  7. enable_native_compiler : bool;
  8. indices_matter : bool;
  9. cumulative_sprop : bool;
  10. allow_uip : bool;
}
type !'opaque constant_body = {
  1. const_hyps : Constr.named_context;
  2. const_body : (Constr.t Mod_subst.substituted, 'opaque) constant_def;
  3. const_type : Constr.types;
  4. const_relevance : Sorts.relevance;
  5. const_body_code : Vmemitcodes.to_patch_substituted option;
  6. const_universes : universes;
  7. const_inline_code : bool;
  8. const_typing_flags : typing_flags;
}
type nested_type =
  1. | NestedInd of Names.inductive
  2. | NestedPrimitive of Names.Constant.t
type recarg =
  1. | Norec
  2. | Mrec of Names.inductive
  3. | Nested of nested_type
type wf_paths = recarg Rtree.t
type record_info =
  1. | NotRecord
  2. | FakeRecord
  3. | PrimRecord of (Names.Id.t * Names.Label.t array * Sorts.relevance 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;
  9. mind_nf_lc : (Constr.rel_context * Constr.types) array;
  10. mind_consnrealargs : int array;
  11. mind_consnrealdecls : int array;
  12. mind_recargs : wf_paths;
  13. mind_relevance : Sorts.relevance;
  14. mind_nb_constant : int;
  15. mind_nb_args : int;
  16. mind_reloc_tbl : Vmvalues.reloc_table;
}
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 : universes;
  10. mind_template : template_universes option;
  11. mind_variance : Univ.Variance.t array option;
  12. mind_sec_variance : Univ.Variance.t array option;
  13. mind_private : bool option;
  14. 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 Opaqueproof.opaque 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_delta : Mod_subst.delta_resolver;
  6. 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