Module DeclareDef

type locality =
| Discharge
| Global of Declare.import_status
module Hook : sig ... end

Declaration hooks

val declare_definition : name:Names.Id.t -> scope:locality -> kind:Decls.logical_kind -> ?⁠hook_data:(Hook.t * UState.t * (Names.Id.t * Constr.t) list) -> UnivNames.universe_binders -> Evd.side_effects Declare.proof_entry -> Impargs.manual_implicits -> Names.GlobRef.t
val declare_fix : ?⁠opaque:bool -> ?⁠hook_data:(Hook.t * UState.t * (Names.Id.t * Constr.t) list) -> name:Names.Id.t -> scope:locality -> kind:Decls.definition_object_kind -> UnivNames.universe_binders -> Entries.universes_entry -> Evd.side_effects Entries.proof_output -> Constr.types -> Impargs.manual_implicits -> Names.GlobRef.t
val prepare_definition : allow_evars:bool -> ?⁠opaque:bool -> ?⁠inline:bool -> poly:bool -> Evd.evar_map -> UState.universe_decl -> types:EConstr.t option -> body:EConstr.t -> Evd.evar_map * Evd.side_effects Declare.proof_entry
val prepare_parameter : allow_evars:bool -> poly:bool -> Evd.evar_map -> UState.universe_decl -> EConstr.types -> Evd.evar_map * Entries.parameter_entry