1 files changed, 59 insertions, 0 deletions
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
new file mode 100644
index 0000000000..72f9d3aa8c
--- /dev/null
+++ b/toplevel/mltop.mli
@@ -0,0 +1,59 @@
+
+(* $Id$ *)
+
+(* If there is a toplevel under Coq *)
+type toplevel = {
+  load_obj : string -> unit;
+  use_file : string -> unit;
+  add_dir : string -> unit }
+
+(* Determines the behaviour of Coq with respect to ML files (compiled 
+   or not) *) 
+type kind_load=
+  | WithTop of toplevel
+  | WithoutTop
+  | Native
+
+(*Sets and initializes the kind of loading*)
+val set : kind_load -> unit
+
+(*Resets the kind of loading*)
+val remove : unit -> unit
+
+(*Tests if an Ocaml toplevel runs under Coq*)
+val is_ocaml_top : unit -> bool
+
+(*Tests if we can load ML files*)
+val enable_load : unit -> 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 ML paths*)
+val dir_ml_dir : string -> unit
+
+val add_init_with_state : (unit -> unit) -> unit
+val init_with_state : unit -> unit
+
+(* List of modules linked to the toplevel *)
+val add_known_module : string -> unit
+val module_is_known : string -> bool
+val load_object : string -> string -> unit
+
+(* Summary of Declared ML Modules *)
+val get_loaded_modules : unit -> string list
+val add_loaded_module : string -> unit
+val init_ml_modules : unit -> unit
+val unfreeze_ml_modules : string list -> unit
+
+type ml_module_object = { mnames: string list }
+val inMLModule : ml_module_object -> Libobject.obj
+val outMLModule : Libobject.obj -> ml_module_object
+
+val declare_ml_modules : string list -> unit
+val print_ml_path : unit -> unit
+
+val print_ml_modules : unit -> unit