diff options
Diffstat (limited to 'vernac')
-rw-r--r-- | vernac/mltop.ml | 9 | ||||
-rw-r--r-- | vernac/mltop.mli | 3 |
2 files changed, 0 insertions, 12 deletions
diff --git a/vernac/mltop.ml b/vernac/mltop.ml index 343b0925d..d25dea141 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -345,13 +345,6 @@ let load_ml_object mname ?path fname= let dir_ml_load m = ignore(dir_ml_load m) let add_known_module m = add_known_module m None -let load_ml_object_raw fname = dir_ml_load (file_of_name fname) -let load_ml_objects_raw_rex rex = - List.iter (fun (_,fp) -> - let name = file_of_name (Filename.basename fp) in - try dir_ml_load name - with e -> prerr_endline (Printexc.to_string e)) - (System.where_in_path_rex !coq_mlpath_copy rex) (* Summary of declared ML Modules *) @@ -396,8 +389,6 @@ let trigger_ml_object verb cache reinit ?path name = if cache then perform_cache_obj name end -let load_ml_object n m = ignore(load_ml_object n m) - let unfreeze_ml_modules x = reset_loaded_modules (); List.iter diff --git a/vernac/mltop.mli b/vernac/mltop.mli index da195f4fc..ed1f9a12d 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} *) |