package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
Toplevel management
module PluginSpec : sig ... end

Coq plugins are identified by their OCaml library name (in the Findlib sense)

type toplevel = {
  1. load_plugin : PluginSpec.t -> unit;
    (*

    Load a findlib library, given by public name

    *)
  2. load_module : string -> unit;
    (*

    Load a cmxs / cmo module, used by the native compiler to load objects

    *)
  3. add_dir : string -> unit;
    (*

    Adds a dir to the module search path

    *)
  4. ml_loop : unit -> unit;
    (*

    Implementation of Drop

    *)
}
val set_top : toplevel -> unit

Sets and initializes a toplevel (if any)

val load_module : string -> unit

Low level module loading, for the native compiler and similar users.

val remove : unit -> unit

Removes the toplevel (if any)

val is_ocaml_top : unit -> bool

Tests if an Ocaml toplevel runs under Coq

val ocaml_toploop : unit -> unit

Starts the Ocaml toplevel loop

val add_ml_dir : string -> unit

Adds a dir to the plugin search path, this also extends OCamlfind's search path

Tests if we can load ML files

val module_is_known : string -> bool
Initialization functions
val add_known_module : string -> unit

Declare a plugin which has been linked. A plugin is a findlib library name. Usually, this will be called automatically when use do DECLARE PLUGIN "pkg.lib" in the .mlg file.

The main effect is that dynlink will not be attempted for this plugin, so eg if it was statically linked Coq will not try and fail to find the cmxs.

val add_init_function : string -> (unit -> unit) -> unit

Declare a initialization function. The initialization function is called in Declare ML Module, including reruns after backtracking over it (either interactive backtrack, module closing backtrack, Require of a file with Declare ML Module).

val declare_cache_obj : (unit -> unit) -> string -> unit

Register a callback that will be called when the module is declared with the Declare ML Module command. This is useful to define Coq objects at that time only. Several functions can be defined for one module; they will be called in the order of declaration, and after the ML module has been properly initialized.

Unlike the init functions it does not run after closing a module or Requiring a file which contains the Declare ML Module. This allows to have effects which depend on the module when command was run in, eg add a named libobject which will use it for the prefix.

Declaring modules
val declare_ml_modules : Vernacexpr.locality_flag -> string list -> unit

Implementation of the Declare ML Module vernacular command.

Utilities
val print_ml_path : unit -> Pp.t
val print_ml_modules : unit -> Pp.t
val print_gc : unit -> Pp.t
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