abandon de autonconf au profit de variables d'environnement

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

4 files changed, 58 insertions, 981 deletions

diff --git a/doc/.cvsignore b/doc/.cvsignore
index 2a42b26550..2761b637c6 100644
--- a/doc/.cvsignore
+++ b/doc/.cvsignore
@@ -26,7 +26,6 @@ doc-html.tar.gz
 all-ps-docs.tar.gz
 config.cache
 config.status
-Makefile
 Reference-Manual.rel
 library.files
 library.coqweb.tex
diff --git a/doc/Makefile.in b/doc/Makefile
index e578bbe5ff..ca6f1cc9f7 100644
--- a/doc/Makefile.in
+++ b/doc/Makefile
@@ -1,23 +1,29 @@
+# Makefile for the Coq documentation
+
+# You need the environment varibles COQTOP and COQBIN to be correctly set
+# (some files are preprocessed using Coq and some part of the documentation
+# is automatically built from the theories sources)
+
 # To compile documentation, you need the following tools:
 # Dvi: latex (latex2e), bibtex, makeindex, dviselect (package RPM dviutils)
 # Ps: dvips, psutils (ftp://ftp.dcs.ed.ac.uk/pub/ajcd/psutils.tar.gz)
 # Pdf: pdflatex
 # Html:
 #   - hevea: http://para.inria.fr/~maranget/hevea/
-#   - htmlSplit: http://coq.inria.fr/~delahaye/
+#   - htmlSplit: http://coq.inria.fr/~delahaye
 # Rapports INRIA: dviselect, rrkit (par Michel Mauny)
 
-DOCCOQTOP=@COQTOPBYTE@
-DOCCOQC=@COQC@ -byte
-COQLIB=@COQLIB@
-COQTEX=@COQTEX@ -image $(DOCCOQTOP) -v -sl -small
+DOCCOQTOP=$(COQBIN)/coqtop.byte
+DOCCOQC=$(COQBIN)/coqc
+COQTEX=$(COQBIN)/coq-tex -image $(DOCCOQTOP) -v -sl -small
+COQWEBSTY=$(HOME)/tex/inputs
 
 LATEX=latex
 BIBTEX=bibtex
 MAKEINDEX=makeindex
 PDFLATEX=pdflatex
 
-TEXINPUTS=/usr/local/lib/rrkit/RRINPUTSDIR:.:
+TEXINPUTS=/usr/local/lib/rrkit/RRINPUTSDIR:$(COQWEBSTY):.:
 
 INPUTS=./macros.tex ./title.tex ./headers.tex ./Reference-Manual.tex
 
@@ -27,11 +33,11 @@ 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-tus.v.tex RefMan-oth.v.tex
+  RefMan-syn.v.tex RefMan-ltac.v.tex RefMan-oth.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 \
-  Programs.v.tex
+  Correctness.v.tex
 
 REFMANFILES= Reference-Manual.tex RefMan-pre.tex RefMan-int.tex \
   RefMan-pro.tex RefMan-com.tex RefMan-uti.tex RefMan-add.tex \
@@ -58,7 +64,11 @@ FTPHTMLDOCS=doc-html.tar.gz
 # Principal targets 
 ########################
 
-all: all-dvi all-pdf
+all: check-env all-dvi all-pdf
+
+check-env:
+	if test "$(COQBIN)" = ""; then echo "COQBIN undefined"; exit 1; fi
+	if test "$(COQTOP)" = ""; then echo "COQTOP undefined"; exit 1; fi
 
 coq-part: $(REFMANCOQTEXFILES) $(COQTEXFILES) demos-programs library/libdoc.tex
 
@@ -184,13 +194,45 @@ cleanall: clean clean-html
 # Dependencies
 ##########################
 
-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)
+Library.dvi: $(INPUTS) library.coqweb.tex Library.tex
+	$(LATEX) Library
+	$(LATEX) Library
+
+Library.pdf: $(INPUTS) library.coqweb.tex Library.tex
+	$(PDFLATEX) Library
+	$(PDFLATEX) Library
+
+Library.html: $(INPUTS) library.coqweb.tex Library.tex
+	hevea ./coq-html.sty $(COQWEBSTY)/coqweb.sty ./Library.tex
+
+LIBDIRS= Logic Bool Arith Zarith Reals Lists Sets Relations \
+         Wellfounded IntMap
+
+library.coqweb.tex: library.files
+	WHERE=`pwd` ; \
+	cd $(COQTOP)/theories; \
+	coqweb --noweb -o $$WHERE/$@ --no-preamble `cat $$WHERE/library.files`
+
+GALLINA=$(COQBIN)/gallina
+
+# ls -tr trie les fichiers dans l'ordre inverse de leur date de création
+# En supposant que make fait son boulot, ca fait un tri topologique du
+# graphe des dépendances
+library.files::
+	rm -f library.files; touch library.files
+	ABSOLUTE=`pwd`/library.files ; \
+	for rep in $(LIBDIRS) ; do \
+	  (cd $(COQTOP)/theories/$$rep ; \
+	   echo $$rep/intro.tex >> $$ABSOLUTE ; \
+	   VOFILES=`ls -tr *.vo` ; \
+	   for file in $$VOFILES ; do \
+		VF=`basename $$file \.vo` ; \
+		if test \( ! -e $$VF.g \) -o \( $$VF.v -nt $$VF.g \); then \
+	          $(GALLINA) $$VF.v; fi ; \
+		echo $$rep/$$VF.g >> $$ABSOLUTE ; \
+           done \
+	  ) ; \
+	done
 
 demos-programs:
 #	(cd ../theories/DEMOS/PROGRAMS ; make all)
diff --git a/doc/configure b/doc/configure
deleted file mode 100755
index 47d270725c..0000000000
--- a/doc/configure
+++ /dev/null
@@ -1,909 +0,0 @@
-#! /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
deleted file mode 100644
index 2c6ca66531..0000000000
--- a/doc/configure.in
+++ /dev/null
@@ -1,55 +0,0 @@
-# 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)