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 /config | |
| 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 'config')
| -rw-r--r-- | config/Makefile.template | 1 | ||||
| -rw-r--r-- | config/coq_config.mli | 2 |
2 files changed, 3 insertions, 0 deletions
diff --git a/config/Makefile.template b/config/Makefile.template index e0e7bf0b0..3fd726923 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -96,6 +96,7 @@ BEST=BESTCOMPILER # Your architecture # Can be obtain by UNIX command arch ARCH=ARCHITECTURE +HASNATDYNLINK=HASNATIVEDYNLINK # Your C compiler and co CC="CCEXEC" diff --git a/config/coq_config.mli b/config/coq_config.mli index 46404215f..e5a32708d 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -44,3 +44,5 @@ val with_geoproof : bool ref (* to (de)activate functions specific to Geoproof w val browser : string (** default web browser to use, may be overriden by environment variable COQREMOTEBROWSER *) + +val has_natdynlink : bool |