diff options
| -rw-r--r-- | library/libobject.ml | 5 | ||||
| -rw-r--r-- | toplevel/mltop.ml4 | 6 | ||||
| -rw-r--r-- | toplevel/mltop.mli | 2 |
3 files changed, 7 insertions, 6 deletions
diff --git a/library/libobject.ml b/library/libobject.ml index d9ffe1cd5c..4cc2fdb350 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -143,8 +143,9 @@ let apply_dyn_fun deflt f lobj = Failure "local to_apply_dyn_fun" -> if not (!relax_flag || Hashtbl.mem missing_tab tag) then begin - Pp.warning ("Cannot find library functions for an object with tag " - ^ tag ^ " (a plugin may be missing)"); + Pp.msg_warning + (Pp.str ("Cannot find library functions for an object with tag " + ^ tag ^ " (a plugin may be missing)")); Hashtbl.add missing_tab tag () end; deflt diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 446efc9540..d9a261ed46 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -235,7 +235,7 @@ let add_known_module mname = let module_is_known mname = Stringset.mem (String.capitalize mname) !known_loaded_modules -let load_object mname fname= +let load_ml_object mname fname= dir_ml_load fname; add_known_module mname @@ -257,7 +257,7 @@ let unfreeze_ml_modules x = if not (module_is_known mname) then if has_dynlink then let fname = file_of_name mname in - load_object mname fname + load_ml_object mname fname else errorlabstrm "Mltop.unfreeze_ml_modules" (str"Loading of ML object file forbidden in a native Coq."); @@ -282,7 +282,7 @@ let cache_ml_module_object (_,{mnames=mnames}) = try if_verbose msg (str"[Loading ML file " ++ str fname ++ str" ..."); - load_object mname fname; + load_ml_object mname fname; if_verbose msgnl (str" done]"); add_loaded_module mname with e -> diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli index c625854eae..1e9c3b03c7 100644 --- a/toplevel/mltop.mli +++ b/toplevel/mltop.mli @@ -49,7 +49,7 @@ val add_rec_path : unix_path:string -> coq_root:Names.dir_path -> unit (** List of modules linked to the toplevel *) val add_known_module : string -> unit val module_is_known : string -> bool -val load_object : string -> string -> unit +val load_ml_object : string -> string -> unit (** Summary of Declared ML Modules *) val get_loaded_modules : unit -> string list |