diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-31 21:19:15 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-31 21:19:15 +0000 |
| commit | f35a2ddd119ca99e924c68e3346a07087811c261 (patch) | |
| tree | d44b62f7c09f284ba05a48191866a80359d4f6c0 /toplevel/mltop.ml4 | |
| parent | 5b7992d4650e0aea9c34cdc08c00d292a000928c (diff) | |
Minor code improvements around libobject
- renamed load_object in mltop into load_ml_object to avoid confusion
with load_object in library
- flushed the liboject warning in real time
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13596 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/mltop.ml4')
| -rw-r--r-- | toplevel/mltop.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 446efc954..d9a261ed4 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 -> |