From aa77afa9d828d0bbb5d6fd5faf2e971b515a19fd Mon Sep 17 00:00:00 2001 From: glondu Date: Tue, 28 Oct 2008 18:43:16 +0000 Subject: 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 --- config/Makefile.template | 1 + config/coq_config.mli | 2 ++ 2 files changed, 3 insertions(+) (limited to 'config') 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 -- cgit v1.2.3