diff options
Diffstat (limited to 'topbin')
| -rw-r--r-- | topbin/coqtop_byte_bin.ml | 1 |
1 files changed, 0 insertions, 1 deletions
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); }) |