Module Declaremods.Interp

declare_module id fargs typ exprs declares module id, from functor arguments fargs, with final type typ. exprs is usually of length 1 (Module definition with a concrete body), but it could also be empty ("Declare Module", with non-empty typ), or multiple (body of the shape M <+ N <+ ...).

val end_module : unit -> Names.ModPath.t
Module types

declare_modtype interp_modast id fargs typs exprs Similar to declare_module, except that the types could be multiple

val declare_modtype : Names.Id.t -> module_params_expr -> module_expr list -> module_expr list -> Names.ModPath.t
val start_modtype : Names.Id.t -> module_params_expr -> module_expr list -> Names.ModPath.t
val end_modtype : unit -> Names.ModPath.t

import_module export mp imports the module mp. It modifies Nametab and performs the open_object function for every object of the module. Raises Not_found when mp is unknown or when mp corresponds to a functor. If export is true, the module is also opened every time the module containing it is.

val import_module : Libobject.open_filter -> export:Lib.export_flag -> Names.ModPath.t -> unit
val import_modules : export:Lib.export_flag -> (Libobject.open_filter * Names.ModPath.t) list -> unit

Same as import_module but for multiple modules, and more optimized than iterating import_module.

Include

val declare_include : module_expr list -> unit