package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type !'a module_signature =
  1. | Enforce of 'a
  2. | Check of 'a list
type inline =
  1. | NoInline
  2. | DefaultInline
  3. | InlineAt of int
type module_params = (Names.lident list * (Constrexpr.module_ast * inline)) list
val end_module : unit -> Names.ModPath.t
val end_modtype : unit -> Names.ModPath.t
type library_name = Names.DirPath.t
type library_objects
val start_library : library_name -> unit
val end_library : ?except:Future.UUIDSet.t -> output_native_objects:bool -> library_name -> Safe_typing.compiled_library * library_objects * Nativelib.native_library
val append_end_library_hook : (unit -> unit) -> unit
val import_module : Libobject.open_filter -> export:bool -> Names.ModPath.t -> unit
val import_modules : export:bool -> (Libobject.open_filter * Names.ModPath.t) list -> unit
val declare_include : (Constrexpr.module_ast * inline) list -> unit
val iter_all_segments : (Libobject.object_name -> Libobject.t -> unit) -> unit
val debug_print_modtab : unit -> Pp.t
val process_module_binding : Names.MBId.t -> Declarations.module_alg_expr -> unit