aboutsummaryrefslogtreecommitdiffhomepage
path: root/config/coq_config.mli
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-10-28 18:43:16 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-10-28 18:43:16 +0000
commitaa77afa9d828d0bbb5d6fd5faf2e971b515a19fd (patch)
tree3d7c44f018987d0048b1bcc4e87f88ac806e110b /config/coq_config.mli
parent578f31889234edba078e14f4152421123c1bc466 (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/coq_config.mli')
-rw-r--r--config/coq_config.mli2
1 files changed, 2 insertions, 0 deletions
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