Module `DeclareDef`

type locality = Declare.locality = | Discharge | Global of Declare.import_status

val declare_definition : name:Names.Id.t -> scope:Declare.locality -> kind:Decls.logical_kind -> opaque:bool -> impargs:Impargs.manual_implicits -> udecl:UState.universe_decl -> ?⁠hook:Declare.Hook.t -> ?⁠obls:(Names.Id.t * Constr.t) list -> poly:bool -> ?⁠inline:bool -> types:EConstr.t option -> body:EConstr.t -> ?⁠fix_exn:(Exninfo.iexn -> Exninfo.iexn) -> Evd.evar_map -> Names.GlobRef.t

module Hook = Declare.Hook