From aa77afa9d828d0bbb5d6fd5faf2e971b515a19fd Mon Sep 17 00:00:00 2001
From: glondu
Date: Tue, 28 Oct 2008 18:43:16 +0000
Subject: Native "Declare ML Module" when possible

Dynlink.add_{interfaces,available_units} are deprecated and not
implemented natively. Currently, native "Declare ML Module" doesn't
work because of this. Dynlink-related should be switched to the API
introduced in OCaml 3.07.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11518 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 scripts/coqmktop.ml | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

(limited to 'scripts')

diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index c89ea827e7..021b1a80d0 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -83,7 +83,8 @@ let module_of_file name =
 
 (* Build the list of files to link and the list of modules names *)
 let files_to_link userfiles =
-  let dyn_objs = if not !opt then dynobjs else [] in
+  let dyn_objs =
+    if not !opt || Coq_config.has_natdynlink then dynobjs else [] in
   let toplevel_objs =
     if !top then topobjs else if !opt then notopobjs else [] in
   let ide_objs = if !coqide then 
@@ -240,17 +241,15 @@ let tmp_dynlink()=
 
 (* Initializes the kind of loading in the main program *)
 let declare_loading_string () =
-  if !opt then
-    "Mltop.set Mltop.Native;;\n"
-  else if not !top then
-    "Mltop.set Mltop.WithoutTop;;\n"
+  if not !top then
+    "Mltop.remove ();;"
   else
     "let ppf = Format.std_formatter;;
-     Mltop.set (Mltop.WithTop
+     Mltop.set_top
        {Mltop.load_obj=Topdirs.dir_load ppf;
         Mltop.use_file=Topdirs.dir_use ppf;
         Mltop.add_dir=Topdirs.dir_directory;
-        Mltop.ml_loop=(fun () -> Toploop.loop ppf) });;\n"
+        Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\n"
 
 (* create a temporary main file to link *)
 let create_tmp_main_file modules =
-- 
cgit v1.2.3