1 files changed, 102 insertions, 0 deletions
diff --git a/vernac/mltop.mli b/vernac/mltop.mli
new file mode 100644
index 00000000..da195f4f
--- /dev/null
+++ b/vernac/mltop.mli
@@ -0,0 +1,102 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** {5 Toplevel management} *)
+
+(** If there is a toplevel under Coq, it is described by the following
+   record. *)
+type toplevel = {
+  load_obj : string -> unit;
+  use_file : string -> unit;
+  add_dir  : string -> unit;
+  ml_loop  : unit -> unit }
+
+(** Sets and initializes a toplevel (if any) *)
+val set_top : toplevel -> unit
+
+(** Are we in a native version of Coq? *)
+val is_native : bool
+
+(** Removes the toplevel (if any) *)
+val remove : unit -> unit
+
+(** Tests if an Ocaml toplevel runs under Coq *)
+val is_ocaml_top : unit -> bool
+
+(** Starts the Ocaml toplevel loop *)
+val ocaml_toploop : unit -> unit
+
+(** {5 ML Dynlink} *)
+
+(** Tests if we can load ML files *)
+val has_dynlink : bool
+
+(** Dynamic loading of .cmo *)
+val dir_ml_load : string -> unit
+
+(** Dynamic interpretation of .ml *)
+val dir_ml_use : string -> unit
+
+(** Adds a path to the Coq and ML paths *)
+type add_ml = AddNoML | AddTopML | AddRecML
+
+type vo_path_spec = {
+  unix_path : string;           (* Filesystem path contaning vo/ml files *)
+  coq_path  : Names.DirPath.t;  (* Coq prefix for the path *)
+  implicit  : bool;             (* [implicit = true] avoids having to qualify with [coq_path] *)
+  has_ml    : add_ml;           (* If [has_ml] is true, the directory will also be search for plugins *)
+}
+
+type coq_path_spec =
+  | VoPath of vo_path_spec
+  | MlPath of string
+
+type coq_path = {
+  path_spec: coq_path_spec;
+  recursive: bool;
+}
+
+val add_coq_path : coq_path -> unit
+
+(** List of modules linked to the toplevel *)
+val add_known_module : string -> unit
+val module_is_known : string -> bool
+val load_ml_object : string -> string -> unit
+val load_ml_object_raw : string -> unit
+val load_ml_objects_raw_rex : Str.regexp -> unit
+
+(** {5 Initialization functions} *)
+
+(** 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
+
+(** 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. *)
+val declare_cache_obj : (unit -> unit) -> string -> unit
+
+(** {5 Declaring modules} *)
+
+val declare_ml_modules : Vernacexpr.locality_flag -> string list -> unit
+
+(** {5 Utilities} *)
+
+val print_ml_path : unit -> Pp.t
+val print_ml_modules : unit -> Pp.t
+val print_gc : unit -> Pp.t