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

2 files changed, 0 insertions, 38 deletions

diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 021b1a80d0..320cbe1824 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -199,44 +199,10 @@ let clean file =
     rm (basename ^ ".cmx")
   end
 
-(* Gives all modules in [dir]. Uses [.cmi] suffixes. Uses [Unix]. *)
-let all_modules_in_dir dir =
-  try
-    let lst = ref []
-    and dh = Unix.opendir dir in
-    try
-      while true do
-	let stg = Unix.readdir dh in
-        if (Filename.check_suffix stg ".cmi") then
-          lst := !lst @ [String.capitalize (Filename.chop_suffix stg ".cmi")]
-      done;
-      []
-    with End_of_file -> 
-      Unix.closedir dh; !lst
-  with Unix.Unix_error (_,"opendir",_) ->
-    failwith ("all_modules_in_dir: directory "^dir^" not found")
-
-(* Gives a part of command line (corresponding to dir) for [extract_crc] *)
-let crc_cmd dir =
-  " -I "^dir^(List.fold_right (fun x y -> " "^x^y) (all_modules_in_dir dir)
-  "")
-
-(* Same as [crc_cmd] but recursively *)
-let rec_crc_cmd dir =
-  List.fold_right (fun x y -> x^y) (List.map crc_cmd (all_subdirs dir)) ""
-
 (* Creates another temporary file for Dynlink if needed *)
 let tmp_dynlink()=
   let tmp = Filename.temp_file "coqdynlink" ".ml" in
   let _ = Sys.command ("echo \"Dynlink.init();;\" > "^tmp) in
-  let _ = Sys.command (Coq_config.camllib^"/extract_crc"^(crc_cmd
-      Coq_config.camllib)^(crc_cmd Coq_config.camlp4lib)^(rec_crc_cmd
-      Coq_config.coqtop)^" >> "^tmp) in
-  let _ = Sys.command ("echo \";;\" >> "^tmp) in
-  let _ = 
-    Sys.command ("echo \"Dynlink.add_available_units crc_unit_list;;\" >> "^
-		 tmp)
-  in
   tmp
 
 (* Initializes the kind of loading in the main program *)
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 4cf1f134fc..275f9a5f79 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