Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

1 files changed, 10 insertions, 0 deletions

diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 1e9c3b03..99b96ed7 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -51,6 +51,16 @@ val add_known_module : string -> unit
 val module_is_known : string -> bool
 val load_ml_object : string -> 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 add_known_plugin : (unit -> unit) -> string -> unit
+
+(* Calls all initialization functions in a non-specified order *)
+val init_known_plugins : unit -> unit
+
 (** Summary of Declared ML Modules *)
 val get_loaded_modules : unit -> string list
 val add_loaded_module : string -> unit