[rfc] [mltop] Removal of dynamic loading of object and `.ml` files

This seems seldom used and I think in general instrumentation this way
is pretty limited (usually better to use the build system to tweak)

It thus seems worth removing as to simplify `Mltop` a bit, but of
course comments are welcome.

1 files changed, 0 insertions, 7 deletions

diff --git a/vernac/mltop.mli b/vernac/mltop.mli
index 56a28b64b0..271772d7ba 100644
--- a/vernac/mltop.mli
+++ b/vernac/mltop.mli
@@ -14,7 +14,6 @@
    record. *)
 type toplevel = {
   load_obj : string -> unit;
-  use_file : string -> unit;
   add_dir  : string -> unit;
   ml_loop  : unit -> unit }
 
@@ -38,12 +37,6 @@ val add_ml_dir : recursive:bool -> string -> unit
 (** 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
-
 (** List of modules linked to the toplevel *)
 val add_known_module : string -> unit
 val module_is_known : string -> bool