Module `DeclareDef`

val get_locality : Names.Id.t -> kind:string -> Decl_kinds.locality -> bool
val declare_definition : ontop:Proof_global.t option -> Names.Id.t -> Decl_kinds.definition_kind -> ?⁠hook_data:(Lemmas.declaration_hook * UState.t * (Names.Id.t * Constr.t) list) -> Safe_typing.private_constants Entries.definition_entry -> UnivNames.universe_binders -> Impargs.manual_implicits -> Names.GlobRef.t
val declare_fix : ontop:Proof_global.t option -> ?⁠opaque:bool -> ?⁠hook_data:(Lemmas.declaration_hook * UState.t * (Names.Id.t * Constr.t) list) -> Decl_kinds.definition_kind -> UnivNames.universe_binders -> Entries.universes_entry -> Names.Id.t -> Safe_typing.private_constants 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 * Safe_typing.private_constants Entries.definition_entry
val prepare_parameter : allow_evars:bool -> poly:bool -> Evd.evar_map -> UState.universe_decl -> EConstr.types -> Evd.evar_map * Entries.parameter_entry