diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-29 19:35:05 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-29 19:35:05 +0000 |
| commit | 3f9eb6ebe5217eaa929ef5632881460692e071f8 (patch) | |
| tree | e14c11d17545358dc24acd0d247cb2b5a459ea88 /toplevel | |
| parent | f3f1b6cece86b785e1cf58fd5f1e273dbeceb92b (diff) | |
Remove calls to Dynlink.add_{interfaces,available_units} altogether
According to OCaml's Changes, all modules loaded so far (and
statically linked) are available to dynamically loaded modules (since
3.07). Therefore, these calls seem irrelevant now.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11522 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/mltop.ml4 | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 4cf1f134f..275f9a5f7 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -109,10 +109,6 @@ let dir_ml_load s = let _,gname = where_in_path true !coq_mlpath_copy s in try Dynlink.loadfile gname; - Dynlink.add_interfaces - [(String.capitalize (Filename.chop_suffix - (Filename.basename gname) ".cmo"))] - [Filename.dirname gname] with | Dynlink.Error a -> errorlabstrm "Mltop.load_object" (str (Dynlink.error_message a)) ELSE |