config avec autoconf

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8146 85f007b7-540e-0410-9357-904b9bb8a0f7

11 files changed, 1001 insertions, 40 deletions

diff --git a/doc/.cvsignore b/doc/.cvsignore
index 261566e347..4174e5c73c 100644
--- a/doc/.cvsignore
+++ b/doc/.cvsignore
@@ -24,3 +24,5 @@ auto
 all-ps-docs.tar
 doc-html.tar.gz
 all-ps-docs.tar.gz
+config.cache
+config.status
diff --git a/doc/Makefile b/doc/Makefile.in
index 611e38d3e2..a9712fb797 100644
--- a/doc/Makefile
+++ b/doc/Makefile.in
@@ -7,19 +7,17 @@
 #   - htmlSplit: http://coq.inria.fr/~delahaye
 # Rapports INRIA: dviselect, rrkit (par Michel Mauny)
 
-include ../config
+DOCCOQTOP=@COQTOPBYTE@
+DOCCOQC=@COQC@
+COQLIB=@COQLIB@
+COQTEX=@COQTEX@ -image $(DOCCOQTOP) -v -sl -small
 
 LATEX=latex
 BIBTEX=bibtex
 MAKEINDEX=makeindex
 PDFLATEX=pdflatex
-DOCCOQTOP="../bin/$(ARCH)/coqtop -full -bindir ../bin/$(ARCH)/ -libdir ../"
-DOCCOQC=../bin/$(ARCH)/coqc -full -bindir ../bin/$(ARCH)/ -libdir ../
-COQTEX=../bin/$(ARCH)/coq-tex -image $(DOCCOQTOP) -v -sl -small
-TEXINPUTS=$(COQTOP)/tools/coq-tex:/usr/local/lib/rrkit/RRINPUTSDIR:.:
-ZLIBS=-I ../src/lib/util -I ../src/parsing -I ../src/meta -I ../src/constr \
-      -I ../src/typing -I ../src/proofs -I ../src/env -I ../src/tactics \
-      -I ../tactics
+
+TEXINPUTS=/usr/local/lib/rrkit/RRINPUTSDIR:.:
 
 INPUTS=./macros.tex ./title.tex ./headers.tex ./Reference-Manual.tex
 
@@ -29,7 +27,7 @@ LIBFILES=library/Logic.tex library/Datatypes.tex library/Peano.tex \
 REFMANCOQTEXFILES=\
   RefMan-gal.v.tex RefMan-ext.v.tex RefMan-tac.v.tex \
   RefMan-cic.v.tex RefMan-lib.v.tex RefMan-tacex.v.tex \
-  RefMan-syn.v.tex RefMan-ppr.v.tex RefMan-tus.v.tex
+  RefMan-syn.v.tex RefMan-tus.v.tex
 
 COQTEXFILES= Cases.v.tex Coercion.v.tex Extraction.v.tex Program.v.tex\
   Omega.v.tex Natural.v.tex Changes.v.tex Tutorial.v.tex Polynom.v.tex \
@@ -61,7 +59,7 @@ FTPHTMLDOCS=doc-html.tar.gz
 # Principal targets 
 ########################
 
-all: demos-programs all-dvi all-pdf
+all: all-dvi all-pdf
 
 coq-part: $(REFMANCOQTEXFILES) $(COQTEXFILES) demos-programs library/libdoc.tex
 
@@ -188,22 +186,24 @@ cleanall: clean clean-html
 ##########################
 
 Library.dvi: $(INPUTS) library/libdoc.tex Library.tex
+	echo "======Library.dvi: A FAIRE========"
 Library.pdf: $(INPUTS) library/libdoc.tex Library.tex
+	echo "======Library.pdf: A FAIRE========"
 
 library/libdoc.tex: 
-	(cd ../theories ; make doc)
+#	(cd ../theories ; make doc)
 
 demos-programs:
-	(cd ../theories/DEMOS/PROGRAMS ; make all)
+#	(cd ../theories/DEMOS/PROGRAMS ; make all)
 
 Recursive-Definition.v.tex: ./title.tex Recursive-Definition.tex
 
 Tutorial.v.dvi: ./title.tex Tutorial.tex
 Tutorial.v.pdf: ./title.tex Tutorial.tex
 
-RefMan-ppr.v.tex: ../tactics/eqdecide.cmo
+# RefMan-ppr.v.tex: ../tactics/eqdecide.cmo
 
-RefMan-tus.v.tex: ../tactics/EqDecide.vo ../tactics/eqdecide.cmo
+# RefMan-tus.v.tex: ../tactics/EqDecide.vo ../tactics/eqdecide.cmo
 
 Reference-Manual.ps: Reference-Manual.dvi
 
diff --git a/doc/RefMan-com.tex b/doc/RefMan-com.tex
index 88cf650a10..47a6e8a5ea 100755
--- a/doc/RefMan-com.tex
+++ b/doc/RefMan-com.tex
@@ -67,7 +67,7 @@ an efficient version of the system.
 \index{Resource file}
 
 When \Coq\ is launched, with either {\tt coqtop} or {\tt coqc}, the
-resource file \verb:$HOME/.coqrc.6.2.4: is loaded, where \verb:$HOME: is
+resource file \verb:$HOME/.coqrc.7.0: is loaded, where \verb:$HOME: is
 the home directory of the user.  If this file is not found, then the
 file \verb:$HOME/.coqrc: is searched. You can also specify an
 arbitrary name for the resource file (see option \verb:-init-file:
@@ -168,14 +168,14 @@ coqtop}).
   {\em state.coq}.
 
 \item[{\tt -init-file} {\em file}]\ \\
-  Take {\em file} as resource file, instead of {\tt \$HOME/.coqrc.6.2.4}.
+  Take {\em file} as resource file, instead of {\tt \$HOME/.coqrc.7.0}.
 
 \item[{\tt -q}]\ \\
   Cause \Coq~not to load the resource file.
 
 \item[{\tt -user} {\em username}]\ \\
   Take resource file of user {\em username} (that is 
-  \verb+~+{\em username}{\tt /.coqrc.6.2.4}) instead of yours.
+  \verb+~+{\em username}{\tt /.coqrc.7.0}) instead of yours.
 
 \item[{\tt -load-ml-source} {\em file}]\ \\
   Load the Caml source file {\em file}.
diff --git a/doc/RefMan-cover.tex b/doc/RefMan-cover.tex
index d5a832eed7..2fdde93574 100644
--- a/doc/RefMan-cover.tex
+++ b/doc/RefMan-cover.tex
@@ -2,8 +2,8 @@
         % L'utilisation du style `french' force le résumé français à
         % apparaître en premier.
 
-\RRtitle{Manuel de r\'ef\'erence du syst\`eme Coq \\ version V6.3}
-\RRetitle{The Coq Proof Assistant \\ Reference Manual \\ Version 6.3
+\RRtitle{Manuel de r\'ef\'erence du syst\`eme Coq \\ version V7.0}
+\RRetitle{The Coq Proof Assistant \\ Reference Manual \\ Version 7.0
 \thanks
 {This research was partly supported by ESPRIT Basic Research
 Action ``Types'' and by the GDR ``Programmation'' co-financed by MRE-PRC and CNRS.}
@@ -14,7 +14,7 @@ Hugo Herbelin, G\'erard Huet, C\'esar Mu\~noz, Chetan Murthy,
 Catherine Parent, Christine Paulin-Mohring,
 Amokrane Sa{\"\i}bi, Benjamin Werner}
 \authorhead{}
-\titlehead{Coq V6.2 Reference Manual}
+\titlehead{Coq V7.0 Reference Manual}
 \RRtheme{2}
 \RRprojet{Coq}
 \RRNo{0123456789}
@@ -25,10 +25,9 @@ Amokrane Sa{\"\i}bi, Benjamin Werner}
 \RRresume{Coq est un syst\`eme permettant le d\'eveloppement et la
 v\'erification de preuves formelles dans une logique d'ordre
 sup\'erieure incluant un riche langage de d\'efinitions de fonctions.
-Ce document constitue le manuel de r\'ef\'erence de la version V6.1
-qui est distribu\'ee par ftp anonyme aux adresses
-ftp.inria.fr:/INRIA/Projects/coq/V6.1 et
-ftp.ens-lyon.fr:/pub/LIP/COQ/V6.1}
+Ce document constitue le manuel de r\'ef\'erence de la version V7.0
+qui est distribu\'ee par ftp anonyme à l'adresse
+\url{ftp://ftp.inria.fr/INRIA/coq/}}
 
 \RRmotcle{Coq, Syst\`eme d'aide \`a la preuve, Preuves formelles,
 Calcul des Constructions Inductives}
@@ -36,9 +35,8 @@ Calcul des Constructions Inductives}
 
 \RRabstract{Coq is a proof assistant based on a higher-order logic
 allowing powerful definitions of functions. 
-Coq V6.1 is available by anonymous
-ftp at ftp.inria.fr:/INRIA/Projects/coq/V6.1 and
-ftp.ens-lyon.fr:/pub/LIP/COQ/V6.1}
+Coq V7.0 is available by anonymous
+ftp at \url{ftp://ftp.inria.fr/INRIA/coq/}}
 
 \RRkeyword{Coq, Proof Assistant, Formal Proofs, Calculus of Inductives
 Constructions}
diff --git a/doc/RefMan-int.tex b/doc/RefMan-int.tex
index d874f7cdb9..83a7a90777 100755
--- a/doc/RefMan-int.tex
+++ b/doc/RefMan-int.tex
@@ -1,7 +1,7 @@
 \setheaders{Introduction}
 \chapter*{Introduction}
 
-This document is the Reference Manual of version V6.2.4 of the \Coq\ 
+This document is the Reference Manual of version V7.0 of the \Coq\ 
 proof assistant. A companion volume, the \Coq\ Tutorial, is provided
 for the beginners. It is advised to read the Tutorial first.
 
diff --git a/doc/Tutorial-cover.tex b/doc/Tutorial-cover.tex
index 832739c3ea..1acd7d084a 100644
--- a/doc/Tutorial-cover.tex
+++ b/doc/Tutorial-cover.tex
@@ -2,11 +2,11 @@
         % L'utilisation du style `french' force le résumé français à
         % apparaître en premier.
 \RRetitle{
-The Coq Proof Assistant \\ A Tutorial \\ Version 6.1
+The Coq Proof Assistant \\ A Tutorial \\ Version 7.0
 \thanks{This research was partly supported by ESPRIT Basic Research
 Action ``Types'' and by the GDR ``Programmation'' co-financed by MRE-PRC and CNRS.}
 }
-\RRtitle{Coq \\ Une introduction \\ V6.1 }
+\RRtitle{Coq \\ Une introduction \\ V7.0 }
 \RRauthor{G\'erard Huet, Gilles Kahn and Christine Paulin-Mohring}
 \RRtheme{2}
 \RRprojet{{Coq
@@ -29,18 +29,16 @@ Action ``Types'' and by the GDR ``Programmation'' co-financed by MRE-PRC and CNR
 v\'erification de preuves formelles dans une logique d'ordre
 sup\'erieure incluant un riche langage de d\'efinitions de fonctions.
 Ce document constitue une introduction pratique \`a l'utilisation de
-la version V6.1 qui est distribu\'ee par ftp anonyme aux adresses
-ftp.inria.fr:/INRIA/Projects/coq/V6.1 et
-ftp.ens-lyon.fr:/pub/LIP/COQ/V6.1}
+la version V7.0 qui est distribu\'ee par ftp anonyme à l'adresse
+\url{ftp://ftp.inria.fr/INRIA/coq/}}
 
 \RRmotcle{Coq, Syst\`eme d'aide \`a la preuve, Preuves formelles, Calcul
 des Constructions Inductives}
 
 \RRabstract{Coq is a proof assistant based on a higher-order logic
 allowing powerful definitions of functions. This document is a
-tutorial for the version V6.1 of Coq. This version is available by
-anonymous ftp at ftp.inria.fr:/INRIA/Projects/coq/V6.1 and
-ftp.ens-lyon.fr:/pub/LIP/COQ/V6.1}
+tutorial for the version V7.0 of Coq. This version is available by
+anonymous ftp at \url{ftp://ftp.inria.fr/INRIA/coq/}}
 
 \RRkeyword{Coq, Proof Assistant, Formal Proofs, Calculus of Inductives
 Constructions}
diff --git a/doc/Tutorial.tex b/doc/Tutorial.tex
index a2459384cf..d554675f1b 100755
--- a/doc/Tutorial.tex
+++ b/doc/Tutorial.tex
@@ -32,7 +32,7 @@ he does not use any special interface such as Emacs or Centaur.
 Instructions on installation procedures, as well as more comprehensive
 documentation, may be found in the standard distribution of \Coq,
 which may be obtained by anonymous FTP from site \verb:ftp.inria.fr:,
-directory \verb:INRIA/coq/V6.3.1:. 
+directory \verb:INRIA/coq/V7.0:. 
 
 In the following, all examples preceded by the prompting sequence
 \verb:Coq < : represent user input, terminated by a period. The
@@ -46,7 +46,7 @@ The standard invocation of \Coq\ delivers a message such as:
 \begin{flushleft}
 \begin{verbatim}
 unix: coqtop
-Welcome to Coq V6.3.1 (December 1999)
+Welcome to Coq 7.0 (November 2000)
 
 Coq <
 \end{verbatim}
diff --git a/doc/configure b/doc/configure
new file mode 100755
index 0000000000..47d270725c
--- /dev/null
+++ b/doc/configure
@@ -0,0 +1,909 @@
+#! /bin/sh
+
+# Guess values for system-dependent variables and create Makefiles.
+# Generated automatically using autoconf version 2.13 
+# Copyright (C) 1992, 93, 94, 95, 96 Free Software Foundation, Inc.
+#
+# This configure script is free software; the Free Software Foundation
+# gives unlimited permission to copy, distribute and modify it.
+
+# Defaults:
+ac_help=
+ac_default_prefix=/usr/local
+# Any additions from configure.in:
+
+# Initialize some variables set by options.
+# The variables have the same names as the options, with
+# dashes changed to underlines.
+build=NONE
+cache_file=./config.cache
+exec_prefix=NONE
+host=NONE
+no_create=
+nonopt=NONE
+no_recursion=
+prefix=NONE
+program_prefix=NONE
+program_suffix=NONE
+program_transform_name=s,x,x,
+silent=
+site=
+srcdir=
+target=NONE
+verbose=
+x_includes=NONE
+x_libraries=NONE
+bindir='${exec_prefix}/bin'
+sbindir='${exec_prefix}/sbin'
+libexecdir='${exec_prefix}/libexec'
+datadir='${prefix}/share'
+sysconfdir='${prefix}/etc'
+sharedstatedir='${prefix}/com'
+localstatedir='${prefix}/var'
+libdir='${exec_prefix}/lib'
+includedir='${prefix}/include'
+oldincludedir='/usr/include'
+infodir='${prefix}/info'
+mandir='${prefix}/man'
+
+# Initialize some other variables.
+subdirs=
+MFLAGS= MAKEFLAGS=
+SHELL=${CONFIG_SHELL-/bin/sh}
+# Maximum number of lines to put in a shell here document.
+ac_max_here_lines=12
+
+ac_prev=
+for ac_option
+do
+
+  # If the previous option needs an argument, assign it.
+  if test -n "$ac_prev"; then
+    eval "$ac_prev=\$ac_option"
+    ac_prev=
+    continue
+  fi
+
+  case "$ac_option" in
+  -*=*) ac_optarg=`echo "$ac_option" | sed 's/[-_a-zA-Z0-9]*=//'` ;;
+  *) ac_optarg= ;;
+  esac
+
+  # Accept the important Cygnus configure options, so we can diagnose typos.
+
+  case "$ac_option" in
+
+  -bindir | --bindir | --bindi | --bind | --bin | --bi)
+    ac_prev=bindir ;;
+  -bindir=* | --bindir=* | --bindi=* | --bind=* | --bin=* | --bi=*)
+    bindir="$ac_optarg" ;;
+
+  -build | --build | --buil | --bui | --bu)
+    ac_prev=build ;;
+  -build=* | --build=* | --buil=* | --bui=* | --bu=*)
+    build="$ac_optarg" ;;
+
+  -cache-file | --cache-file | --cache-fil | --cache-fi \
+  | --cache-f | --cache- | --cache | --cach | --cac | --ca | --c)
+    ac_prev=cache_file ;;
+  -cache-file=* | --cache-file=* | --cache-fil=* | --cache-fi=* \
+  | --cache-f=* | --cache-=* | --cache=* | --cach=* | --cac=* | --ca=* | --c=*)
+    cache_file="$ac_optarg" ;;
+
+  -datadir | --datadir | --datadi | --datad | --data | --dat | --da)
+    ac_prev=datadir ;;
+  -datadir=* | --datadir=* | --datadi=* | --datad=* | --data=* | --dat=* \
+  | --da=*)
+    datadir="$ac_optarg" ;;
+
+  -disable-* | --disable-*)
+    ac_feature=`echo $ac_option|sed -e 's/-*disable-//'`
+    # Reject names that are not valid shell variable names.
+    if test -n "`echo $ac_feature| sed 's/[-a-zA-Z0-9_]//g'`"; then
+      { echo "configure: error: $ac_feature: invalid feature name" 1>&2; exit 1; }
+    fi
+    ac_feature=`echo $ac_feature| sed 's/-/_/g'`
+    eval "enable_${ac_feature}=no" ;;
+
+  -enable-* | --enable-*)
+    ac_feature=`echo $ac_option|sed -e 's/-*enable-//' -e 's/=.*//'`
+    # Reject names that are not valid shell variable names.
+    if test -n "`echo $ac_feature| sed 's/[-_a-zA-Z0-9]//g'`"; then
+      { echo "configure: error: $ac_feature: invalid feature name" 1>&2; exit 1; }
+    fi
+    ac_feature=`echo $ac_feature| sed 's/-/_/g'`
+    case "$ac_option" in
+      *=*) ;;
+      *) ac_optarg=yes ;;
+    esac
+    eval "enable_${ac_feature}='$ac_optarg'" ;;
+
+  -exec-prefix | --exec_prefix | --exec-prefix | --exec-prefi \
+  | --exec-pref | --exec-pre | --exec-pr | --exec-p | --exec- \
+  | --exec | --exe | --ex)
+    ac_prev=exec_prefix ;;
+  -exec-prefix=* | --exec_prefix=* | --exec-prefix=* | --exec-prefi=* \
+  | --exec-pref=* | --exec-pre=* | --exec-pr=* | --exec-p=* | --exec-=* \
+  | --exec=* | --exe=* | --ex=*)
+    exec_prefix="$ac_optarg" ;;
+
+  -gas | --gas | --ga | --g)
+    # Obsolete; use --with-gas.
+    with_gas=yes ;;
+
+  -help | --help | --hel | --he)
+    # Omit some internal or obsolete options to make the list less imposing.
+    # This message is too long to be a string in the A/UX 3.1 sh.
+    cat << EOF
+Usage: configure [options] [host]
+Options: [defaults in brackets after descriptions]
+Configuration:
+  --cache-file=FILE       cache test results in FILE
+  --help                  print this message
+  --no-create             do not create output files
+  --quiet, --silent       do not print \`checking...' messages
+  --version               print the version of autoconf that created configure
+Directory and file names:
+  --prefix=PREFIX         install architecture-independent files in PREFIX
+                          [$ac_default_prefix]
+  --exec-prefix=EPREFIX   install architecture-dependent files in EPREFIX
+                          [same as prefix]
+  --bindir=DIR            user executables in DIR [EPREFIX/bin]
+  --sbindir=DIR           system admin executables in DIR [EPREFIX/sbin]
+  --libexecdir=DIR        program executables in DIR [EPREFIX/libexec]
+  --datadir=DIR           read-only architecture-independent data in DIR
+                          [PREFIX/share]
+  --sysconfdir=DIR        read-only single-machine data in DIR [PREFIX/etc]
+  --sharedstatedir=DIR    modifiable architecture-independent data in DIR
+                          [PREFIX/com]
+  --localstatedir=DIR     modifiable single-machine data in DIR [PREFIX/var]
+  --libdir=DIR            object code libraries in DIR [EPREFIX/lib]
+  --includedir=DIR        C header files in DIR [PREFIX/include]
+  --oldincludedir=DIR     C header files for non-gcc in DIR [/usr/include]
+  --infodir=DIR           info documentation in DIR [PREFIX/info]
+  --mandir=DIR            man documentation in DIR [PREFIX/man]
+  --srcdir=DIR            find the sources in DIR [configure dir or ..]
+  --program-prefix=PREFIX prepend PREFIX to installed program names
+  --program-suffix=SUFFIX append SUFFIX to installed program names
+  --program-transform-name=PROGRAM
+                          run sed PROGRAM on installed program names
+EOF
+    cat << EOF
+Host type:
+  --build=BUILD           configure for building on BUILD [BUILD=HOST]
+  --host=HOST             configure for HOST [guessed]
+  --target=TARGET         configure for TARGET [TARGET=HOST]
+Features and packages:
+  --disable-FEATURE       do not include FEATURE (same as --enable-FEATURE=no)
+  --enable-FEATURE[=ARG]  include FEATURE [ARG=yes]
+  --with-PACKAGE[=ARG]    use PACKAGE [ARG=yes]
+  --without-PACKAGE       do not use PACKAGE (same as --with-PACKAGE=no)
+  --x-includes=DIR        X include files are in DIR
+  --x-libraries=DIR       X library files are in DIR
+EOF
+    if test -n "$ac_help"; then
+      echo "--enable and --with options recognized:$ac_help"
+    fi
+    exit 0 ;;
+
+  -host | --host | --hos | --ho)
+    ac_prev=host ;;
+  -host=* | --host=* | --hos=* | --ho=*)
+    host="$ac_optarg" ;;
+
+  -includedir | --includedir | --includedi | --included | --include \
+  | --includ | --inclu | --incl | --inc)
+    ac_prev=includedir ;;
+  -includedir=* | --includedir=* | --includedi=* | --included=* | --include=* \
+  | --includ=* | --inclu=* | --incl=* | --inc=*)
+    includedir="$ac_optarg" ;;
+
+  -infodir | --infodir | --infodi | --infod | --info | --inf)
+    ac_prev=infodir ;;
+  -infodir=* | --infodir=* | --infodi=* | --infod=* | --info=* | --inf=*)
+    infodir="$ac_optarg" ;;
+
+  -libdir | --libdir | --libdi | --libd)
+    ac_prev=libdir ;;
+  -libdir=* | --libdir=* | --libdi=* | --libd=*)
+    libdir="$ac_optarg" ;;
+
+  -libexecdir | --libexecdir | --libexecdi | --libexecd | --libexec \
+  | --libexe | --libex | --libe)
+    ac_prev=libexecdir ;;
+  -libexecdir=* | --libexecdir=* | --libexecdi=* | --libexecd=* | --libexec=* \
+  | --libexe=* | --libex=* | --libe=*)
+    libexecdir="$ac_optarg" ;;
+
+  -localstatedir | --localstatedir | --localstatedi | --localstated \
+  | --localstate | --localstat | --localsta | --localst \
+  | --locals | --local | --loca | --loc | --lo)
+    ac_prev=localstatedir ;;
+  -localstatedir=* | --localstatedir=* | --localstatedi=* | --localstated=* \
+  | --localstate=* | --localstat=* | --localsta=* | --localst=* \
+  | --locals=* | --local=* | --loca=* | --loc=* | --lo=*)
+    localstatedir="$ac_optarg" ;;
+
+  -mandir | --mandir | --mandi | --mand | --man | --ma | --m)
+    ac_prev=mandir ;;
+  -mandir=* | --mandir=* | --mandi=* | --mand=* | --man=* | --ma=* | --m=*)
+    mandir="$ac_optarg" ;;
+
+  -nfp | --nfp | --nf)
+    # Obsolete; use --without-fp.
+    with_fp=no ;;
+
+  -no-create | --no-create | --no-creat | --no-crea | --no-cre \
+  | --no-cr | --no-c)
+    no_create=yes ;;
+
+  -no-recursion | --no-recursion | --no-recursio | --no-recursi \
+  | --no-recurs | --no-recur | --no-recu | --no-rec | --no-re | --no-r)
+    no_recursion=yes ;;
+
+  -oldincludedir | --oldincludedir | --oldincludedi | --oldincluded \
+  | --oldinclude | --oldinclud | --oldinclu | --oldincl | --oldinc \
+  | --oldin | --oldi | --old | --ol | --o)
+    ac_prev=oldincludedir ;;
+  -oldincludedir=* | --oldincludedir=* | --oldincludedi=* | --oldincluded=* \
+  | --oldinclude=* | --oldinclud=* | --oldinclu=* | --oldincl=* | --oldinc=* \
+  | --oldin=* | --oldi=* | --old=* | --ol=* | --o=*)
+    oldincludedir="$ac_optarg" ;;
+
+  -prefix | --prefix | --prefi | --pref | --pre | --pr | --p)
+    ac_prev=prefix ;;
+  -prefix=* | --prefix=* | --prefi=* | --pref=* | --pre=* | --pr=* | --p=*)
+    prefix="$ac_optarg" ;;
+
+  -program-prefix | --program-prefix | --program-prefi | --program-pref \
+  | --program-pre | --program-pr | --program-p)
+    ac_prev=program_prefix ;;
+  -program-prefix=* | --program-prefix=* | --program-prefi=* \
+  | --program-pref=* | --program-pre=* | --program-pr=* | --program-p=*)
+    program_prefix="$ac_optarg" ;;
+
+  -program-suffix | --program-suffix | --program-suffi | --program-suff \
+  | --program-suf | --program-su | --program-s)
+    ac_prev=program_suffix ;;
+  -program-suffix=* | --program-suffix=* | --program-suffi=* \
+  | --program-suff=* | --program-suf=* | --program-su=* | --program-s=*)
+    program_suffix="$ac_optarg" ;;
+
+  -program-transform-name | --program-transform-name \
+  | --program-transform-nam | --program-transform-na \
+  | --program-transform-n | --program-transform- \
+  | --program-transform | --program-transfor \
+  | --program-transfo | --program-transf \
+  | --program-trans | --program-tran \
+  | --progr-tra | --program-tr | --program-t)
+    ac_prev=program_transform_name ;;
+  -program-transform-name=* | --program-transform-name=* \
+  | --program-transform-nam=* | --program-transform-na=* \
+  | --program-transform-n=* | --program-transform-=* \
+  | --program-transform=* | --program-transfor=* \
+  | --program-transfo=* | --program-transf=* \
+  | --program-trans=* | --program-tran=* \
+  | --progr-tra=* | --program-tr=* | --program-t=*)
+    program_transform_name="$ac_optarg" ;;
+
+  -q | -quiet | --quiet | --quie | --qui | --qu | --q \
+  | -silent | --silent | --silen | --sile | --sil)
+    silent=yes ;;
+
+  -sbindir | --sbindir | --sbindi | --sbind | --sbin | --sbi | --sb)
+    ac_prev=sbindir ;;
+  -sbindir=* | --sbindir=* | --sbindi=* | --sbind=* | --sbin=* \
+  | --sbi=* | --sb=*)
+    sbindir="$ac_optarg" ;;
+
+  -sharedstatedir | --sharedstatedir | --sharedstatedi \
+  | --sharedstated | --sharedstate | --sharedstat | --sharedsta \
+  | --sharedst | --shareds | --shared | --share | --shar \
+  | --sha | --sh)
+    ac_prev=sharedstatedir ;;
+  -sharedstatedir=* | --sharedstatedir=* | --sharedstatedi=* \
+  | --sharedstated=* | --sharedstate=* | --sharedstat=* | --sharedsta=* \
+  | --sharedst=* | --shareds=* | --shared=* | --share=* | --shar=* \
+  | --sha=* | --sh=*)
+    sharedstatedir="$ac_optarg" ;;
+
+  -site | --site | --sit)
+    ac_prev=site ;;
+  -site=* | --site=* | --sit=*)
+    site="$ac_optarg" ;;
+
+  -srcdir | --srcdir | --srcdi | --srcd | --src | --sr)
+    ac_prev=srcdir ;;
+  -srcdir=* | --srcdir=* | --srcdi=* | --srcd=* | --src=* | --sr=*)
+    srcdir="$ac_optarg" ;;
+
+  -sysconfdir | --sysconfdir | --sysconfdi | --sysconfd | --sysconf \
+  | --syscon | --sysco | --sysc | --sys | --sy)
+    ac_prev=sysconfdir ;;
+  -sysconfdir=* | --sysconfdir=* | --sysconfdi=* | --sysconfd=* | --sysconf=* \
+  | --syscon=* | --sysco=* | --sysc=* | --sys=* | --sy=*)
+    sysconfdir="$ac_optarg" ;;
+
+  -target | --target | --targe | --targ | --tar | --ta | --t)
+    ac_prev=target ;;
+  -target=* | --target=* | --targe=* | --targ=* | --tar=* | --ta=* | --t=*)
+    target="$ac_optarg" ;;
+
+  -v | -verbose | --verbose | --verbos | --verbo | --verb)
+    verbose=yes ;;
+
+  -version | --version | --versio | --versi | --vers)
+    echo "configure generated by autoconf version 2.13"
+    exit 0 ;;
+
+  -with-* | --with-*)
+    ac_package=`echo $ac_option|sed -e 's/-*with-//' -e 's/=.*//'`
+    # Reject names that are not valid shell variable names.
+    if test -n "`echo $ac_package| sed 's/[-_a-zA-Z0-9]//g'`"; then
+      { echo "configure: error: $ac_package: invalid package name" 1>&2; exit 1; }
+    fi
+    ac_package=`echo $ac_package| sed 's/-/_/g'`
+    case "$ac_option" in
+      *=*) ;;
+      *) ac_optarg=yes ;;
+    esac
+    eval "with_${ac_package}='$ac_optarg'" ;;
+
+  -without-* | --without-*)
+    ac_package=`echo $ac_option|sed -e 's/-*without-//'`
+    # Reject names that are not valid shell variable names.
+    if test -n "`echo $ac_package| sed 's/[-a-zA-Z0-9_]//g'`"; then
+      { echo "configure: error: $ac_package: invalid package name" 1>&2; exit 1; }
+    fi
+    ac_package=`echo $ac_package| sed 's/-/_/g'`
+    eval "with_${ac_package}=no" ;;
+
+  --x)
+    # Obsolete; use --with-x.
+    with_x=yes ;;
+
+  -x-includes | --x-includes | --x-include | --x-includ | --x-inclu \
+  | --x-incl | --x-inc | --x-in | --x-i)
+    ac_prev=x_includes ;;
+  -x-includes=* | --x-includes=* | --x-include=* | --x-includ=* | --x-inclu=* \
+  | --x-incl=* | --x-inc=* | --x-in=* | --x-i=*)
+    x_includes="$ac_optarg" ;;
+
+  -x-libraries | --x-libraries | --x-librarie | --x-librari \
+  | --x-librar | --x-libra | --x-libr | --x-lib | --x-li | --x-l)
+    ac_prev=x_libraries ;;
+  -x-libraries=* | --x-libraries=* | --x-librarie=* | --x-librari=* \
+  | --x-librar=* | --x-libra=* | --x-libr=* | --x-lib=* | --x-li=* | --x-l=*)
+    x_libraries="$ac_optarg" ;;
+
+  -*) { echo "configure: error: $ac_option: invalid option; use --help to show usage" 1>&2; exit 1; }
+    ;;
+
+  *)
+    if test -n "`echo $ac_option| sed 's/[-a-z0-9.]//g'`"; then
+      echo "configure: warning: $ac_option: invalid host type" 1>&2
+    fi
+    if test "x$nonopt" != xNONE; then
+      { echo "configure: error: can only configure for one host and one target at a time" 1>&2; exit 1; }
+    fi
+    nonopt="$ac_option"
+    ;;
+
+  esac
+done
+
+if test -n "$ac_prev"; then
+  { echo "configure: error: missing argument to --`echo $ac_prev | sed 's/_/-/g'`" 1>&2; exit 1; }
+fi
+
+trap 'rm -fr conftest* confdefs* core core.* *.core $ac_clean_files; exit 1' 1 2 15
+
+# File descriptor usage:
+# 0 standard input
+# 1 file creation
+# 2 errors and warnings
+# 3 some systems may open it to /dev/tty
+# 4 used on the Kubota Titan
+# 6 checking for... messages and results
+# 5 compiler messages saved in config.log
+if test "$silent" = yes; then
+  exec 6>/dev/null
+else
+  exec 6>&1
+fi
+exec 5>./config.log
+
+echo "\
+This file contains any messages produced by compilers while
+running configure, to aid debugging if configure makes a mistake.
+" 1>&5
+
+# Strip out --no-create and --no-recursion so they do not pile up.
+# Also quote any args containing shell metacharacters.
+ac_configure_args=
+for ac_arg
+do
+  case "$ac_arg" in
+  -no-create | --no-create | --no-creat | --no-crea | --no-cre \
+  | --no-cr | --no-c) ;;
+  -no-recursion | --no-recursion | --no-recursio | --no-recursi \
+  | --no-recurs | --no-recur | --no-recu | --no-rec | --no-re | --no-r) ;;
+  *" "*|*"	"*|*[\[\]\~\#\$\^\&\*\(\)\{\}\\\|\;\<\>\?]*)
+  ac_configure_args="$ac_configure_args '$ac_arg'" ;;
+  *) ac_configure_args="$ac_configure_args $ac_arg" ;;
+  esac
+done
+
+# NLS nuisances.
+# Only set these to C if already set.  These must not be set unconditionally
+# because not all systems understand e.g. LANG=C (notably SCO).
+# Fixing LC_MESSAGES prevents Solaris sh from translating var values in `set'!
+# Non-C LC_CTYPE values break the ctype check.
+if test "${LANG+set}"   = set; then LANG=C;   export LANG;   fi
+if test "${LC_ALL+set}" = set; then LC_ALL=C; export LC_ALL; fi
+if test "${LC_MESSAGES+set}" = set; then LC_MESSAGES=C; export LC_MESSAGES; fi
+if test "${LC_CTYPE+set}"    = set; then LC_CTYPE=C;    export LC_CTYPE;    fi
+
+# confdefs.h avoids OS command line length limits that DEFS can exceed.
+rm -rf conftest* confdefs.h
+# AIX cpp loses on an empty file, so make sure it contains at least a newline.
+echo > confdefs.h
+
+# A filename unique to this package, relative to the directory that
+# configure is in, which we can look for to find out if srcdir is correct.
+ac_unique_file=Reference-Manual.tex
+
+# Find the source files, if location was not specified.
+if test -z "$srcdir"; then
+  ac_srcdir_defaulted=yes
+  # Try the directory containing this script, then its parent.
+  ac_prog=$0
+  ac_confdir=`echo $ac_prog|sed 's%/[^/][^/]*$%%'`
+  test "x$ac_confdir" = "x$ac_prog" && ac_confdir=.
+  srcdir=$ac_confdir
+  if test ! -r $srcdir/$ac_unique_file; then
+    srcdir=..
+  fi
+else
+  ac_srcdir_defaulted=no
+fi
+if test ! -r $srcdir/$ac_unique_file; then
+  if test "$ac_srcdir_defaulted" = yes; then
+    { echo "configure: error: can not find sources in $ac_confdir or .." 1>&2; exit 1; }
+  else
+    { echo "configure: error: can not find sources in $srcdir" 1>&2; exit 1; }
+  fi
+fi
+srcdir=`echo "${srcdir}" | sed 's%\([^/]\)/*$%\1%'`
+
+# Prefer explicitly selected file to automatically selected ones.
+if test -z "$CONFIG_SITE"; then
+  if test "x$prefix" != xNONE; then
+    CONFIG_SITE="$prefix/share/config.site $prefix/etc/config.site"
+  else
+    CONFIG_SITE="$ac_default_prefix/share/config.site $ac_default_prefix/etc/config.site"
+  fi
+fi
+for ac_site_file in $CONFIG_SITE; do
+  if test -r "$ac_site_file"; then
+    echo "loading site script $ac_site_file"
+    . "$ac_site_file"
+  fi
+done
+
+if test -r "$cache_file"; then
+  echo "loading cache $cache_file"
+  . $cache_file
+else
+  echo "creating cache $cache_file"
+  > $cache_file
+fi
+
+ac_ext=c
+# CFLAGS is not in ac_cpp because -g, -O, etc. are not valid cpp options.
+ac_cpp='$CPP $CPPFLAGS'
+ac_compile='${CC-cc} -c $CFLAGS $CPPFLAGS conftest.$ac_ext 1>&5'
+ac_link='${CC-cc} -o conftest${ac_exeext} $CFLAGS $CPPFLAGS $LDFLAGS conftest.$ac_ext $LIBS 1>&5'
+cross_compiling=$ac_cv_prog_cc_cross
+
+ac_exeext=
+ac_objext=o
+if (echo "testing\c"; echo 1,2,3) | grep c >/dev/null; then
+  # Stardent Vistra SVR4 grep lacks -e, says ghazi@caip.rutgers.edu.
+  if (echo -n testing; echo 1,2,3) | sed s/-n/xn/ | grep xn >/dev/null; then
+    ac_n= ac_c='
+' ac_t='	'
+  else
+    ac_n=-n ac_c= ac_t=
+  fi
+else
+  ac_n= ac_c='\c' ac_t=
+fi
+
+
+
+# Check for Coq binaries
+
+# we first look for coqtop.byte in the path; if not present we fail
+# Extract the first word of "coqtop.byte", so it can be a program name with args.
+set dummy coqtop.byte; ac_word=$2
+echo $ac_n "checking for $ac_word""... $ac_c" 1>&6
+echo "configure:532: checking for $ac_word" >&5
+if eval "test \"`echo '$''{'ac_cv_prog_COQTOPBYTE'+set}'`\" = set"; then
+  echo $ac_n "(cached) $ac_c" 1>&6
+else
+  if test -n "$COQTOPBYTE"; then
+  ac_cv_prog_COQTOPBYTE="$COQTOPBYTE" # Let the user override the test.
+else
+  IFS="${IFS= 	}"; ac_save_ifs="$IFS"; IFS=":"
+  ac_dummy="$PATH"
+  for ac_dir in $ac_dummy; do
+    test -z "$ac_dir" && ac_dir=.
+    if test -f $ac_dir/$ac_word; then
+      ac_cv_prog_COQTOPBYTE="coqtop.byte"
+      break
+    fi
+  done
+  IFS="$ac_save_ifs"
+  test -z "$ac_cv_prog_COQTOPBYTE" && ac_cv_prog_COQTOPBYTE="no"
+fi
+fi
+COQTOPBYTE="$ac_cv_prog_COQTOPBYTE"
+if test -n "$COQTOPBYTE"; then
+  echo "$ac_t""$COQTOPBYTE" 1>&6
+else
+  echo "$ac_t""no" 1>&6
+fi
+
+if test "$COQTOPBYTE" = no ; then
+	{ echo "configure: error: Cannot find coqtop.byte" 1>&2; exit 1; }
+fi
+
+# we extract Coq version number and library path
+echo $COQTOPBYTE
+COQVERSION=`$COQTOPBYTE -v | sed -n -e 's|.*version* *\([^ ]*\).*|\1|p' `
+echo "Coq version is $COQVERSION"
+COQLIB=`$COQTOPBYTE -where`
+echo "Coq library path is $COQLIB"
+
+# then we look for coqc
+# Extract the first word of "coqc", so it can be a program name with args.
+set dummy coqc; ac_word=$2
+echo $ac_n "checking for $ac_word""... $ac_c" 1>&6
+echo "configure:574: checking for $ac_word" >&5
+if eval "test \"`echo '$''{'ac_cv_prog_COQC'+set}'`\" = set"; then
+  echo $ac_n "(cached) $ac_c" 1>&6
+else
+  if test -n "$COQC"; then
+  ac_cv_prog_COQC="$COQC" # Let the user override the test.
+else
+  IFS="${IFS= 	}"; ac_save_ifs="$IFS"; IFS=":"
+  ac_dummy="$PATH"
+  for ac_dir in $ac_dummy; do
+    test -z "$ac_dir" && ac_dir=.
+    if test -f $ac_dir/$ac_word; then
+      ac_cv_prog_COQC="coqc"
+      break
+    fi
+  done
+  IFS="$ac_save_ifs"
+  test -z "$ac_cv_prog_COQC" && ac_cv_prog_COQC="no"
+fi
+fi
+COQC="$ac_cv_prog_COQC"
+if test -n "$COQC"; then
+  echo "$ac_t""$COQC" 1>&6
+else
+  echo "$ac_t""no" 1>&6
+fi
+
+if test "$COQC" = no ; then
+	{ echo "configure: error: Cannot find coqc" 1>&2; exit 1; }
+fi
+COQCVERSION=`$COQC -v | sed -n -e 's|.*version* *\([^ ]*\).*|\1|p' `
+echo $ac_n "checking coqc version""... $ac_c" 1>&6
+echo "configure:606: checking coqc version" >&5
+if test "$COQCVERSION" != $COQVERSION ; then
+    { echo "configure: error: coqc and coqtop.byte versions differ" 1>&2; exit 1; }
+else
+    echo "$ac_t""ok" 1>&6
+fi
+
+# we look for coq-tex
+# Extract the first word of "coq-tex", so it can be a program name with args.
+set dummy coq-tex; ac_word=$2
+echo $ac_n "checking for $ac_word""... $ac_c" 1>&6
+echo "configure:617: checking for $ac_word" >&5
+if eval "test \"`echo '$''{'ac_cv_prog_COQTEX'+set}'`\" = set"; then
+  echo $ac_n "(cached) $ac_c" 1>&6
+else
+  if test -n "$COQTEX"; then
+  ac_cv_prog_COQTEX="$COQTEX" # Let the user override the test.
+else
+  IFS="${IFS= 	}"; ac_save_ifs="$IFS"; IFS=":"
+  ac_dummy="$PATH"
+  for ac_dir in $ac_dummy; do
+    test -z "$ac_dir" && ac_dir=.
+    if test -f $ac_dir/$ac_word; then
+      ac_cv_prog_COQTEX="coq-tex"
+      break
+    fi
+  done
+  IFS="$ac_save_ifs"
+  test -z "$ac_cv_prog_COQTEX" && ac_cv_prog_COQTEX="no"
+fi
+fi
+COQTEX="$ac_cv_prog_COQTEX"
+if test -n "$COQTEX"; then
+  echo "$ac_t""$COQTEX" 1>&6
+else
+  echo "$ac_t""no" 1>&6
+fi
+
+if test "$COQTEX" = no ; then
+    { echo "configure: error: Cannot find coq-tex" 1>&2; exit 1; }
+fi
+# substitutions to perform
+
+
+
+
+
+
+# Finally create the Makefile from Makefile.in
+trap '' 1 2 15
+cat > confcache <<\EOF
+# This file is a shell script that caches the results of configure
+# tests run on this system so they can be shared between configure
+# scripts and configure runs.  It is not useful on other systems.
+# If it contains results you don't want to keep, you may remove or edit it.
+#
+# By default, configure uses ./config.cache as the cache file,
+# creating it if it does not exist already.  You can give configure
+# the --cache-file=FILE option to use a different cache file; that is
+# what configure does when it calls configure scripts in
+# subdirectories, so they share the cache.
+# Giving --cache-file=/dev/null disables caching, for debugging configure.
+# config.status only pays attention to the cache file if you give it the
+# --recheck option to rerun configure.
+#
+EOF
+# The following way of writing the cache mishandles newlines in values,
+# but we know of no workaround that is simple, portable, and efficient.
+# So, don't put newlines in cache variables' values.
+# Ultrix sh set writes to stderr and can't be redirected directly,
+# and sets the high bit in the cache file unless we assign to the vars.
+(set) 2>&1 |
+  case `(ac_space=' '; set | grep ac_space) 2>&1` in
+  *ac_space=\ *)
+    # `set' does not quote correctly, so add quotes (double-quote substitution
+    # turns \\\\ into \\, and sed turns \\ into \).
+    sed -n \
+      -e "s/'/'\\\\''/g" \
+      -e "s/^\\([a-zA-Z0-9_]*_cv_[a-zA-Z0-9_]*\\)=\\(.*\\)/\\1=\${\\1='\\2'}/p"
+    ;;
+  *)
+    # `set' quotes correctly as required by POSIX, so do not add quotes.
+    sed -n -e 's/^\([a-zA-Z0-9_]*_cv_[a-zA-Z0-9_]*\)=\(.*\)/\1=${\1=\2}/p'
+    ;;
+  esac >> confcache
+if cmp -s $cache_file confcache; then
+  :
+else
+  if test -w $cache_file; then
+    echo "updating cache $cache_file"
+    cat confcache > $cache_file
+  else
+    echo "not updating unwritable cache $cache_file"
+  fi
+fi
+rm -f confcache
+
+trap 'rm -fr conftest* confdefs* core core.* *.core $ac_clean_files; exit 1' 1 2 15
+
+test "x$prefix" = xNONE && prefix=$ac_default_prefix
+# Let make expand exec_prefix.
+test "x$exec_prefix" = xNONE && exec_prefix='${prefix}'
+
+# Any assignment to VPATH causes Sun make to only execute
+# the first set of double-colon rules, so remove it if not needed.
+# If there is a colon in the path, we need to keep it.
+if test "x$srcdir" = x.; then
+  ac_vpsub='/^[ 	]*VPATH[ 	]*=[^:]*$/d'
+fi
+
+trap 'rm -f $CONFIG_STATUS conftest*; exit 1' 1 2 15
+
+# Transform confdefs.h into DEFS.
+# Protect against shell expansion while executing Makefile rules.
+# Protect against Makefile macro expansion.
+cat > conftest.defs <<\EOF
+s%#define \([A-Za-z_][A-Za-z0-9_]*\) *\(.*\)%-D\1=\2%g
+s%[ 	`~#$^&*(){}\\|;'"<>?]%\\&%g
+s%\[%\\&%g
+s%\]%\\&%g
+s%\$%$$%g
+EOF
+DEFS=`sed -f conftest.defs confdefs.h | tr '\012' ' '`
+rm -f conftest.defs
+
+
+# Without the "./", some shells look in PATH for config.status.
+: ${CONFIG_STATUS=./config.status}
+
+echo creating $CONFIG_STATUS
+rm -f $CONFIG_STATUS
+cat > $CONFIG_STATUS <<EOF
+#! /bin/sh
+# Generated automatically by configure.
+# Run this file to recreate the current configuration.
+# This directory was configured as follows,
+# on host `(hostname || uname -n) 2>/dev/null | sed 1q`:
+#
+# $0 $ac_configure_args
+#
+# Compiler output produced by configure, useful for debugging
+# configure, is in ./config.log if it exists.
+
+ac_cs_usage="Usage: $CONFIG_STATUS [--recheck] [--version] [--help]"
+for ac_option
+do
+  case "\$ac_option" in
+  -recheck | --recheck | --rechec | --reche | --rech | --rec | --re | --r)
+    echo "running \${CONFIG_SHELL-/bin/sh} $0 $ac_configure_args --no-create --no-recursion"
+    exec \${CONFIG_SHELL-/bin/sh} $0 $ac_configure_args --no-create --no-recursion ;;
+  -version | --version | --versio | --versi | --vers | --ver | --ve | --v)
+    echo "$CONFIG_STATUS generated by autoconf version 2.13"
+    exit 0 ;;
+  -help | --help | --hel | --he | --h)
+    echo "\$ac_cs_usage"; exit 0 ;;
+  *) echo "\$ac_cs_usage"; exit 1 ;;
+  esac
+done
+
+ac_given_srcdir=$srcdir
+
+trap 'rm -fr `echo "Makefile" | sed "s/:[^ ]*//g"` conftest*; exit 1' 1 2 15
+EOF
+cat >> $CONFIG_STATUS <<EOF
+
+# Protect against being on the right side of a sed subst in config.status.
+sed 's/%@/@@/; s/@%/@@/; s/%g\$/@g/; /@g\$/s/[\\\\&%]/\\\\&/g;
+ s/@@/%@/; s/@@/@%/; s/@g\$/%g/' > conftest.subs <<\\CEOF
+$ac_vpsub
+$extrasub
+s%@SHELL@%$SHELL%g
+s%@CFLAGS@%$CFLAGS%g
+s%@CPPFLAGS@%$CPPFLAGS%g
+s%@CXXFLAGS@%$CXXFLAGS%g
+s%@FFLAGS@%$FFLAGS%g
+s%@DEFS@%$DEFS%g
+s%@LDFLAGS@%$LDFLAGS%g
+s%@LIBS@%$LIBS%g
+s%@exec_prefix@%$exec_prefix%g
+s%@prefix@%$prefix%g
+s%@program_transform_name@%$program_transform_name%g
+s%@bindir@%$bindir%g
+s%@sbindir@%$sbindir%g
+s%@libexecdir@%$libexecdir%g
+s%@datadir@%$datadir%g
+s%@sysconfdir@%$sysconfdir%g
+s%@sharedstatedir@%$sharedstatedir%g
+s%@localstatedir@%$localstatedir%g
+s%@libdir@%$libdir%g
+s%@includedir@%$includedir%g
+s%@oldincludedir@%$oldincludedir%g
+s%@infodir@%$infodir%g
+s%@mandir@%$mandir%g
+s%@COQTOPBYTE@%$COQTOPBYTE%g
+s%@COQC@%$COQC%g
+s%@COQTEX@%$COQTEX%g
+s%@COQLIB@%$COQLIB%g
+s%@COQVERSION@%$COQVERSION%g
+
+CEOF
+EOF
+
+cat >> $CONFIG_STATUS <<\EOF
+
+# Split the substitutions into bite-sized pieces for seds with
+# small command number limits, like on Digital OSF/1 and HP-UX.
+ac_max_sed_cmds=90 # Maximum number of lines to put in a sed script.
+ac_file=1 # Number of current file.
+ac_beg=1 # First line for current file.
+ac_end=$ac_max_sed_cmds # Line after last line for current file.
+ac_more_lines=:
+ac_sed_cmds=""
+while $ac_more_lines; do
+  if test $ac_beg -gt 1; then
+    sed "1,${ac_beg}d; ${ac_end}q" conftest.subs > conftest.s$ac_file
+  else
+    sed "${ac_end}q" conftest.subs > conftest.s$ac_file
+  fi
+  if test ! -s conftest.s$ac_file; then
+    ac_more_lines=false
+    rm -f conftest.s$ac_file
+  else
+    if test -z "$ac_sed_cmds"; then
+      ac_sed_cmds="sed -f conftest.s$ac_file"
+    else
+      ac_sed_cmds="$ac_sed_cmds | sed -f conftest.s$ac_file"
+    fi
+    ac_file=`expr $ac_file + 1`
+    ac_beg=$ac_end
+    ac_end=`expr $ac_end + $ac_max_sed_cmds`
+  fi
+done
+if test -z "$ac_sed_cmds"; then
+  ac_sed_cmds=cat
+fi
+EOF
+
+cat >> $CONFIG_STATUS <<EOF
+
+CONFIG_FILES=\${CONFIG_FILES-"Makefile"}
+EOF
+cat >> $CONFIG_STATUS <<\EOF
+for ac_file in .. $CONFIG_FILES; do if test "x$ac_file" != x..; then
+  # Support "outfile[:infile[:infile...]]", defaulting infile="outfile.in".
+  case "$ac_file" in
+  *:*) ac_file_in=`echo "$ac_file"|sed 's%[^:]*:%%'`
+       ac_file=`echo "$ac_file"|sed 's%:.*%%'` ;;
+  *) ac_file_in="${ac_file}.in" ;;
+  esac
+
+  # Adjust a relative srcdir, top_srcdir, and INSTALL for subdirectories.
+
+  # Remove last slash and all that follows it.  Not all systems have dirname.
+  ac_dir=`echo $ac_file|sed 's%/[^/][^/]*$%%'`
+  if test "$ac_dir" != "$ac_file" && test "$ac_dir" != .; then
+    # The file is in a subdirectory.
+    test ! -d "$ac_dir" && mkdir "$ac_dir"
+    ac_dir_suffix="/`echo $ac_dir|sed 's%^\./%%'`"
+    # A "../" for each directory in $ac_dir_suffix.
+    ac_dots=`echo $ac_dir_suffix|sed 's%/[^/]*%../%g'`
+  else
+    ac_dir_suffix= ac_dots=
+  fi
+
+  case "$ac_given_srcdir" in
+  .)  srcdir=.
+      if test -z "$ac_dots"; then top_srcdir=.
+      else top_srcdir=`echo $ac_dots|sed 's%/$%%'`; fi ;;
+  /*) srcdir="$ac_given_srcdir$ac_dir_suffix"; top_srcdir="$ac_given_srcdir" ;;
+  *) # Relative path.
+    srcdir="$ac_dots$ac_given_srcdir$ac_dir_suffix"
+    top_srcdir="$ac_dots$ac_given_srcdir" ;;
+  esac
+
+
+  echo creating "$ac_file"
+  rm -f "$ac_file"
+  configure_input="Generated automatically from `echo $ac_file_in|sed 's%.*/%%'` by configure."
+  case "$ac_file" in
+  *Makefile*) ac_comsub="1i\\
+# $configure_input" ;;
+  *) ac_comsub= ;;
+  esac
+
+  ac_file_inputs=`echo $ac_file_in|sed -e "s%^%$ac_given_srcdir/%" -e "s%:% $ac_given_srcdir/%g"`
+  sed -e "$ac_comsub
+s%@configure_input@%$configure_input%g
+s%@srcdir@%$srcdir%g
+s%@top_srcdir@%$top_srcdir%g
+" $ac_file_inputs | (eval "$ac_sed_cmds") > $ac_file
+fi; done
+rm -f conftest.s*
+
+EOF
+cat >> $CONFIG_STATUS <<EOF
+
+EOF
+cat >> $CONFIG_STATUS <<\EOF
+
+exit 0
+EOF
+chmod +x $CONFIG_STATUS
+rm -fr confdefs* $ac_clean_files
+test "$no_create" = yes || ${CONFIG_SHELL-/bin/sh} $CONFIG_STATUS || exit 1
+
diff --git a/doc/configure.in b/doc/configure.in
new file mode 100644
index 0000000000..d4eecdd832
--- /dev/null
+++ b/doc/configure.in
@@ -0,0 +1,54 @@
+# autoconf input for Coq documentation
+#
+# the script generated by autoconf from this input will set the following
+# variables:
+#   COQTOP        "coqtop.byte"
+#   COQLIB        result of $COQTOP -where
+#   COQVERSION    result of $COQTOP -v
+#   COQC          "coqc"
+
+# check for one particular file of the sources 
+AC_INIT(Reference-Manual.tex)
+
+# Check for Coq binaries
+
+# we first look for coqtop.byte in the path; if not present we fail
+AC_CHECK_PROG(COQTOPBYTE,coqtop.byte,coqtop.byte,no)
+if test "$COQTOPBYTE" = no ; then
+	AC_MSG_ERROR(Cannot find coqtop.byte)
+fi
+
+# we extract Coq version number and library path
+echo $COQTOPBYTE
+COQVERSION=`$COQTOPBYTE -v | sed -n -e 's|.*version* *\([[^ ]]*\).*|\1|p' `
+echo "Coq version is $COQVERSION"
+COQLIB=`$COQTOPBYTE -where`
+echo "Coq library path is $COQLIB"
+
+# then we look for coqc
+AC_CHECK_PROG(COQC,coqc,coqc,no)
+if test "$COQC" = no ; then
+	AC_MSG_ERROR(Cannot find coqc)
+fi
+COQCVERSION=`$COQC -v | sed -n -e 's|.*version* *\([[^ ]]*\).*|\1|p' `
+AC_MSG_CHECKING(coqc version)
+if test "$COQCVERSION" != $COQVERSION ; then
+    AC_MSG_ERROR(coqc and coqtop.byte versions differ)
+else
+    AC_MSG_RESULT(ok)
+fi
+
+# we look for coq-tex
+AC_CHECK_PROG(COQTEX,coq-tex,coq-tex,no)
+if test "$COQTEX" = no ; then
+    AC_MSG_ERROR(Cannot find coq-tex)
+fi
+# substitutions to perform
+AC_SUBST(COQTOPBYTE)
+AC_SUBST(COQC)
+AC_SUBST(COQLIB)
+AC_SUBST(COQVERSION)
+AC_SUBST(COQTEX)
+
+# Finally create the Makefile from Makefile.in
+AC_OUTPUT(Makefile)
diff --git a/doc/macros.tex b/doc/macros.tex
index 3ccfbbdddf..108d716357 100755
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -2,7 +2,7 @@
 % MACROS FOR THE REFERENCE MANUAL OF COQ %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\newcommand{\coqversion}{6.3.1}
+\newcommand{\coqversion}{7.0}
 
 % For commentaries (define \com as {} for the release manual)
 %\newcommand{\com}[1]{{\it(* #1 *)}}
diff --git a/doc/title.tex b/doc/title.tex
index 816f0fd539..14ca2204d1 100755
--- a/doc/title.tex
+++ b/doc/title.tex
@@ -46,7 +46,7 @@ Action ``Types'' and by the GDR ``Programmation'' co-financed by MRE-PRC and CNR
 \vspace*{520pt}
 \thispagestyle{empty}
 \begin{flushleft}
-{\large{V6.3.1,
+{\large{V7.0,
 \printingdate}}\\[20pt]
 {\large{\copyright INRIA 1999}}\\
 \end{flushleft}