summaryrefslogtreecommitdiff
path: root/vernac/mltop.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/mltop.mli')
-rw-r--r--vernac/mltop.mli3
1 files changed, 0 insertions, 3 deletions
diff --git a/vernac/mltop.mli b/vernac/mltop.mli
index da195f4f..ed1f9a12 100644
--- a/vernac/mltop.mli
+++ b/vernac/mltop.mli
@@ -68,9 +68,6 @@ val add_coq_path : coq_path -> unit
(** List of modules linked to the toplevel *)
val add_known_module : string -> unit
val module_is_known : string -> bool
-val load_ml_object : string -> string -> unit
-val load_ml_object_raw : string -> unit
-val load_ml_objects_raw_rex : Str.regexp -> unit
(** {5 Initialization functions} *)