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 * Safe_typing.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
val mod_ops : Printmod.mod_ops
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct