summaryrefslogtreecommitdiff
path: root/config
diff options
context:
space:
mode:
Diffstat (limited to 'config')
-rw-r--r--config/Makefile.template37
-rw-r--r--config/coq_config.mli3
2 files changed, 30 insertions, 10 deletions
diff --git a/config/Makefile.template b/config/Makefile.template
index aa7f2d62..3ea7c7c9 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -35,31 +35,41 @@ COQTOP=COQTOPDIRECTORY
VERSION=COQVERSION
# Directory containing Camlp4 binaries. Can be empty if camlp4 is in the PATH
-CAMLP4BIN=CAMLP4BINDIRECTORY
+CAMLP4BIN="CAMLP4BINDIRECTORY"
# Ocaml version number
CAMLVERSION=CAMLTAG
# Ocaml .h directory
-CAMLHLIB=CAMLLIBDIRECTORY/caml
+CAMLHLIB="CAMLLIBDIRECTORY"/caml
# Camlp4 library directory (avoid CAMLP4LIB used on Windows)
CAMLP4O=CAMLP4TOOL
CAMLP4COMPAT=CAMLP4COMPATFLAGS
-MYCAMLP4LIB=CAMLP4LIBDIRECTORY
+MYCAMLP4LIB="CAMLP4LIBDIRECTORY"
# Objective-Caml compile command
-OCAMLC=BYTECAMLC
-OCAMLOPT=NATIVECAMLC
+OCAMLC="BYTECAMLC"
+OCAMLOPT="NATIVECAMLC"
+OCAMLDEP="OCAMLDEPEXEC"
+OCAMLDOC="OCAMLDOCEXEC"
+OCAMLLEX="OCAMLLEXEXEC"
+OCAMLYACC="OCAMLYACCEXEC"
# Caml link command and Caml make top command
-CAMLLINK=BYTECAMLC
-CAMLOPTLINK=NATIVECAMLC
-CAMLMKTOP=ocamlmktop
+CAMLLINK="BYTECAMLC"
+CAMLOPTLINK="NATIVECAMLC"
+CAMLMKTOP="CAMLMKTOPEXEC"
+
+# Caml flags
+CAMLFLAGS=CAMLANNOTATEFLAG
# Compilation debug flag
CAMLDEBUG=COQDEBUGFLAG
+# Inlining flag (inlining causes problems with ocaml < 3.09.x)
+INLINEFLAG=COQINLINEFLAG
+
# User compilation flag
USERFLAGS=
@@ -77,6 +87,11 @@ P4DEP=$(COQTOP)/bin/$(ARCH)/camlp4dep
# Can be obtain by UNIX command arch
ARCH=ARCHITECTURE
+# Your C compiler and co
+CC="CCEXEC"
+AR="AREXEC"
+RANLIB="RANLIBEXEC"
+
# Supplementary libs for some systems, currently:
# . Sun Solaris: -cclib -lunix -cclib -lnsl -cclib -lsocket
# . others : -cclib -lunix
@@ -93,7 +108,7 @@ EXE=EXECUTEEXTENSION
MKDIR=mkdir -p
# where to put the coqdoc.sty style file
-COQDOCDIR=COQDOCDIRECTORY
+COQDOCDIR="COQDOCDIRECTORY"
# command to update TeX' kpathsea database
#MKTEXLSR=MKTEXLSRCOMMAND
@@ -113,5 +128,9 @@ REALS=REALSOPT
# CoqIde (no/byte/opt)
HASCOQIDE=COQIDEOPT
+# Defining REVISION
+CHECKEDOUT=CHECKEDOUTSOURCETREE
+
# make or sed are bogus and believe lines not terminating by a return
# are inexistent
+
diff --git a/config/coq_config.mli b/config/coq_config.mli
index 29ee7f9d..c214344e 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: coq_config.mli 8932 2006-06-09 09:29:03Z notin $ i*)
+(*i $Id: coq_config.mli 9115 2006-09-01 13:47:00Z notin $ i*)
val local : bool (* local use (no installation) *)
@@ -15,6 +15,7 @@ val coqlib : string (* where the std library is installed *)
val coqtop : string (* where are the sources *)
+val camldir : string (* base directory of OCaml binaries *)
val camllib : string (* for Dynlink *)
val camlp4lib : string (* where is the library of Camlp4 *)