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 /ide | |
| 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 'ide')
| -rw-r--r-- | ide/coq.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 2c8d7b8db1..2d8c2ff99a 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -79,7 +79,7 @@ let version () = ver date Coq_config.arch Sys.os_type (let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z) - (if Mltop.get () = Mltop.Native then "native" else "bytecode") + (if Mltop.is_native then "native" else "bytecode") (if Coq_config.best="opt" then "native" else "bytecode") let is_in_coq_lib dir = |