package coq
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=36577b55f4a4b1c64682c387de7abea932d0fd42fc0cd5406927dca344f53587
doc/coq-core.vernac/Mltop/index.html
Module MltopSource
Toplevel management
Coq plugins are identified by their OCaml library name (in the Findlib sense)
type toplevel = {load_plugin : PluginSpec.t -> unit;(*Load a findlib library, given by public name
*)load_module : string -> unit;(*Load a cmxs / cmo module, used by the native compiler to load objects
*)add_dir : string -> unit;(*Adds a dir to the module search path
*)ml_loop : unit -> unit;(*Implementation of Drop
*)
}Removes the toplevel (if any)
Tests if an Ocaml toplevel runs under Coq
Starts the Ocaml toplevel loop
ML Dynlink
Adds a dir to the plugin search path, this also extends OCamlfind's search path
Tests if we can load ML files
Initialization functions
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.
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
Calls all initialization functions in a non-specified order
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
Implementation of the Declare ML Module vernacular command.