Module Declare

type 'a proof_entry = private {
proof_entry_body : 'a Entries.const_entry_body;
proof_entry_secctx : Names.Id.Set.t option;
proof_entry_feedback : Stateid.t option;
proof_entry_type : Constr.types option;
proof_entry_universes : Entries.universes_entry;
proof_entry_opaque : bool;
proof_entry_inline_code : bool;
}

Proof entries

type variable_declaration =
| SectionLocalDef of Evd.side_effects proof_entry
| SectionLocalAssum of {
typ : Constr.types;
impl : Glob_term.binding_kind;
}
type 'a constant_entry =
| DefinitionEntry of 'a proof_entry
| ParameterEntry of Entries.parameter_entry
| PrimitiveEntry of Entries.primitive_entry
val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
val declare_variable : name:Names.variable -> kind:Decls.logical_kind -> variable_declaration -> unit
val definition_entry : ?⁠fix_exn:Future.fix_exn -> ?⁠opaque:bool -> ?⁠inline:bool -> ?⁠types:Constr.types -> ?⁠univs:Entries.universes_entry -> ?⁠eff:Evd.side_effects -> Constr.constr -> Evd.side_effects proof_entry
val pure_definition_entry : ?⁠fix_exn:Future.fix_exn -> ?⁠opaque:bool -> ?⁠inline:bool -> ?⁠types:Constr.types -> ?⁠univs:Entries.universes_entry -> Constr.constr -> unit proof_entry
val delayed_definition_entry : ?⁠opaque:bool -> ?⁠inline:bool -> ?⁠feedback_id:Stateid.t -> ?⁠section_vars:Names.Id.Set.t -> ?⁠univs:Entries.universes_entry -> ?⁠types:Constr.types -> 'a Entries.const_entry_body -> 'a proof_entry
type import_status =
| ImportDefaultBehavior
| ImportNeedQualified
val declare_constant : ?⁠local:import_status -> name:Names.Id.t -> kind:Decls.logical_kind -> Evd.side_effects constant_entry -> Names.Constant.t

declare_constant id cd declares a global declaration (constant/parameter) with name id in the current section; it returns the full path of the declaration

internal specify if the constant has been created by the kernel or by the user, and in the former case, if its errors should be silent

val declare_private_constant : ?⁠role:Evd.side_effect_role -> ?⁠local:import_status -> name:Names.Id.t -> kind:Decls.logical_kind -> unit proof_entry -> Names.Constant.t * Evd.side_effects
val inline_private_constants : univs:UState.t -> Environ.env -> Evd.side_effects proof_entry -> Constr.t * UState.t

inline_private_constants ~sideff ~univs env ce will inline the constants in ce's body and return the body plus the updated UState.t.

val definition_message : Names.Id.t -> unit
val assumption_message : Names.Id.t -> unit
val fixpoint_message : int array option -> Names.Id.t list -> unit
val cofixpoint_message : Names.Id.t list -> unit
val recursive_message : bool -> int array option -> Names.Id.t list -> unit
val check_exists : Names.Id.t -> unit
exception AlreadyDeclared of string option * Names.Id.t
module Internal : sig ... end