diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-28 18:43:16 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-28 18:43:16 +0000 |
| commit | aa77afa9d828d0bbb5d6fd5faf2e971b515a19fd (patch) | |
| tree | 3d7c44f018987d0048b1bcc4e87f88ac806e110b /README.doc | |
| 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 'README.doc')
0 files changed, 0 insertions, 0 deletions