Interp (coq-core.Declaremods.Interp)

val declare_module : 
  Names.Id.t ->
  module_params_expr ->
  module_expr module_signature ->
  module_expr list ->
  Names.ModPath.t

val start_module : 
  Lib.export ->
  Names.Id.t ->
  module_params_expr ->
  module_expr module_signature ->
  Names.ModPath.t

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

val register_library : 
  library_name ->
  Safe_typing.compiled_library ->
  library_objects ->
  Safe_typing.vodigest ->
  Univ.ContextSet.t ->
  unit

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