12 files changed, 652 insertions, 387 deletions
diff --git a/doc/Makefile b/doc/Makefile
index d61e02a3c..ac1be10f1 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -1,368 +1,280 @@
 # Makefile for the Coq documentation
 
-# if coqc,coqtop,coq-tex are not in your PATH, you need the environment 
-# variable COQBIN to be correctly set  
-# (COQTOP is autodetected)
-# (some files are preprocessed using Coq and some part of the documentation
-# is automatically built from the theories sources)
+# COQTOP needs to be set to a coq source repository
 
 # 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)
+# Dvi: latex (latex2e), bibtex, makeindex
 # Pdf: pdflatex
-# Html:
-#   - hevea: http://para.inria.fr/~maranget/hevea/
-#   - htmlSplit: http://coq.inria.fr/~delahaye
-# Rapports INRIA: dviselect, rrkit (par Michel Mauny)
-
-
-ifeq ("$(COQBIN)","")
- COQBINPATH =  
-else    
- COQBINPATH = $(COQBIN)/
-endif
-
-DOCCOQTOP=$(COQBINPATH)coqtop #.byte
-DOCCOQC=$(COQBINPATH)coqc
-COQTOP=`$(DOCCOQC) -where`
-COQTEX=$(COQBINPATH)coq-tex -n 72 -image $(DOCCOQTOP) -v -sl -small
-#COQWEBSTY=$(HOME)/lib/tex/
-COQWEBSTY=/usr/share/texmf/tex/latex/misc/
-HEVEALIB=/usr/local/lib/hevea:/usr/lib/hevea
+# Html: hevea (http://hevea.inria.fr) >= 1.05
 
 LATEX=latex
 BIBTEX=bibtex -min-crossrefs=10
 MAKEINDEX=makeindex
 PDFLATEX=pdflatex
 
-MKDIR=mkdir
-TEST=test
+HEVEALIB=/usr/local/lib/hevea:/usr/lib/hevea
+TEXINPUTS=$(HEVEALIB):.:
 
-TEXINPUTS=/usr/local/lib/rrkit/RRINPUTSDIR:$(COQWEBSTY):$(HEVEALIB):.:
+DOCCOQTOP=$(COQTOP)/bin/coqtop
+COQTEX=$(COQTOP)/bin/coq-tex -n 72 -image $(DOCCOQTOP) -v -sl -small
+COQDOC=$(COQTOP)/bin/coqdoc
 
-INPUTS=./version.tex ./macros.tex ./title.tex ./headers.tex ./Reference-Manual.tex
+VERSION=8.0pl3
+#VERSION=POSITIONNEZ-CETTE-VARIABLE
 
-LIBFILES=library/Logic.tex library/Datatypes.tex library/Peano.tex \
-         library/Wf.tex library/Specif.tex
+######################################################################
+### General rules
+######################################################################
 
-REFMANCOQTEXFILES=\
-  RefMan-gal.v.tex RefMan-ext.v.tex RefMan-mod.v.tex RefMan-tac.v.tex \
-  RefMan-cic.v.tex RefMan-lib.v.tex RefMan-tacex.v.tex \
-  RefMan-syn.v.tex RefMan-oth.v.tex
+all: all-html all-pdf all-ps
 
-COQTEXFILES= Cases.v.tex Coercion.v.tex Extraction.v.tex \
-  Omega.v.tex Changes.v.tex Tutorial.v.tex Polynom.v.tex \
-  Setoid.v.tex Helm.tex
-#SUPPRIME: Program.v.tex Natural.v.tex Correctness.v.tex
+all-html:\
+  tutorial/Tutorial.v.html refman/html/index.html \
+  faq/html/index.html stdlib/html/index.html
 
-REFMANFILES= Reference-Manual.tex RefMan-pre.tex RefMan-int.tex \
-  RefMan-pro.tex RefMan-com.tex RefMan-ltac.tex RefMan-uti.tex \
-  RefMan-ide.tex coqide.eps coqide-queries.eps RefMan-add.tex RefMan-modr.tex \
-  $(REFMANCOQTEXFILES) 
+all-pdf:\
+  tutorial/Tutorial.v.pdf refman/Reference-Manual.pdf \
+  faq/faq.v.pdf stdlib/Library.pdf
 
-REFMAN=Reference-Manual
+all-ps:\
+  tutorial/Tutorial.v.ps refman/Reference-Manual.ps \
+  faq/faq.v.ps stdlib/Library.ps
 
-VERSION=8.0
-#VERSION=POSITIONNEZ-CETTE-VARIABLE
+refman:\
+  refman/html/index.html refman/Reference-Manual.ps refman/Reference-Manual.pdf
 
-FTPDOCDIR=/net/pauillac/infosystems/ftp/coq/coq/V$(VERSION)/doc
-WWWDOCDIR=/net/pauillac/infosystems/www/coq/doc
-
-FTPDOCS=Reference-Manual-base.ps.gz Reference-Manual-base.dvi.gz \
-        Reference-Manual-addendum.ps.gz Reference-Manual-addendum.dvi.gz\
-        Reference-Manual-all.ps.gz Reference-Manual-all.dvi.gz\
-#	Library.dvi.gz Library.ps.gz\
-        Tutorial.dvi.gz Tutorial.ps.gz\
-#        README all-ps-docs.tar.gz\
-#	Changes.dvi.gz Changes.ps.gz
-
-FTPHTMLDOCS=doc-html.tar.gz
-
-#########################
-# Principal targets 
-########################
-
-all: check-env all-ps all-pdf
-
-check-env:
-	@if $(TEST) "$(COQBIN)" = ""; then \
-		if coq-tex; then true ; \
-		else echo "coq-tex not found, COQBIN undefined"; exit 1; fi; \
-	fi
-	@if $(TEST) "$(COQTOP)" = ""; then echo "COQTOP undefined"; exit 1; \
-		else echo "COQTOP = $(COQTOP)"; fi
-
-coq-part: $(REFMANCOQTEXFILES) $(COQTEXFILES) demos-programs library/libdoc.tex
-
-latex-part: all-dvi
-
-all-dvi: Tutorial.v.dvi Reference-Manual.dvi # faq.v.dvi Library.dvi Changes.v.dvi
-
-all-pdf: Tutorial.v.pdf Reference-Manual.pdf # faq.v.pdf Library.pdf Changes.v.pdf
-
-all-ps: Tutorial.v.ps Reference-Manual.ps # faq.v.ps  Library.ps Changes.v.ps
-
-all-html: Tutorial.v.html Reference-Manual.html # faq.v.html Library.html Changes.v.html
-
-#version
-version.tex: Makefile
-	echo "\newcommand{\coqversion}{$(VERSION)}" > version.tex
-
-
-# dvips et dviselect existent sur loupiac
-distrib:
-	make check-env
-	make clean-coq demos-programs
-	make clean-latex all-dvi all-ps all-pdf compress-latex
-	make clean-html all-html doc-html.tar.gz html-www
-
-compress-latex:
-	sh Reference-Manual.sh
-	mv -f Reference-Manual.ps Reference-Manual-all.ps
-	mv -f Tutorial.v.ps Tutorial.ps
-	mv -f Tutorial.v.dvi Tutorial.dvi
-	mv -f Reference-Manual.dvi Reference-Manual-all.dvi
-#	mv -f Changes.v.ps Changes.ps
-#	mv -f Changes.v.dvi Changes.dvi
-	- mv -f Tutorial.v.pdf Tutorial.pdf
-#	- mv -f Changes.v.pdf Changes.pdf
-	tar cf all-ps-docs.tar Reference-Manual-base.ps \
-	  Reference-Manual-addendum.ps Tutorial.ps # Library.ps # Changes.ps
-	gzip -f *.ps
-	gzip -f *.dvi
-	gzip -f *.pdf
-	gzip -f all-ps-docs.tar
-
-Tutorial.v.html: Tutorial.v.tex
-	hevea ./book-html.sty ./coq-html.sty ./Tutorial.v
-
-Changes.v.html: Changes.v.tex
-	hevea ./Changes.v.tex
-
-Reference-Manual.html: $(INPUTS) $(REFMANFILES) $(COQTEXFILES) biblio.bib
-#1.05 ?	hevea -fix ./book-html.sty ./coq-html.sty ./Reference-Manual.tex
-#1.04	hevea ./book-html.sty ./coq-html.sty ./Reference-Manual.tex
-	hevea -fix -nosymb -exec xxdate.exe ./Reference-Manual.tex
-
-faq.v.html: faq.v.tex
-	hevea ./faq.v
-
-coq.info: $(INPUTS) $(REFMANFILES) $(COQTEXFILES) biblio.bib
-	hevea -info ./book-html.sty ./coq-html.sty ./Reference-Manual.tex
-
-doc-html.tar.gz: all-html
-	$(MKDIR) -p coq-docs-html
-	rm -rf coq-docs-html/*
-	cp Tutorial.v.html coq-docs-html/tutorial.html
-	cp Reference-Manual.html coqide-queries.png coqide.png coq-docs-html 
-	(cd coq-docs-html; hacha -o toc.html ./Reference-Manual.html; rm ./Reference-Manual.html)
-	cp cover.html main.html main-0.html coq-docs-html
-	tar cf doc-html.tar coq-docs-html
-	gzip -f doc-html.tar
-
-# Pour le site de Coq.
-html-www: all-html
-	$(MKDIR) -p www
-	rm -rf www/*
-	cp Tutorial.v.html www/tutorial.html
-	cp coqide-queries.png coqide.png www
-	(cd www; hacha -o toc.html ../Reference-Manual.html)
-	cp cover.html main.html main-0.html www
-	ln -s main.html www/index.html
-
-
-clean-refman:
-	rm -f Reference-Manual.toc Reference-Manual.idx Reference-Manual.atoc\
-	  Reference-Manual.aux Reference-Manual.bbl Reference-Manual.blg\
-	  Reference-Manual.ilg Reference-Manual.ind\
-	  Reference-Manual.tacidx Reference-Manual.tacind\
-	  Reference-Manual.comidx Reference-Manual.comind\
-	  Reference-Manual.erridx Reference-Manual.errind\
-          Reference-Manual.dvi Reference-Manual.ps\
-	  Reference-Manual.sh\
-	  $(REFMANFILES:.tex=.aux) $(REFMANFILES:.tex=.log)\
-	  $(COQTEXFILES:.tex=.aux) $(COQTEXFILES:.tex=.log)
-
-clean-latex: clean-refman
-	rm -f *.dvi *.aux *.log *.bbl *.blg *.ps *.toc *.idx *~ *.ilg *.ind\
-	*.dvi.gz *.ps.gz *.pdf *.pdf.gz
-
-clean-coq:
-	rm -f *.v.tex avl.ml heapsort.ml euclid.ml library/libdoc.tex *.cm[io]
-
-clean: clean-coq clean-latex
-
-clean-html:
-	rm -f Tutorial.v.html Reference-Manual.html # Changes.v.html
-	rm -f *.hatoc *.haux *.hcomind *.herrind *.hidx *.hind *.htacind *.htoc
-
-
-cleanall: clean clean-html
-
-#########################
-# Implicit rules
-#########################
+tutorial:\
+  tutorial/Tutorial.v.html tutorial/Tutorial.v.ps tutorial/Tutorial.v.pdf
 
-.SUFFIXES: .dvi .tex .v.tex .ps .pdf .eps .png
+stdlib:\
+  stdlib/html/index.html stdlib/Library.ps stdlib/Library.pdf
+
+faq:\
+  faq/html/index.html faq/faq.v.ps faq/faq.v.pdf
 
-.tex.dvi:
-	$(LATEX) $<
-	$(LATEX) $<
+######################################################################
+### Implicit rules
+######################################################################
 
-.tex.pdf:
-	$(PDFLATEX) $<
-	$(PDFLATEX) $<
+.SUFFIXES: .dvi .tex .v.tex .ps .pdf .eps .png
 
 .tex.v.tex:
-	$(COQTEX) $<
+	(cd `dirname $<`; $(COQTEX) `basename $<`)
 
 .dvi.ps:
-	dvips -o $@ $<
+	(cd `dirname $<`; dvips -o `basename $@` `basename $<`)
 
-%.eps: %.png
+.png.eps:
 	pngtopnm $< | pnmtops -equalpixels -noturn -rle > $@
 
+clean:
+	rm -f */*.dvi */*.aux */*.log */*.bbl */*.blg */*.toc \
+	*/*.idx */*~ */*.ilg */*.ind */*.dvi.gz */*.ps.gz */*.pdf.gz\
+	*/*.???idx */*.???ind */*.v.tex */*.atoc */*.lof\
+	*/*.hatoc */*.haux */*.hcomind */*.herrind */*.hidx */*.hind \
+	*/*.htacind */*.htoc */*.v.html
+	rm -f stdlib/index-list.html stdlib/index-body.html \
+	  stdlib/library.coqdoc.tex stdlib/library.files \
+	  stdlib/library.files.ls
+	rm -f refman/euclid.ml{,i} refman/heapsort.ml{,i}
+	rm -f common/version.tex
+	rm -f refman/*.eps refman/Reference-Manual.html
+
+cleanall: clean
+	rm -f */*.ps */*.pdf
+	rm -rf refman/html stdlib/html faq/html tutorial/tutorial.v.html
+
+######################################################################
+# Common
+######################################################################
 
+COMMON=common/version.tex common/title.tex common/macros.tex 
 
-##########################
-# Dependencies
-##########################
-
-Library.dvi: $(INPUTS) library.coqweb.tex Library.tex
-	$(LATEX) Library
-	$(LATEX) Library
-
-Library.pdf: $(INPUTS) library.coqweb.tex Library.tex
-	$(PDFLATEX) Library
-	$(PDFLATEX) Library
-
-# L'option -exec xxdate.exe sert a produire la date (macro \today) 
-# mais ne marche pas avec hevea 1.04
-Library.html: $(INPUTS) library.coqweb.tex Library.tex
-	hevea ./coq-html.sty -exec xxdate.exe $(COQWEBSTY)/coqweb.sty ./Library.tex
-#1.04	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=$(COQBINPATH)gallina
-
-# On garde la liste de tous les *.v avec dates dans library.files.ls
-# Si elle a change depuis la derniere fois ou library.files n'existe pas
-# on fabrique des .g (si besoin) et la liste library.files dans 
-# l'ordre de ls -tr des *.vo
-# Ce dernier 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.ls.tmp
-	(cd $(COQTOP)/theories ; find $(LIBDIRS) -name "*.v" -ls) > library.files.ls.tmp
-	if ! test -e library.files || ! cmp library.files.ls library.files.ls.tmp; then \
-	  mv -f library.files.ls.tmp library.files.ls; \
-	  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 ; \
-	fi
-
-demos-programs:
-#	(cd ../theories/DEMOS/PROGRAMS ; make all)
-
-Recursive-Definition.v.tex: ./title.tex Recursive-Definition.tex
-
-Tutorial.v.dvi: ./version.tex ./title.tex Tutorial.v.tex
-Tutorial.v.pdf: ./version.tex ./title.tex Tutorial.v.tex
-
-# RefMan-ppr.v.tex: ../tactics/eqdecide.cmo
-
-# RefMan-tus.v.tex: ../tactics/EqDecide.vo ../tactics/eqdecide.cmo
-
-Reference-Manual.ps: Reference-Manual.dvi
+### Version
+
+common/version.tex: Makefile
+	echo "\newcommand{\coqversion}{$(VERSION)}" > common/version.tex
+
+######################################################################
+# Reference Manual
+######################################################################
+
+REFMANCOQTEXFILES=\
+  refman/RefMan-gal.v.tex refman/RefMan-ext.v.tex \
+  refman/RefMan-mod.v.tex refman/RefMan-tac.v.tex \
+  refman/RefMan-cic.v.tex refman/RefMan-lib.v.tex \
+  refman/RefMan-tacex.v.tex refman/RefMan-syn.v.tex \
+  refman/RefMan-oth.v.tex \
+  refman/Cases.v.tex refman/Coercion.v.tex refman/Extraction.v.tex \
+  refman/Omega.v.tex refman/Polynom.v.tex \
+  refman/Setoid.v.tex refman/Helm.tex # refman/Natural.v.tex
+
+REFMANTEXFILES=\
+  refman/headers.tex \
+  refman/Reference-Manual.tex refman/RefMan-pre.tex \
+  refman/RefMan-int.tex refman/RefMan-pro.tex \
+  refman/RefMan-com.tex refman/RefMan-ltac.tex \
+  refman/RefMan-uti.tex refman/RefMan-ide.tex \
+  refman/RefMan-add.tex refman/RefMan-modr.tex \
+  $(REFMANCOQTEXFILES) \
+
+REFMANEPSFILES= refman/coqide.eps refman/coqide-queries.eps
+
+REFMANFILES=\
+  $(REFMANTEXFILES) $(COMMON) $(REFMANEPSFILES) refman/biblio.bib
+
+REFMANPNGFILES=$(REFMANEPSFILES:.eps=.png)
+
+### Reference Manual (printable format)
 
 # The second LATEX compilation is necessary otherwise the pages of the index
 # are not correct (don't know why...) - BB
-Reference-Manual.dvi: $(INPUTS) $(REFMANFILES) $(COQTEXFILES) biblio.bib
-	$(LATEX) Reference-Manual
-	$(BIBTEX) Reference-Manual
-	$(LATEX) Reference-Manual
-	$(MAKEINDEX) Reference-Manual
-	$(MAKEINDEX) Reference-Manual.tacidx -o Reference-Manual.tacind
-	$(MAKEINDEX) Reference-Manual.comidx -o Reference-Manual.comind
-	$(MAKEINDEX) Reference-Manual.erridx -o Reference-Manual.errind
-	$(LATEX) Reference-Manual
-	$(LATEX) Reference-Manual
-
-Reference-Manual.pdf: Reference-Manual.dvi
-	#rm -f Reference-Manual.sh
-	$(PDFLATEX) Reference-Manual.tex
-
-quick: $(INPUTS) $(REFMANFILES) $(COQTEXFILES) biblio.bib
-	#rm -f Reference-Manual.sh
-	$(LATEX) Reference-Manual
-
-
-###################
-# RT
-###################
-# Fabrication d'un RT INRIA (utilise rrkit de Michel Mauny)
-Reference-Manual-RT.dvi: Reference-Manual.dvi RefMan-cover.tex
-	dviselect -i Reference-Manual.dvi -o RefMan-body.dvi 3:
-	$(LATEX) RefMan-cover.tex
-	set a=`tail -1 Reference-Manual.log`;\
-	set a=expr \("$$a" : '.*(\(.*\) pages.*'\) % 2;\
-	if $(TEST) "$$a = 0";\
-	 then rrkit  RefMan-cover.dvi RefMan-body.dvi Reference-Manual-RT.dvi;\
-	 else rrkit -odd RefMan-cover.dvi RefMan-body.dvi Reference-Manual-RT.dvi;\
-	fi
-
-# Fabrication d'un RT INRIA (utilise rrkit de Michel Mauny)
-Tutorial-RT.dvi : Tutorial.v.dvi Tutorial-cover.tex
-	dviselect -i Tutorial.v.dvi -o Tutorial-body.dvi 3:
-	$(LATEX) Tutorial-cover.tex
-	set a=`tail -1 Tutorial.v.log`;\
-	set a=expr \("$$a" : '.*(\(.*\) pages.*'\) % 2;\
-	if $(TEST) "$$a = 0";\
-	 then rrkit      Tutorial-cover.dvi Tutorial-body.dvi Tutorial-RT.dvi;\
-	 else rrkit -odd Tutorial-cover.dvi Tutorial-body.dvi Tutorial-RT.dvi;\
-	fi
-
-################ doc ftp and www installation ############
-doc-ftp-www-install: doc-ftp-install doc-www-install
-
-doc-ftp-install: 
-	- mkdir $(FTPDOCDIR)
-	cp $(FTPDOCS) $(FTPHTMLDOCS) $(FTPDOCDIR)
-	- chmod g+w $(FTPDOCDIR)/*
-
-faq-www-install:
-	cp faq.v.html $(WWWDOCDIR)/faq.html
-
-doc-www-install: 
-	(cd $(WWWDOCDIR); rm -f node*.html main*.html toc.html \
-	 tutorial.html changes.html cover.html)
-	cp www/* $(WWWDOCDIR)
-
-# traducteur V7 -> V8
-tradv8: tradv8.ml4
-	ocamlopt.opt -o $@ str.cmxa unix.cmxa -pp "camlp4o -impl" -impl $^
-
-v8: tradv8
-	for f in `grep -l coq_exa *tex`; do \
-	  echo $$f; \
-	  ./tradv8 $$f; mv $$f $$f.save; mv $$f.v8 $$f; \
-	done
+refman/Reference-Manual.dvi: $(REFMANFILES)
+	(cd refman;\
+	$(LATEX) Reference-Manual;\
+	$(BIBTEX) Reference-Manual;\
+	$(LATEX) Reference-Manual;\
+	$(MAKEINDEX) Reference-Manual;\
+	$(MAKEINDEX) Reference-Manual.tacidx -o Reference-Manual.tacind;\
+	$(MAKEINDEX) Reference-Manual.comidx -o Reference-Manual.comind;\
+	$(MAKEINDEX) Reference-Manual.erridx -o Reference-Manual.errind;\
+	$(LATEX) Reference-Manual;\
+	$(LATEX) Reference-Manual)
+
+refman/Reference-Manual.pdf: refman/Reference-Manual.dvi
+	(cd refman; $(PDFLATEX) Reference-Manual.tex)
+
+### Reference Manual (browsable format)
+
+refman/Reference-Manual.html: refman/Reference-Manual.dvi # to ensure bbl file
+	(cd refman; hevea -fix -nosymb -exec xxdate.exe ./Reference-Manual.tex)
+
+refman/html/index.html: refman/Reference-Manual.html $(REFMANPNGFILES) \
+                        refman/cover.html refman/index.html
+	- rm -rf refman/html
+	mkdir refman/html
+	cp $(REFMANPNGFILES) refman/html
+	(cd refman/html; hacha -o toc.html ../Reference-Manual.html)
+	cp refman/cover.html refman/html
+	cp refman/index.html refman/html
+
+######################################################################
+# Tutorial
+######################################################################
+
+tutorial/Tutorial.v.dvi: common/version.tex common/title.tex tutorial/Tutorial.v.tex
+	(cd tutorial; $(LATEX) Tutorial.v)
+
+tutorial/Tutorial.v.pdf: common/version.tex common/title.tex tutorial/Tutorial.v.dvi
+	(cd tutorial; $(PDFLATEX) Tutorial.v.tex)
+
+tutorial/Tutorial.v.html: tutorial/Tutorial.v.tex
+	(cd tutorial; hevea -exec xxdate.exe Tutorial.v)
+
+
+######################################################################
+# FAQ
+######################################################################
+
+faq/faq.v.dvi: common/version.tex common/title.tex faq/faq.v.tex
+	(cd faq;\
+	$(LATEX) faq.v;\
+	$(BIBTEX) faq.v;\
+	$(LATEX) faq.v;\
+	$(LATEX) faq.v)
+
+faq/faq.v.pdf: common/version.tex common/title.tex faq/faq.v.dvi faq/axioms.png
+	(cd faq; $(PDFLATEX) faq.v.tex)
+
+faq/faq.v.html: faq/faq.v.dvi # to ensure faq.v.bbl
+	(cd faq; hevea -fix -nosymb faq.v.tex)
+
+faq/html/index.html: faq/faq.v.html
+	- rm -rf faq/html
+	mkdir faq/html
+	cp faq/interval_discr.v faq/axioms.png faq/html
+	cp faq/faq.v.html faq/html/index.html
+
+######################################################################
+# Standard library
+######################################################################
+
+GLOBDUMP=$(COQTOP)/glob.dump
+
+LIBDIRS=\
+  Logic Bool Arith ZArith Reals \
+  Lists Strings IntMap Sorting \
+  Sets Relations Wellfounded 
+
+$(GLOBDUMP): $(COQDOC)
+	(cd $(COQTOP); $(MAKE) GLOB="-dump-glob $(GLOBDUMP)" coqlib)
+
+### Standard library (browsable html format)
+
+stdlib/index-body.html: $(GLOBDUMP)
+	- rm -rf stdlib/html
+	mkdir stdlib/html
+	(cd stdlib/html;\
+	 $(COQDOC) -q --multi-index --body-only --html --glob-from $(GLOBDUMP)\
+	  -R $(COQTOP)/theories Coq $(COQTOP)/theories/*/*.v)
+	mv stdlib/html/index.html stdlib/index-body.html
+
+stdlib/index-list.html: stdlib/index-list.html.template
+	./stdlib/make-library-index stdlib/index-list.html
+
+stdlib/html/index.html: stdlib/index-list.html stdlib/index-body.html stdlib/index-trailer.html
+	cat $^ > $@
+
+### Standard library (printable format - produces > 350 pages)
+
+stdlib/library.files:
+	(cd stdlib; GALLINA=gallina ./make-library-files)
+
+stdlib/library.coqdoc.tex: stdlib/library.files
+	WHERE=`pwd`/stdlib; cd $(COQTOP)/theories; \
+	$(COQDOC) -q --body-only --latex -o $$WHERE/library.coqdoc.tex \
+         -R `pwd`/$(COQTOP)/theories Coq `cat $$WHERE/library.files`
+
+stdlib/Library.dvi: $(COMMON) stdlib/library.coqdoc.tex stdlib/Library.tex
+	(cd stdlib;\
+	$(LATEX) Library;\
+	$(LATEX) Library)
+
+stdlib/Library.pdf: $(COMMON) stdlib/library.coqdoc.tex stdlib/Library.dvi
+	(cd stdlib; $(PDFLATEX) Library)
+
+######################################################################
+# Install all documentation files
+######################################################################
+
+COQINSTALLPREFIX=
+DOCDIR=/usr/local/share/doc/coq-8.0
+FULLDOCDIR=$(COQINSTALLPREFIX)$(DOCDIR)
+HTMLINSTALLDIR=$(FULLDOCDIR)/html
+PRINTABLEINSTALLDIR=$(FULLDOCDIR)/ps
+
+install-doc: install-meta install-doc-html install-doc-printable
+
+install-meta:
+	mkdir $(DOCDIC)
+	cp LICENCE $(DOCDIC)/LICENCE.doc
+#	cp $(COQTOP)/LICENCE $(COQTOP)/CREDITS $(COQTOP)/COPYRIGHT $(DOCDIC)
+#	cp $(COQTOP)/README $(COQTOP)/CHANGES $(DOCDIC)
+
+install-doc-html: all-html
+	mkdir $(HTMLINSTALLDIR)
+	cp -r refman/html $(HTMLINSTALLDIR)/refman
+	cp -r stdlib/html $(HTMLINSTALLDIR)/stdlib
+	cp -r tutorial/tutorial.html $(HTMLINSTALLDIR)/
+	cp -r faq/html $(HTMLINSTALLDIR)/faq
+
+install-doc-printable: all-pdf all-ps
+	mkdir $(PRINTABLEINSTALLDIR)
+	cp -r refman/Reference-manual.pdf $(PRINTABLEINSTALLDIR)
+	cp -r stdlib/Library.pdf $(PRINTABLEINSTALLDIR)
+	cp -r tutorial/Tutorial.v.pdf $(PRINTABLEINSTALLDIR)/Tutorial.pdf
+	cp -r faq/faq.v.pdf $(PRINTABLEINSTALLDIR)/faq.pdf
+	cp -r refman/Reference-manual.ps $(PRINTABLEINSTALLDIR)
+	cp -r stdlib/Library.ps $(PRINTABLEINSTALLDIR)
+	cp -r tutorial/Tutorial.v.ps $(PRINTABLEINSTALLDIR)/Tutorial.ps
+	cp -r faq/faq.v.ps $(PRINTABLEINSTALLDIR)/faq.ps
diff --git a/doc/README b/doc/README
index 1693b1ca0..14cb6e448 100755
--- a/doc/README
+++ b/doc/README
@@ -5,40 +5,26 @@ V8.0 is divided into the following documents :
 
      * Tutorial.ps: An introduction to the use of the Coq Proof Assistant;
 
-     * Reference-Manual-base.ps:  215 pp., includes
-
-     - the description of Gallina, the language of Coq
-     - the description of the Vernacular, the commands of Coq
-     - the description of each tactic
-     - chapters about Grammar/Syntax extentions and Writing tactics
-     - index on tactics, commands and error messages
-
-     * Reference-Manual-addendum.ps, 75 pp., includes more detailed
-       explanations and examples about the following topics:
-
-     - the extended Cases (C.Cornes)
-     - the Coercions (A. Sa�bi)
-     - the tactic Omega (P. Cr�gut)
-     - the Correctness tactic (J.-C. Filli�tre)
-     - the extraction features (J.-C. Filli�tre and P. Letouzey) 
-     - the tactic Ring (S. Boutin and P. Loiseleur)
-     - the Setoid_replace tactic (C. Renard)
-
-     Index, page and chapter numbers are shared by the two documents, in
-     order to make cross-references possible. There is also a on the ftp
-     server a Postscript file Reference-Manual-all.ps that contains the two
-     documents (base and addendum).
+     * Reference-Manual.ps:
+
+       Base chapters:
+       - the description of Gallina, the language of Coq
+       - the description of the Vernacular, the commands of Coq
+       - the description of each tactic
+       - index on tactics, commands and error messages
+
+       Additional chapters:
+       - the extended Cases (C.Cornes)
+       - the coercions (A. Sa�bi)
+       - the tactic Omega (P. Cr�gut)
+       - the extraction features (J.-C. Filli�tre and P. Letouzey) 
+       - the tactic Ring (S. Boutin and P. Loiseleur)
+       - the Setoid_replace tactic (C. Renard)
+       - etc.
 
      * Library.ps: A description of the Coq standard library;
 
-     * CHANGES: A description of the differences between version 8.0
-       and previous versions
-
      * rectypes.ps : A tutorial on recursive types by Eduardo Gimenez
 
-Documentation is also available in the DVI format (you can get the DVI docs 
-separately or in the tar file all-dvi.docs.tar).
-
-The Reference Manual and the Tutorial are also available in HTML format 
+Documentation is also available in the PDF format and HTML format
 (online at http://coq.inria.fr or by ftp in the file doc-html.tar.gz).
-
diff --git a/doc/common/title.tex b/doc/common/title.tex
index 8e1d1c9c9..51e817cc5 100755
--- a/doc/common/title.tex
+++ b/doc/common/title.tex
@@ -20,7 +20,7 @@
 %To show the top for the toc in html
 \newcommand{\tophtml}{}
 
-\newcommand{\coverpage}[2]{
+\newcommand{\coverpage}[3]{
 \thispagestyle{empty}
 \begin{center}
 \begin{Huge}
@@ -51,12 +51,9 @@ The Coq Proof Assistant\\
 {\large{V\coqversion,
 \printingdate}}\\[20pt]
 %END LATEX
-{\large{\copyright INRIA 1999-2004 ({\Coq} versions 7)}}\\
-{\large{\copyright INRIA 2004-2006 ({\Coq} version 8)}}\\
-{\large{This material may be distributed only subject to the terms and
-conditions set forth in the Open Publication License, v1.0 or later
-(the latest version is presently available at
-\ahrefurl{http://www.opencontent.org/openpub})}}.
+{\large{\copyright INRIA 1999-2004 ({\Coq} versions 7.x)}}\\
+{\large{\copyright INRIA 2004-2006 ({\Coq} versions 8.x)}}\\
+{\large{#3}}
 \end{flushleft}
 %BEGIN LATEX
 \newpage
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index 7b8ed6d10..5fcee708f 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -1,4 +1,8 @@
+\ifx\pdfoutput\undefined   % si on est pas en pdflatex
 \documentclass[a4paper]{article}
+\else
+\documentclass[a4paper,pdftex]{article}
+\fi
 \pagestyle{plain}
 
 % yay les symboles
@@ -10,7 +14,12 @@
 \usepackage{fullpage}
 \usepackage[latin1]{inputenc}
 \usepackage[english]{babel}
-\usepackage{graphics}
+
+\ifx\pdfoutput\undefined   % si on est pas en pdflatex
+  \usepackage[dvips]{graphicx}
+\else
+  \usepackage[pdftex]{graphicx}
+\fi
 
 %\input{../macros.tex}
 
@@ -464,7 +473,14 @@ standard library of {\Coq}. The most interesting ones are
 Here is a summary of the relative strength of these axioms, most
 proofs can be found in directory {\tt Logic} of the standard library.
 
-\includegraphics{axioms}
+%HEVEA\imgsrc{axioms.png}
+%BEGIN LATEX
+\ifx\pdfoutput\undefined   % si on est pas en pdflatex
+\includegraphics[width=1.0\textwidth]{axioms.eps}
+\else
+\includegraphics[width=1.0\textwidth]{axioms.png}
+\fi
+%END LATEX
 
 \Question{What standard axioms are inconsistent with {\Coq}?}
 
@@ -1621,7 +1637,7 @@ Definition R (a b:list nat) := length a < length b.
 \item Prove that this order is well-founded (in fact that all elements in {\tt A} are accessible along {\tt R}).
 
 \begin{coq_example*}
-Lemma Rwf : well_founded (A:=R).
+Lemma Rwf : well_founded R.
 \end{coq_example*}
 
 \item Define the step function (which needs proofs that recursive
@@ -1989,6 +2005,7 @@ This is provable without requiring any axiom because axiom $K$
 directly holds on {\tt nat}. Here is a proof using question \ref{K-nat}.
 
 \begin{coq_example*}
+Require Import Arith.
 Scheme le_ind' := Induction for le Sort Prop.
 Theorem le_uniqueness_proof : forall (n m : nat) (p q : n <= m), p = q.
 Proof.
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index fa909b607..08b527588 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -23,9 +23,9 @@
 
 %\includeonly{RefMan-gal.v,RefMan-ltac.v,RefMan-lib.v,Cases.v}
 
-\input{./version.tex}
-\input{./macros.tex}% extension .tex pour htmlgen
-\input{./title.tex}% extension .tex pour htmlgen
+\input{../common/version.tex}
+\input{../common/macros.tex}% extension .tex pour htmlgen
+\input{../common/title.tex}% extension .tex pour htmlgen
 \input{./headers.tex}% extension .tex pour htmlgen
 
 \begin{document}
@@ -36,6 +36,11 @@
 \tophtml{}
 %BEGIN LATEX
 \coverpage{Reference Manual}{The Coq Development Team}
+  {This material may be distributed only subject to the terms and
+   conditions set forth in the Open Publication License, v1.0 or later
+   (the latest version is presently available at
+   \ahrefurl{http://www.opencontent.org/openpub}).
+   Options A and B of the licence are {\em not} elected.}
 %END LATEX
 
 %\defaultheaders
diff --git a/doc/refman/cover.html b/doc/refman/cover.html
index 2a09ea231..1d2700b1c 100644
--- a/doc/refman/cover.html
+++ b/doc/refman/cover.html
@@ -22,7 +22,7 @@ The Coq Proof Assistant<BR>
 <DIV ALIGN=left>
 <FONT SIZE=4>V7.x � INRIA 1999-2004</FONT><BR>
 <FONT SIZE=4>V8.0 � INRIA 2004-2006</FONT><BR>
-This material may be distributed only subject to the terms and conditions set forth in the Open Publication License, v1.0 or later (the latest version is presently available at <A HREF="http://www.opencontent.org/openpub">http://www.opencontent.org/openpub</A>).
+This material may be distributed only subject to the terms and conditions set forth in the Open Publication License, v1.0 or later (the latest version is presently available at <A HREF="http://www.opencontent.org/openpub">http://www.opencontent.org/openpub</A>). Options A and B are not elected.
 </DIV>
 <BR>
 
diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex
index 58b2dc6df..9fae7495b 100755
--- a/doc/stdlib/Library.tex
+++ b/doc/stdlib/Library.tex
@@ -3,15 +3,18 @@
 \usepackage[latin1]{inputenc}
 \usepackage[T1]{fontenc}
 \usepackage{fullpage}
-\usepackage[noweb]{coqweb}
+\usepackage{coqdoc}
 
-\input{./title}
-\input{./macros}
+\input{../common/version}
+\input{../common/title}
+\input{../common/macros}
 
 \begin{document}
  
 \coverpage{The standard library}%
 {\ }
+{This material is distributed under the terms of the GNU Lesser
+General Public License Version 2.1.}
 
 \tableofcontents
 
@@ -53,7 +56,7 @@ is also a version of this document in HTML format on the WWW, which
 you can access from the \Coq\ home page at
 \texttt{http://coq.inria.fr/library}.
 
-\input{library.coqweb.tex}
+\input{library.coqdoc}
 
 \end{document}
 
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
new file mode 100644
index 000000000..fbed33ccf
--- /dev/null
+++ b/doc/stdlib/index-list.html.template
@@ -0,0 +1,275 @@
+<html>
+
+<head>
+<link rel="stylesheet" href="style.css" type="text/css">
+<title>The Coq Standard Library
+</head>
+
+<body>
+
+<H1>The Coq Standard Library</H1>
+
+Here is a short description of the Coq standard library, which is
+distributed with the system.
+It provides a set of modules directly available 
+through the <tt>Require Import</tt> command.
+<p>
+The standard library is composed of the following subdirectories:
+
+<p>
+
+<dl>
+  <dt> <b>Init</b>:
+       The core library (automatically loaded when starting Coq)
+  <dd> 
+theories/Init/Notations.v
+theories/Init/Datatypes.v
+theories/Init/Logic.v
+theories/Init/Logic_Type.v
+theories/Init/Peano.v
+theories/Init/Specif.v
+theories/Init/Wf.v
+(theories/Init/Prelude.v)
+
+  <dt> <b>Logic</b>:
+       Classical logic and dependent equality
+  <dd>
+theories/Logic/Classical_Pred_Set.v
+theories/Logic/Classical_Pred_Type.v
+theories/Logic/Classical_Prop.v
+theories/Logic/Classical_Type.v
+(theories/Logic/Classical.v)
+theories/Logic/Decidable.v
+theories/Logic/Eqdep_dec.v
+theories/Logic/Eqdep.v
+theories/Logic/JMeq.v
+theories/Logic/RelationalChoice.v
+theories/Logic/ClassicalChoice.v
+theories/Logic/ChoiceFacts.v
+theories/Logic/ClassicalDescription.v
+theories/Logic/ClassicalFacts.v
+theories/Logic/Berardi.v
+theories/Logic/Diaconescu.v
+theories/Logic/Hurkens.v
+theories/Logic/ProofIrrelevance.v
+
+  <dt> <b>Arith</b>:
+       Basic Peano arithmetic
+  <dd> 
+theories/Arith/Le.v
+theories/Arith/Lt.v
+theories/Arith/Plus.v
+theories/Arith/Minus.v
+theories/Arith/Mult.v
+theories/Arith/Gt.v
+theories/Arith/Between.v
+theories/Arith/Peano_dec.v
+theories/Arith/Compare_dec.v
+(theories/Arith/Arith.v)
+theories/Arith/Min.v
+theories/Arith/Max.v
+theories/Arith/Compare.v
+theories/Arith/Div2.v
+theories/Arith/Div.v
+theories/Arith/EqNat.v
+theories/Arith/Euclid.v
+theories/Arith/Even.v
+theories/Arith/Bool_nat.v
+theories/Arith/Factorial.v
+theories/Arith/Wf_nat.v
+
+  <dt> <b>NArith</b>:
+       Binary positive integers
+  <dd> 
+
+theories/NArith/BinPos.v
+theories/NArith/BinNat.v
+(theories/NArith/NArith.v)
+theories/NArith/Pnat.v
+
+  <dt> <b>ZArith</b>:
+       Binary integers
+  <dd> 
+theories/ZArith/BinInt.v
+theories/ZArith/Zorder.v
+theories/ZArith/Zcompare.v
+theories/ZArith/Znat.v
+theories/ZArith/Zmin.v
+theories/ZArith/Zabs.v
+theories/ZArith/Zeven.v
+theories/ZArith/auxiliary.v
+theories/ZArith/ZArith_dec.v
+theories/ZArith/Zbool.v
+theories/ZArith/Zmisc.v
+theories/ZArith/Wf_Z.v
+theories/ZArith/Zhints.v
+(theories/ZArith/ZArith_base.v)
+theories/ZArith/Zcomplements.v
+theories/ZArith/Zsqrt.v
+theories/ZArith/Zpower.v
+theories/ZArith/Zdiv.v
+theories/ZArith/Zlogarithm.v
+(theories/ZArith/ZArith.v)
+theories/ZArith/Zwf.v
+theories/ZArith/Zbinary.v
+theories/ZArith/Znumtheory.v
+
+  <dt> <b>Reals</b>:
+       Formalization of real numbers
+  <dd> 
+theories/Reals/Rdefinitions.v
+theories/Reals/Raxioms.v
+theories/Reals/RIneq.v
+theories/Reals/DiscrR.v
+(theories/Reals/Rbase.v)
+theories/Reals/RList.v
+theories/Reals/Ranalysis.v
+theories/Reals/Rbasic_fun.v
+theories/Reals/Rderiv.v
+theories/Reals/Rfunctions.v
+theories/Reals/Rgeom.v
+theories/Reals/R_Ifp.v
+theories/Reals/Rlimit.v
+theories/Reals/Rseries.v
+theories/Reals/Rsigma.v
+theories/Reals/R_sqr.v
+theories/Reals/Rtrigo_fun.v
+theories/Reals/Rtrigo.v
+theories/Reals/SplitAbsolu.v
+theories/Reals/SplitRmult.v
+theories/Reals/Alembert.v
+theories/Reals/AltSeries.v
+theories/Reals/ArithProp.v
+theories/Reals/Binomial.v
+theories/Reals/Cauchy_prod.v
+theories/Reals/Cos_plus.v
+theories/Reals/Cos_rel.v
+theories/Reals/Exp_prop.v
+theories/Reals/Integration.v
+theories/Reals/MVT.v
+theories/Reals/NewtonInt.v
+theories/Reals/PSeries_reg.v
+theories/Reals/PartSum.v
+theories/Reals/R_sqrt.v
+theories/Reals/Ranalysis1.v
+theories/Reals/Ranalysis2.v
+theories/Reals/Ranalysis3.v
+theories/Reals/Ranalysis4.v
+theories/Reals/Rcomplete.v
+theories/Reals/RiemannInt.v
+theories/Reals/RiemannInt_SF.v
+theories/Reals/Rpower.v
+theories/Reals/Rprod.v
+theories/Reals/Rsqrt_def.v
+theories/Reals/Rtopology.v
+theories/Reals/Rtrigo_alt.v
+theories/Reals/Rtrigo_calc.v
+theories/Reals/Rtrigo_def.v
+theories/Reals/Rtrigo_reg.v
+theories/Reals/SeqProp.v
+theories/Reals/SeqSeries.v
+theories/Reals/Sqrt_reg.v
+(theories/Reals/Reals.v)
+
+  <dt> <b>Bool</b>:
+       Booleans (basic functions and results)
+  <dd> 
+theories/Bool/Bool.v
+theories/Bool/BoolEq.v
+theories/Bool/DecBool.v
+theories/Bool/IfProp.v
+theories/Bool/Sumbool.v
+theories/Bool/Zerob.v
+theories/Bool/Bvector.v
+
+  <dt> <b>Lists</b>:
+       Polymorphic lists, Streams (infinite sequences)
+  <dd> 
+theories/Lists/List.v
+theories/Lists/ListSet.v
+theories/Lists/TheoryList.v
+theories/Lists/Streams.v
+theories/Lists/MonoList.v
+
+  <dt> <b>Sets</b>:
+       Sets (classical, constructive, finite, infinite, powerset,
+            etc.)
+  <dd> 
+theories/Sets/Classical_sets.v
+theories/Sets/Constructive_sets.v
+theories/Sets/Cpo.v
+theories/Sets/Ensembles.v
+theories/Sets/Finite_sets_facts.v
+theories/Sets/Finite_sets.v
+theories/Sets/Image.v
+theories/Sets/Infinite_sets.v
+theories/Sets/Integers.v
+theories/Sets/Multiset.v
+theories/Sets/Partial_Order.v
+theories/Sets/Permut.v
+theories/Sets/Powerset_Classical_facts.v
+theories/Sets/Powerset_facts.v
+theories/Sets/Powerset.v
+theories/Sets/Relations_1_facts.v
+theories/Sets/Relations_1.v
+theories/Sets/Relations_2_facts.v
+theories/Sets/Relations_2.v
+theories/Sets/Relations_3_facts.v
+theories/Sets/Relations_3.v
+theories/Sets/Uniset.v
+
+  <dt> <b>Relations</b>:
+       Relations (definitions and basic results)
+  <dd> 
+theories/Relations/Relation_Definitions.v
+theories/Relations/Relation_Operators.v
+theories/Relations/Relations.v
+theories/Relations/Operators_Properties.v
+theories/Relations/Rstar.v
+theories/Relations/Newman.v
+
+  <dt> <b>Wellfounded</b>:
+       Well-founded Relations
+  <dd> 
+theories/Wellfounded/Disjoint_Union.v
+theories/Wellfounded/Inclusion.v
+theories/Wellfounded/Inverse_Image.v
+theories/Wellfounded/Lexicographic_Exponentiation.v
+theories/Wellfounded/Lexicographic_Product.v
+theories/Wellfounded/Transitive_Closure.v
+theories/Wellfounded/Union.v
+theories/Wellfounded/Wellfounded.v
+theories/Wellfounded/Well_Ordering.v
+
+  <dt> <b>Sorting</b>:
+       Axiomatizations of sorts
+  <dd> 
+theories/Sorting/Heap.v
+theories/Sorting/Permutation.v
+theories/Sorting/Sorting.v
+
+  <dt> <b>Setoids</b>:
+  <dd> 
+theories/Setoids/Setoid.v
+
+  <dt> <b>IntMap</b>:
+       Finite sets/maps as trees indexed by addresses
+  <dd> 
+theories/IntMap/Addr.v
+theories/IntMap/Adist.v
+theories/IntMap/Addec.v
+theories/IntMap/Adalloc.v
+theories/IntMap/Map.v
+theories/IntMap/Fset.v
+theories/IntMap/Mapaxioms.v
+theories/IntMap/Mapiter.v
+theories/IntMap/Mapcanon.v
+theories/IntMap/Mapsubset.v
+theories/IntMap/Lsort.v
+theories/IntMap/Mapfold.v
+theories/IntMap/Mapcard.v
+theories/IntMap/Mapc.v
+theories/IntMap/Maplists.v
+(theories/IntMap/Allmaps.v)
+
+</dl>
diff --git a/doc/stdlib/index-trailer.html b/doc/stdlib/index-trailer.html
new file mode 100644
index 000000000..308b1d01b
--- /dev/null
+++ b/doc/stdlib/index-trailer.html
@@ -0,0 +1,2 @@
+</body>
+</html>
diff --git a/doc/stdlib/make-library-files b/doc/stdlib/make-library-files
new file mode 100755
index 000000000..91e3cc3f4
--- /dev/null
+++ b/doc/stdlib/make-library-files
@@ -0,0 +1,36 @@
+#!/bin/sh
+
+# Needs COQTOP and GALLINA set
+
+# On garde la liste de tous les *.v avec dates dans library.files.ls
+# Si elle a change depuis la derniere fois ou library.files n'existe pas
+# on fabrique des .g (si besoin) et la liste library.files dans 
+# l'ordre de ls -tr des *.vo
+# Ce dernier 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
+
+LIBDIRS="Arith NArith ZArith Reals Logic Bool Lists IntMap Relations Sets Sorting Wellfounded Setoids"
+
+rm -f library.files.ls.tmp
+(cd $COQTOP/theories; find $LIBDIR -name "*.v" -ls) > library.files.ls.tmp
+if ! test -e library.files || ! cmp library.files.ls library.files.ls.tmp; then
+  mv -f library.files.ls.tmp library.files.ls
+  rm -f library.files; touch library.files
+  ABSOLUTE=`pwd`/library.files
+  cd $COQTOP/theories
+  echo $LIBDIRS
+  for rep in $LIBDIRS ; do
+    (cd $rep
+     echo $rep/intro.tex >> $ABSOLUTE
+     VOFILES=`ls -tr *.vo`
+     for file in $VOFILES ; do
+       VF=`basename $file \.vo`
+       if [ \( ! -e $VF.g \) -o \( $VF.v -nt $VF.g \) ] ; then
+          $GALLINA $VF.v
+       fi
+       echo $rep/$VF.g >> $ABSOLUTE
+     done
+    )
+  done
+fi
diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index
new file mode 100755
index 000000000..1da642df3
--- /dev/null
+++ b/doc/stdlib/make-library-index
@@ -0,0 +1,32 @@
+#!/bin/sh
+
+# Instantiate links to library files in index template
+
+FILE=$1
+
+cp -f $FILE.template tmp
+echo -n Building file index-list.prehtml ...
+for i in $COQTOP/theories/*; do
+  d=`basename $i`
+  if [ "$d" != "Num" -a "$d" != "CVS" ]; then
+  for j in $i/*.v; do
+    b=`basename $j .v`
+    rm -f tmp2
+    grep -q theories/$d/$b.v tmp
+    a=$?
+    if [ $a = 0 ]; then
+      sed -e "s/theories\/$d\/$b.v/<a href=\"Coq.$d.$b.html\">$b<\/a>/g" tmp > tmp2
+      mv -f tmp2 tmp
+    else
+      echo Warning: theories/$d/$b.v is missing in the template file
+    fi
+  done
+  fi
+  rm -f tmp2
+  sed -e "s/#$d#//" tmp > tmp2
+  mv -f tmp2 tmp
+done
+a=`grep theories tmp`
+if [ $? = 0 ]; then echo Warning: extra files:; echo $a; fi
+mv tmp $FILE
+echo Done
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index c5b977628..7909e20f7 100755
--- a/doc/tutorial/Tutorial.tex
+++ b/doc/tutorial/Tutorial.tex
@@ -1,16 +1,16 @@
-\documentclass[11pt]{book}
+\documentclass[11pt,a4paper]{book}
 \usepackage[T1]{fontenc}
 \usepackage[latin1]{inputenc}
 \usepackage{pslatex}
 
-\input{./version.tex}
-\input{./macros.tex}
-\input{./title.tex}
+\input{../common/version.tex}
+\input{../common/macros.tex}
+\input{../common/title.tex}
 
 %\makeindex
 
 \begin{document}
-\coverpage{A Tutorial}{G�rard Huet, Gilles Kahn and Christine Paulin-Mohring}
+\coverpage{A Tutorial}{G�rard Huet, Gilles Kahn and Christine Paulin-Mohring}{}
 
 %\tableofcontents