If there is a toplevel under Coq, it is described by the following record.

Sets and initializes a toplevel (if any)

Removes the toplevel (if any)

Tests if an Ocaml toplevel runs under Coq

Starts the Ocaml toplevel loop

Adds a dir to the plugin search path

Tests if we can load ML files

List of modules linked to the toplevel

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

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.