diff options
Diffstat (limited to 'toplevel/mltop.mli')
| -rw-r--r-- | toplevel/mltop.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli index af638241c0..715355635e 100644 --- a/toplevel/mltop.mli +++ b/toplevel/mltop.mli @@ -64,7 +64,6 @@ val inMLModule : ml_module_object -> Libobject.obj val outMLModule : Libobject.obj -> ml_module_object val declare_ml_modules : string list -> unit -val load_initial_plugins : unit -> unit val print_ml_path : unit -> unit |