Imported Upstream version 8.1~gammaupstream/8.1.gamma

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 *)