Module MltopSource

Toplevel management
Sourcemodule PluginSpec : sig ... end

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

Sourcetype 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

    *)
}
Sourceval set_top : toplevel -> unit

Sets and initializes a toplevel (if any)

Sourceval remove : unit -> unit

Removes the toplevel (if any)

Sourceval is_ocaml_top : unit -> bool

Tests if an Ocaml toplevel runs under Coq

Sourceval ocaml_toploop : unit -> unit

Starts the Ocaml toplevel loop

Sourceval 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

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

Declare a plugin without an initialization function. A plugin is a findlib library name. Usually, this will be called automatically when use do DECLARE PLUGIN "pkg.lib" in the .mlg file.

Sourceval add_known_plugin : (unit -> unit) -> string -> unit

Declare a plugin plus a Coq-specific initialization function. The initialization function is granted to be called after Coq is fully bootstrapped, even if the plugin is statically linked with the toplevel

Sourceval init_known_plugins : unit -> unit

Calls all initialization functions in a non-specified order

Sourceval 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.

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

Implementation of the Declare ML Module vernacular command.

Utilities
Sourceval print_ml_path : unit -> Pp.t
Sourceval print_ml_modules : unit -> Pp.t
Sourceval print_gc : unit -> Pp.t