package coq

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

type local_entry =

| LocalDefEntry of Constr.constr
| LocalAssumEntry of Constr.constr

type inductive_universes =

| Monomorphic_ind_entry of Univ.ContextSet.t
| Polymorphic_ind_entry of Univ.UContext.t
| Cumulative_ind_entry of Univ.CumulativityInfo.t

type one_inductive_entry = {

mind_entry_typename : Names.Id.t;
mind_entry_arity : Constr.constr;
mind_entry_template : bool;
mind_entry_consnames : Names.Id.t list;
mind_entry_lc : Constr.constr list;

}

type mutual_inductive_entry = {

mind_entry_record : Names.Id.t option option;
mind_entry_finite : Declarations.recursivity_kind;
mind_entry_params : (Names.Id.t * local_entry) list;
mind_entry_inds : one_inductive_entry list;
mind_entry_universes : inductive_universes;
mind_entry_private : bool option;

}

type !'a proof_output = Constr.constr Univ.in_universe_context_set * 'a

type 'a const_entry_body = 'a proof_output Future.computation

type constant_universes_entry =

| Monomorphic_const_entry of Univ.ContextSet.t
| Polymorphic_const_entry of Univ.UContext.t

type !'a in_constant_universes_entry = 'a * constant_universes_entry

type !'a definition_entry = {

const_entry_body : 'a const_entry_body;
const_entry_secctx : Context.Named.t option;
const_entry_feedback : Stateid.t option;
const_entry_type : Constr.types option;
const_entry_universes : constant_universes_entry;
const_entry_opaque : bool;
const_entry_inline_code : bool;

}

type section_def_entry = {

secdef_body : Constr.constr;
secdef_secctx : Context.Named.t option;
secdef_feedback : Stateid.t option;
secdef_type : Constr.types option;

}

type inline = int option

type parameter_entry =
  Context.Named.t option * Constr.types in_constant_universes_entry * inline

type projection_entry = {

proj_entry_ind : Names.MutInd.t;
proj_entry_arg : int;

}

type !'a constant_entry =

| DefinitionEntry of 'a definition_entry
| ParameterEntry of parameter_entry
| ProjectionEntry of projection_entry

type module_struct_entry = Declarations.module_alg_expr

type module_params_entry = (Names.MBId.t * module_struct_entry) list

type module_type_entry = module_params_entry * module_struct_entry

type module_entry =

| MType of module_params_entry * module_struct_entry
| MExpr of module_params_entry * module_struct_entry * module_struct_entry option

type seff_env = [

| `Nothing
| `Opaque of Constr.t * Univ.ContextSet.t

]

type side_eff =

| SEsubproof of Names.Constant.t * Declarations.constant_body * seff_env
| SEscheme of (Names.inductive * Names.Constant.t * Declarations.constant_body * seff_env) list * string

type side_effect = {

from_env : Declarations.structure_body CEphemeron.key;
eff : side_eff;

}