Imported Upstream version 8.0pl1upstream/8.0pl1

3 files changed, 144 insertions, 0 deletions

diff --git a/config/Makefile.template b/config/Makefile.template
new file mode 100644
index 00000000..cd49db89
--- /dev/null
+++ b/config/Makefile.template
@@ -0,0 +1,107 @@
+##################################
+#
+#  Configuration file for Coq
+# 
+##################################
+
+#############################################################################
+#
+#  This file is generated by the script "configure"
+#
+#  DO NOT EDIT IT !! DO NOT EDIT IT !! DO NOT EDIT IT !! DO NOT EDIT IT !! 
+#
+#  If something is wrong below, then rerun the script "configure"
+#  with the good options (see the file INSTALL).
+#
+#############################################################################
+
+# Local use (no installation)
+LOCAL=LOCALINSTALLATION
+
+# Paths for true installation
+# BINDIR=path where coqtop, coqc, coqmktop, coq-tex, coqdep, gallina and
+#        do_Makefile will reside
+# LIBDIR=path where the Coq library will reside
+# MANDIR=path where to install manual pages
+# EMACSDIR=path where to put Coq's Emacs mode (coq.el)
+BINDIR="BINDIRDIRECTORY"
+COQLIB="COQLIBDIRECTORY"
+MANDIR="MANDIRDIRECTORY"
+EMACSLIB="EMACSLIBDIRECTORY"
+EMACS=EMACSCOMMAND
+
+# Path to Coq distribution
+COQTOP=COQTOPDIRECTORY
+VERSION=COQVERSION
+
+# Directory containing Camlp4 binaries. Can be empty if camlp4 is in the PATH
+CAMLP4BIN=CAMLP4BINDIRECTORY
+
+# Ocaml version number
+CAMLVERSION=CAMLTAG
+
+# Camlp4 library directory (avoid CAMLP4LIB used on Windows)
+CAMLP4O=CAMLP4TOOL
+MYCAMLP4LIB=CAMLP4LIBDIRECTORY
+
+# Objective-Caml compile command 
+OCAMLC=BYTECAMLC
+OCAMLOPT=NATIVECAMLC
+
+# Caml link command and Caml make top command
+CAMLLINK=BYTECAMLC
+CAMLOPTLINK=NATIVECAMLC
+CAMLMKTOP=ocamlmktop
+
+# Compilation debug flag
+CAMLDEBUG=COQDEBUGFLAG
+
+# Compilation profile flag
+CAMLTIMEPROF=COQPROFILEFLAG
+
+# The best compiler: native (=opt) or bytecode (=byte) if no native compiler
+BEST=BESTCOMPILER
+
+# For Camlp4 use
+P4=$(COQTOP)/bin/$(ARCH)/call_camlp4 -I $(COQTOP)/src/parsing
+P4DEP=$(COQTOP)/bin/$(ARCH)/camlp4dep
+
+# Your architecture
+# Can be obtain by UNIX command arch
+ARCH=ARCHITECTURE
+
+# Supplementary libs for some systems, currently:
+#  . Sun Solaris: -cclib -lunix -cclib -lnsl -cclib -lsocket
+#  . others     : -cclib -lunix
+#  . windows	: -cclib -lunix
+
+OSDEPLIBS=OSDEPENDENTLIBS
+
+# executable files extension, currently:
+#  Unix systems:
+#  Win32 systems : .exe
+EXE=EXECUTEEXTENSION
+
+# the command MKDIR (try to replace it with mkdirhier if you have problems)
+MKDIR=mkdir -p
+
+# where to put the coqdoc.sty style file
+COQDOCDIR=COQDOCDIRECTORY
+
+# command to update TeX' kpathsea database
+#MKTEXLSR=MKTEXLSRCOMMAND
+
+#the command STRIP 
+# Unix systems and profiling: true
+# Unix systems and no profiling: strip
+# Win32 systems: true (actually strip is bogus)
+STRIP=STRIPCOMMAND
+
+# Options for reals (all/basic)
+REALS=REALSOPT
+
+# CoqIde (no/byte/opt)
+HASCOQIDE=COQIDEOPT
+
+# 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
new file mode 100644
index 00000000..1d88358a
--- /dev/null
+++ b/config/coq_config.mli
@@ -0,0 +1,36 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: coq_config.mli,v 1.9.16.1 2004/07/16 19:29:58 herbelin Exp $ i*)
+
+val local : bool        (* local use (no installation) *)
+
+val bindir : string     (* where the binaries are installed *)
+val coqlib : string     (* where the std library is installed *)
+
+val coqtop : string     (* where are the sources *)
+
+val camllib : string    (* for Dynlink *)
+
+val camlp4lib : string  (* where is the library of Camlp4 *)
+
+val best : string       (* byte/opt *)
+val arch : string       (* architecture *)
+val osdeplibs : string  (* OS dependant link options for ocamlc *)
+
+(* val defined : string list  (* options for lib/ocamlpp *) *)
+
+val version : string    (* version number of Coq *)
+val versionsi : string  (* version number of Coq\_SearchIsos *)
+val date : string       (* release date *)
+val compile_date : string (* compile date *)
+
+val theories_dirs : string list
+val contrib_dirs : string list
+
+val exec_extension : string (* "" under Unix, ".exe" under MS-windows *)
diff --git a/config/giveostype.ml b/config/giveostype.ml
new file mode 100644
index 00000000..e657bc79
--- /dev/null
+++ b/config/giveostype.ml
@@ -0,0 +1 @@
+print_string Sys.os_type;;