diff options
| author | glondu | 2008-10-28 18:43:16 +0000 |
|---|---|---|
| committer | glondu | 2008-10-28 18:43:16 +0000 |
| commit | aa77afa9d828d0bbb5d6fd5faf2e971b515a19fd (patch) | |
| tree | 3d7c44f018987d0048b1bcc4e87f88ac806e110b /scripts/coqmktop.ml | |
| parent | 578f31889234edba078e14f4152421123c1bc466 (diff) | |
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
Diffstat (limited to 'scripts/coqmktop.ml')
| -rw-r--r-- | scripts/coqmktop.ml | 13 |
1 files changed, 6 insertions, 7 deletions
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 = |