Module `Declaremods`

Modules

type 'a module_signature = | Enforce of 'a ... : T | Check of 'a list ... <: T1 <: T2, possibly empty

type inline = | NoInline | DefaultInline | InlineAt of int

type module_params = (Names.lident list * (Constrexpr.module_ast * inline)) list

val declare_module : Names.Id.t -> module_params -> (Constrexpr.module_ast * inline) module_signature -> (Constrexpr.module_ast * inline) list -> Names.ModPath.t
val start_module : bool option -> Names.Id.t -> module_params -> (Constrexpr.module_ast * inline) module_signature -> Names.ModPath.t
val end_module : unit -> Names.ModPath.t

Module types

val declare_modtype : Names.Id.t -> module_params -> (Constrexpr.module_ast * inline) list -> (Constrexpr.module_ast * inline) list -> Names.ModPath.t
val start_modtype : Names.Id.t -> module_params -> (Constrexpr.module_ast * inline) list -> Names.ModPath.t
val end_modtype : unit -> Names.ModPath.t

Libraries i.e. modules on disk

type library_name = Names.DirPath.t
type library_objects

val register_library : library_name -> Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest -> Univ.ContextSet.t -> unit
val start_library : library_name -> unit
val end_library : output_native_objects:bool -> library_name -> Safe_typing.compiled_library * library_objects * Nativelib.native_library
val append_end_library_hook : (unit -> unit) -> unit: append a function to be executed at end_library

val import_module : Libobject.open_filter -> export:bool -> Names.ModPath.t -> unit
val import_modules : export:bool -> (Libobject.open_filter * Names.ModPath.t) list -> unit: Same as import_module but for multiple modules, and more optimized than iterating import_module.

val declare_include : (Constrexpr.module_ast * inline) list -> unit

...

val iter_all_segments : (Libobject.object_name -> Libobject.t -> unit) -> unit
val debug_print_modtab : unit -> Pp.t

val process_module_binding : Names.MBId.t -> Declarations.module_alg_expr -> unit