Module `Mltop`

Toplevel management

type toplevel = { load_obj : string -> unit; use_file : string -> unit; add_dir : string -> unit; ml_loop : unit -> unit; }: If there is a toplevel under Coq, it is described by the following record.

val set_top : toplevel -> unit: Sets and initializes a toplevel (if any)

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

ML Dynlink

val add_ml_dir : recursive:bool -> string -> unit: Adds a dir to the plugin search path

val has_dynlink : bool: Tests if we can load ML files

val dir_ml_load : string -> unit: Dynamic loading of .cmo

val dir_ml_use : string -> unit: Dynamic interpretation of .ml

val add_known_module : string -> unit: List of modules linked to the toplevel

val module_is_known : string -> bool

Initialization functions

val add_known_plugin : (unit -> unit) -> string -> unit: Declare a plugin and its initialization function. A plugin is just an ML module with an initialization function. Adding a known plugin implies adding it as a known ML module. The initialization function is granted to be called after Coq is fully bootstrapped, even if the plugin is statically linked with the toplevel

val init_known_plugins : unit -> unit: Calls all initialization functions in a non-specified order

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.

Declaring modules

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

Utilities

val print_ml_path : unit -> Pp.t
val print_ml_modules : unit -> Pp.t
val print_gc : unit -> Pp.t