From ab2ce06bffb0f06be96af24c0be546f5ebd11471 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 16 Jan 2020 20:07:41 +0100
Subject: [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.
---
 topbin/coqtop_byte_bin.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'topbin')

diff --git a/topbin/coqtop_byte_bin.ml b/topbin/coqtop_byte_bin.ml
index 85d8a48eda..604c6e251a 100644
--- a/topbin/coqtop_byte_bin.ml
+++ b/topbin/coqtop_byte_bin.ml
@@ -31,7 +31,6 @@ let drop_setup () =
            { load_obj = (fun f -> if not (Topdirs.load_file ppf f)
                           then CErrors.user_err Pp.(str ("Could not load plugin "^f))
                         );
-             use_file = Topdirs.dir_use ppf;
              add_dir  = Topdirs.dir_directory;
              ml_loop  = (fun () -> Toploop.loop ppf);
            })
-- 
cgit v1.2.3