package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type !'modast module_params = (Misctypes.lident 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.ModPath.t
val start_module : 'modast module_interpretor -> bool option -> Names.Id.t -> 'modast module_params -> ('modast * Vernacexpr.inline) Vernacexpr.module_signature -> Names.ModPath.t
val end_module : unit -> Names.ModPath.t
val declare_modtype : 'modast module_interpretor -> Names.Id.t -> 'modast module_params -> ('modast * Vernacexpr.inline) list -> ('modast * Vernacexpr.inline) list -> Names.ModPath.t
val start_modtype : 'modast module_interpretor -> Names.Id.t -> 'modast module_params -> ('modast * Vernacexpr.inline) list -> Names.ModPath.t
val end_modtype : unit -> Names.ModPath.t
type library_name = Names.DirPath.t
type library_objects
val get_library_native_symbols : library_name -> Nativecode.symbols
val start_library : library_name -> unit
val append_end_library_hook : (unit -> unit) -> unit
val really_import_module : Names.ModPath.t -> unit
val import_module : bool -> Names.ModPath.t -> 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.t
val process_module_binding : Names.MBId.t -> Declarations.module_alg_expr -> unit
OCaml

Innovation. Community. Security.