Declaremods.Interpdeclare_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 declare_module : Names.Id.t -> module_params_expr -> module_expr module_signature -> module_expr list -> Names.ModPath.tval start_module : Lib.export -> Names.Id.t -> module_params_expr -> module_expr module_signature -> Names.ModPath.tval end_module : unit -> Names.ModPath.tdeclare_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.tval start_modtype : Names.Id.t -> module_params_expr -> module_expr list -> Names.ModPath.tval end_modtype : unit -> Names.ModPath.tval register_library : library_name -> Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest -> Vmlibrary.on_disk -> unitimport_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 -> unitval import_modules : export:Lib.export_flag -> (Libobject.open_filter * Names.ModPath.t) list -> unitSame as import_module but for multiple modules, and more optimized than iterating import_module.
Include
val declare_include : module_expr list -> unit