coq 8.7.1 · OCaml Package

coq

type !'modast module_interpretor =
  Environ.env ->
  Misctypes.module_kind ->
  'modast ->
  Entries.module_struct_entry * Misctypes.module_kind

type !'modast module_params =
  (Names.Id.t Loc.located list * ('modast * Vernacexpr.inline)) list

val declare_module : 
  'modast module_interpretor ->
  Names.Id.t ->
  'modast module_params ->
  ('modast * Vernacexpr.inline) Vernacexpr.module_signature ->
  ('modast * Vernacexpr.inline) list ->
  Names.module_path

val start_module : 
  'modast module_interpretor ->
  bool option ->
  Names.Id.t ->
  'modast module_params ->
  ('modast * Vernacexpr.inline) Vernacexpr.module_signature ->
  Names.module_path

val end_module : unit -> Names.module_path

val declare_modtype : 
  'modast module_interpretor ->
  Names.Id.t ->
  'modast module_params ->
  ('modast * Vernacexpr.inline) list ->
  ('modast * Vernacexpr.inline) list ->
  Names.module_path

val start_modtype : 
  'modast module_interpretor ->
  Names.Id.t ->
  'modast module_params ->
  ('modast * Vernacexpr.inline) list ->
  Names.module_path

val end_modtype : unit -> Names.module_path

val xml_declare_module : (Names.module_path -> unit) Hook.t

val xml_start_module : (Names.module_path -> unit) Hook.t

val xml_end_module : (Names.module_path -> unit) Hook.t

val xml_declare_module_type : (Names.module_path -> unit) Hook.t

val xml_start_module_type : (Names.module_path -> unit) Hook.t

val xml_end_module_type : (Names.module_path -> unit) Hook.t

type library_name = Names.DirPath.t

type library_objects

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

val get_library_native_symbols : library_name -> Nativecode.symbols

val start_library : library_name -> unit

val end_library : 
  ?except:Future.UUIDSet.t ->
  library_name ->
  Safe_typing.compiled_library * library_objects * Safe_typing.native_library

val append_end_library_hook : (unit -> unit) -> unit

val really_import_module : Names.module_path -> unit

val import_module : bool -> Names.module_path -> unit

val declare_include : 
  'modast module_interpretor ->
  ('modast * Vernacexpr.inline) list ->
  unit

val iter_all_segments : (Libnames.object_name -> Libobject.obj -> unit) -> unit

val debug_print_modtab : unit -> Pp.std_ppcmds

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

package coq