Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

5 files changed, 278 insertions, 470 deletions

diff --git a/doc/Makefile b/doc/Makefile
deleted file mode 100644
index 5158fbeb..00000000
--- a/doc/Makefile
+++ /dev/null
@@ -1,307 +0,0 @@
-# Makefile for the Coq documentation
-
-# COQSRC needs to be set to a coq source repository
-
-# To compile documentation, you need the following tools:
-# Dvi: latex (latex2e), bibtex, makeindex
-# Pdf: pdflatex
-# Html: hevea (http://hevea.inria.fr) >= 1.05
-
-include ../config/Makefile
-
-
-LATEX=latex
-BIBTEX=bibtex -min-crossrefs=10
-MAKEINDEX=makeindex
-PDFLATEX=pdflatex
-
-HEVEALIB=/usr/local/lib/hevea:/usr/lib/hevea
-TEXINPUTS=$(HEVEALIB):.:
-
-COQTOP=$(COQSRC)/bin/coqtop
-COQTEX=$(COQSRC)/bin/coq-tex -n 72 -image $(COQTOP) -v -sl -small
-COQDOC=$(COQSRC)/bin/coqdoc
-
-#VERSION=POSITIONNEZ-CETTE-VARIABLE
-
-######################################################################
-### General rules
-######################################################################
-
-all: all-html all-pdf all-ps
-
-all-html:\
-  tutorial/Tutorial.v.html refman/html/index.html \
-  faq/html/index.html stdlib/html/index.html RecTutorial/RecTutorial.v.html
-
-all-pdf:\
-  tutorial/Tutorial.v.pdf refman/Reference-Manual.pdf \
-  faq/FAQ.v.pdf stdlib/Library.pdf RecTutorial/RecTutorial.v.pdf
-
-all-ps:\
-  tutorial/Tutorial.v.ps refman/Reference-Manual.ps \
-  faq/FAQ.v.ps stdlib/Library.ps RecTutorial/RecTutorial.v.ps
-
-refman:\
-  refman/html/index.html refman/Reference-Manual.ps refman/Reference-Manual.pdf
-
-tutorial:\
-  tutorial/Tutorial.v.html tutorial/Tutorial.v.ps tutorial/Tutorial.v.pdf
-
-stdlib:\
-  stdlib/html/index.html stdlib/Library.ps stdlib/Library.pdf
-
-faq:\
-  faq/html/index.html faq/FAQ.v.ps faq/FAQ.v.pdf
-
-rectutorial:\
-  RecTutorial/RecTutorial.v.html \
-  RecTutorial/RecTutorial.v.ps RecTutorial/RecTutorial.v.pdf
-
-######################################################################
-### Implicit rules
-######################################################################
-
-.SUFFIXES: .dvi .tex .v.tex .ps .pdf .eps .png
-
-%.v.tex: %.tex
-	(cd `dirname $<`; $(COQTEX) `basename $<`)
-
-%.ps: %.dvi
-	(cd `dirname $<`; dvips -o `basename $@` `basename $<`)
-
-%.eps: %.png
-	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 
-
-### 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/RefMan-ltac.v.tex \
-  refman/Cases.v.tex refman/Coercion.v.tex refman/Extraction.v.tex \
-  refman/Program.v.tex refman/Omega.v.tex refman/Polynom.v.tex \
-  refman/Setoid.v.tex refman/Helm.tex # refman/Natural.v.tex
-
-REFMANTEXFILES=\
-  refman/headers.sty \
-  refman/Reference-Manual.tex refman/RefMan-pre.tex \
-  refman/RefMan-int.tex refman/RefMan-pro.tex \
-  refman/RefMan-com.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
-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.tex
-	(cd refman; $(PDFLATEX) Reference-Manual.tex)
-
-### Reference Manual (browsable format)
-
-refman/Reference-Manual.html: refman/headers.hva refman/Reference-Manual.dvi # to ensure bbl file
-	(cd refman; hevea -fix -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/menu.html refman/html
-	cp refman/index.html refman/html
-
-refman-quick:
-	(cd refman; \
-	 $(PDFLATEX) Reference-Manual.tex; \
-	 hevea -fix -exec xxdate.exe ./Reference-Manual.tex)
-
-
-######################################################################
-# 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 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=$(COQSRC)/glob.dump
-
-LIBDIRS= Logic Bool Arith ZArith QArith Reals Lists Sets Relations Sorting Wellfounded IntMap FSets
-
-### Standard library (browsable html format)
-
-stdlib/index-body.html: $(GLOBDUMP)
-	- rm -rf stdlib/html
-	mkdir stdlib/html
-	(cd stdlib/html;\
-	 $(COQDOC) -q --multi-index --html --glob-from $(GLOBDUMP)\
-	  -R $(COQSRC)/theories Coq $(COQSRC)/theories/*/*.v)
-	mv stdlib/html/index.html stdlib/index-body.html
-
-stdlib/index-list.html: stdlib/index-list.html.template
-	COQTOP=$(COQSRC) ./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 stdlib/index-list.html > $@
-	sed -n -e '/<table>/,/<\/table>/p' stdlib/index-body.html >> $@
-	cat stdlib/index-trailer.html >> $@
-
-### Standard library (printable format - produces > 350 pages)
-
-stdlib/Library.coqdoc.tex: 
-	(for dir in $(LIBDIRS) ; do \
-	  $(COQDOC) -q --gallina --body-only --latex --stdout \
-	    --coqlib_path $(COQSRC) \
-            -R $(COQSRC)/theories Coq "$(COQSRC)/theories/$$dir/"*.v >> $@ ; done)
-
-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)
-
-######################################################################
-# Tutorial on inductive types
-######################################################################
-
-RecTutorial/RecTutorial.v.dvi: common/version.tex common/title.tex RecTutorial/RecTutorial.v.tex
-	(cd RecTutorial;\
-	 $(LATEX) RecTutorial.v;\
-	 $(BIBTEX) RecTutorial.v;\
-	 $(LATEX) RecTutorial.v;\
-	 $(LATEX) RecTutorial.v)
-
-RecTutorial/RecTutorial.v.pdf: common/version.tex common/title.tex RecTutorial/RecTutorial.v.dvi
-	(cd RecTutorial; $(PDFLATEX) RecTutorial.v.tex)
-
-RecTutorial/RecTutorial.v.html: RecTutorial/RecTutorial.v.tex
-	(cd RecTutorial; hevea -exec xxdate.exe RecTutorial.v)
-
-
-######################################################################
-# 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 $(COQSRC)/LICENCE $(COQSRC)/CREDITS $(COQSRC)/COPYRIGHT $(DOCDIC)
-#	cp $(COQSRC)/README $(COQSRC)/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 RecTutorial/RecTutorial.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 RecTutorial/RecTutorial.v.pdf $(PRINTABLEINSTALLDIR)/RecTutorial.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 RecTutorial/RecTutorial.v.ps $(PRINTABLEINSTALLDIR)/RecTutorial.ps
-	cp -r faq/FAQ.v.ps $(PRINTABLEINSTALLDIR)/FAQ.ps
diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex
index 598943a4..f9764bea 100755
--- a/doc/stdlib/Library.tex
+++ b/doc/stdlib/Library.tex
@@ -3,7 +3,7 @@
 \usepackage[latin1]{inputenc}
 \usepackage[T1]{fontenc}
 \usepackage{fullpage}
-\usepackage{coqdoc}
+\usepackage{../../coqdoc}
 
 \input{../common/version}
 \input{../common/title}
@@ -43,8 +43,10 @@ The standard library is composed of the following subdirectories:
   \item[Sorting] Sorted list (basic definitions and heapsort
                  correctness). 
   \item[Wellfounded] Well-founded relations (basic results).
-  \item[IntMap]       Representation of finite sets by an efficient
-                     structure of map (trees indexed by binary integers).
+  \item[Program] Tactics to deal with dependently-typed programs and
+    their proofs.
+  \item[Classes] Standard type class instances on relations and
+    Coq part of the setoid rewriting tactic.
 \end{description}
 
 
@@ -59,4 +61,4 @@ you can access from the \Coq\ home page at
 
 \end{document}
 
-% $Id: Library.tex 9245 2006-10-17 12:53:34Z notin $ 
+% $Id: Library.tex 11091 2008-06-10 18:24:52Z notin $ 
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 81ab034b..5e95a692 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -3,10 +3,9 @@
     "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
 
 <html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en">
-
 <head>
 <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-15"/>
-<link rel="stylesheet" href="css/context.css" type="text/css">
+<link rel="stylesheet" href="css/context.css" type="text/css"/>
 <title>The Coq Standard Library</title>
 </head>
 
@@ -41,6 +40,7 @@ through the <tt>Require Import</tt> command.</p>
       Classical logic and dependent equality
   </dt>
   <dd>
+    theories/Logic/SetIsType.v
     theories/Logic/Classical_Pred_Set.v
     theories/Logic/Classical_Pred_Type.v
     theories/Logic/Classical_Prop.v
@@ -66,12 +66,29 @@ through the <tt>Require Import</tt> command.</p>
     theories/Logic/ProofIrrelevance.v
     theories/Logic/ProofIrrelevanceFacts.v
     theories/Logic/ConstructiveEpsilon.v
+    theories/Logic/Description.v
+    theories/Logic/Epsilon.v
+    theories/Logic/IndefiniteDescription.v
+  </dd>
+    
+  <dt> <b>Bool</b>:
+       Booleans (basic functions and results)
+  </dt>
+  <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
   </dd>
     
   <dt> <b>Arith</b>:
     Basic Peano arithmetic
   </dt>
   <dd> 
+    theories/Arith/Arith_base.v
     theories/Arith/Le.v
     theories/Arith/Lt.v
     theories/Arith/Plus.v
@@ -86,7 +103,6 @@ through the <tt>Require Import</tt> command.</p>
     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
@@ -107,7 +123,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/NArith/Ndigits.v
     theories/NArith/Ndist.v
     theories/NArith/Ndec.v
-.  </dd>
+  </dd>
 
   <dt> <b>ZArith</b>:
        Binary integers
@@ -131,14 +147,19 @@ through the <tt>Require Import</tt> command.</p>
     (theories/ZArith/ZArith_base.v)
     theories/ZArith/Zcomplements.v
     theories/ZArith/Zsqrt.v
+    theories/ZArith/Zpow_def.v
     theories/ZArith/Zpower.v
     theories/ZArith/Zdiv.v
     theories/ZArith/Zlogarithm.v
     (theories/ZArith/ZArith.v)
+    theories/ZArith/Zgcd_alt.v
     theories/ZArith/Zwf.v
     theories/ZArith/Zbinary.v
     theories/ZArith/Znumtheory.v
     theories/ZArith/Int.v
+    theories/ZArith/ZOdiv_def.v
+    theories/ZArith/ZOdiv.v
+    theories/ZArith/Zpow_facts.v
   </dd>
 
   <dt> <b>QArith</b>:
@@ -146,72 +167,114 @@ through the <tt>Require Import</tt> command.</p>
   </dt>
   <dd>
     theories/QArith/QArith_base.v
+    theories/QArith/Qabs.v
+    theories/QArith/Qpower.v
     theories/QArith/Qreduction.v
     theories/QArith/Qring.v
+    theories/QArith/Qfield.v
     (theories/QArith/QArith.v)
     theories/QArith/Qreals.v
     theories/QArith/Qcanon.v
+    theories/QArith/Qround.v
   </dd>
-    
-  <dt> <b>Reals</b>:
-    Formalization of real numbers
+
+  <dt> <b>Numbers</b>: 
+    A modular axiomatic construction for numbers
+  </dt>
+  <dd>
+  theories/Numbers/NumPrelude.v
+  theories/Numbers/BigNumPrelude.v
+  theories/Numbers/NaryFunctions.v
+  </dd>
+  
+  <dd>
+theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+theories/Numbers/Cyclic/Abstract/NZCyclic.v
+theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
+theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
+theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
+theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
+theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
+theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
+theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
+theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
+theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
+theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
+theories/Numbers/Cyclic/Int31/Cyclic31.v
+theories/Numbers/Cyclic/Int31/Int31.v
+theories/Numbers/Cyclic/ZModulo/ZModulo.v
+  </dd>
+
+  <dd>
+    theories/Numbers/Integer/Abstract/ZAdd.v
+theories/Numbers/Integer/Abstract/ZAddOrder.v
+theories/Numbers/Integer/Abstract/ZAxioms.v
+theories/Numbers/Integer/Abstract/ZBase.v
+theories/Numbers/Integer/Abstract/ZDomain.v
+theories/Numbers/Integer/Abstract/ZLt.v
+theories/Numbers/Integer/Abstract/ZMul.v
+theories/Numbers/Integer/Abstract/ZMulOrder.v
+theories/Numbers/Integer/BigZ/BigZ.v
+theories/Numbers/Integer/BigZ/ZMake.v
+theories/Numbers/Integer/Binary/ZBinary.v
+theories/Numbers/Integer/NatPairs/ZNatPairs.v
+theories/Numbers/Integer/SpecViaZ/ZSig.v
+theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+  </dd>
+
+  <dd>
+theories/Numbers/NatInt/NZAdd.v
+theories/Numbers/NatInt/NZAddOrder.v
+theories/Numbers/NatInt/NZAxioms.v
+theories/Numbers/NatInt/NZBase.v
+theories/Numbers/NatInt/NZMul.v
+theories/Numbers/NatInt/NZMulOrder.v
+theories/Numbers/NatInt/NZOrder.v
+  </dd>
+
+  <dd>
+theories/Numbers/Natural/Abstract/NAdd.v
+theories/Numbers/Natural/Abstract/NAddOrder.v
+theories/Numbers/Natural/Abstract/NAxioms.v
+theories/Numbers/Natural/Abstract/NBase.v
+theories/Numbers/Natural/Abstract/NDefOps.v
+theories/Numbers/Natural/Abstract/NIso.v
+theories/Numbers/Natural/Abstract/NMul.v
+theories/Numbers/Natural/Abstract/NMulOrder.v
+theories/Numbers/Natural/Abstract/NOrder.v
+theories/Numbers/Natural/Abstract/NStrongRec.v
+theories/Numbers/Natural/Abstract/NSub.v
+theories/Numbers/Natural/BigN/BigN.v
+theories/Numbers/Natural/BigN/Nbasic.v
+theories/Numbers/Natural/BigN/NMake.v
+theories/Numbers/Natural/Binary/NBinary.v
+theories/Numbers/Natural/Binary/NBinDefs.v
+theories/Numbers/Natural/Peano/NPeano.v
+theories/Numbers/Natural/SpecViaZ/NSig.v
+theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+  </dd>
+
+  <dd>
+    theories/Numbers/Rational/BigQ/BigQ.v
+    theories/Numbers/Rational/BigQ/Q0Make.v
+    theories/Numbers/Rational/BigQ/QbiMake.v
+    theories/Numbers/Rational/BigQ/QifMake.v
+    theories/Numbers/Rational/BigQ/QMake_base.v
+    theories/Numbers/Rational/BigQ/QpMake.v
+    theories/Numbers/Rational/BigQ/QvMake.v
+    theories/Numbers/Rational/SpecViaQ/QSig.v
+  </dd>
+  
+  <dt> <b>Relations</b>:
+       Relations (definitions and basic results)
   </dt>
   <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/LegacyRfield.v
-    theories/Reals/Rpow_def.v
-    (theories/Reals/Reals.v)
+    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
   </dd>
     
   <dt> <b>Sets</b>:
@@ -242,51 +305,26 @@ through the <tt>Require Import</tt> command.</p>
     theories/Sets/Uniset.v
   </dd>
     
-  <dt> <b>Relations</b>:
-       Relations (definitions and basic results)
-  </dt>
+  <dt> <b>Classes</b>:
   <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
+    theories/Classes/Init.v
+    theories/Classes/RelationClasses.v
+    theories/Classes/Morphisms.v
+    theories/Classes/Morphisms_Prop.v
+    theories/Classes/Morphisms_Relations.v
+    theories/Classes/Equivalence.v
+    theories/Classes/EquivDec.v
+    theories/Classes/SetoidTactics.v
+    theories/Classes/SetoidClass.v
+    theories/Classes/SetoidDec.v
+    theories/Classes/SetoidAxioms.v
   </dd>
-    
-  <dt> <b>Wellfounded</b>:
-       Well-founded Relations
-  </dt>
-  <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
-  </dd>
-    
+
   <dt> <b>Setoids</b>:
   <dd> 
     theories/Setoids/Setoid.v
   </dd>
     
-  <dt> <b>Bool</b>:
-       Booleans (basic functions and results)
-  </dt>
-  <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
-  </dd>
-    
   <dt> <b>Lists</b>:
     Polymorphic lists, Streams (infinite sequences)
   </dt>
@@ -296,12 +334,40 @@ through the <tt>Require Import</tt> command.</p>
     theories/Lists/MonoList.v
     theories/Lists/SetoidList.v
     theories/Lists/Streams.v
+    theories/Lists/StreamMemo.v
     theories/Lists/TheoryList.v
     theories/Lists/ListTactics.v
   </dd>
 
+  <dt> <b>Sorting</b>:
+    Axiomatizations of sorts
+  </dt>
+  <dd> 
+    theories/Sorting/Heap.v
+    theories/Sorting/Permutation.v
+    theories/Sorting/Sorting.v
+    theories/Sorting/PermutEq.v
+    theories/Sorting/PermutSetoid.v
+  </dd>
+
+  <dt> <b>Wellfounded</b>:
+       Well-founded Relations
+  </dt>
+  <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
+  </dd>
+    
   <dt> <b>FSets</b>:
-    Modular implementation of finite sets/maps using lists
+    Modular implementation of finite sets/maps using lists or
+    efficient trees
   </dt>
   <dd>
     theories/FSets/OrderedType.v
@@ -309,67 +375,110 @@ through the <tt>Require Import</tt> command.</p>
     theories/FSets/OrderedTypeEx.v
     theories/FSets/FSetInterface.v
     theories/FSets/FSetBridge.v
+    theories/FSets/FSetFacts.v
+    theories/FSets/FSetDecide.v
     theories/FSets/FSetProperties.v
     theories/FSets/FSetEqProperties.v
     theories/FSets/FSetList.v
+    theories/FSets/FSetWeakList.v
     (theories/FSets/FSets.v)
-    theories/FSets/FSetFacts.v
     theories/FSets/FSetAVL.v
     theories/FSets/FSetToFiniteSet.v
-    theories/FSets/FSetWeakProperties.v
-    theories/FSets/FSetWeakInterface.v
-    theories/FSets/FSetWeakFacts.v
-    theories/FSets/FSetWeakList.v
-    theories/FSets/FSetWeak.v
     theories/FSets/FMapInterface.v
+    theories/FSets/FMapWeakList.v
     theories/FSets/FMapList.v
     theories/FSets/FMapPositive.v
-    theories/FSets/FMapIntMap.v
     theories/FSets/FMapFacts.v
     (theories/FSets/FMaps.v)
     theories/FSets/FMapAVL.v
-    theories/FSets/FMapWeakInterface.v
-    theories/FSets/FMapWeakList.v
-    theories/FSets/FMapWeak.v
-    theories/FSets/FMapWeakFacts.v
+    theories/FSets/FSetFullAVL.v
+    theories/FSets/FMapFullAVL.v
   </dd>
 
-  <dt> <b>IntMap</b>:
-    An implementation of finite sets/maps as trees indexed by addresses
-  </dt>
-  <dd> 
-    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
-  </dd>
-    
-  <dt> <b>Strings</b>
+<!--  <dt> <b>Strings</b>
     Implementation of string as list of ascii characters
   </dt>
   <dd>
     theories/Strings/Ascii.v
     theories/Strings/String.v
+  </dd> -->
+    
+  <dt> <b>Reals</b>:
+    Formalization of real numbers
+  </dt>
+  <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/Rpow_def.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/Rlogic.v
+    theories/Reals/LegacyRfield.v
+    (theories/Reals/Reals.v)
   </dd>
     
-  <dt> <b>Sorting</b>:
-    Axiomatizations of sorts
+  <dt> <b>Program</b>:
+    Support for dependently-typed programming.
   </dt>
   <dd> 
-    theories/Sorting/Heap.v
-    theories/Sorting/Permutation.v
-    theories/Sorting/Sorting.v
-    theories/Sorting/PermutEq.v
-    theories/Sorting/PermutSetoid.v
+    theories/Program/Basics.v
+    theories/Program/Wf.v
+    theories/Program/Subset.v
+    theories/Program/Equality.v
+    theories/Program/Tactics.v
+    theories/Program/Utils.v
+    theories/Program/Syntax.v
+    theories/Program/Program.v
+    theories/Program/FunctionalExtensionality.v
+    theories/Program/Combinators.v
   </dd>
 
 </dl>
diff --git a/doc/stdlib/make-library-files b/doc/stdlib/make-library-files
index 91e3cc3f..add14a13 100755
--- a/doc/stdlib/make-library-files
+++ b/doc/stdlib/make-library-files
@@ -10,7 +10,7 @@
 # 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"
+LIBDIRS="Arith NArith ZArith Reals Logic Bool Lists Relations Sets Sorting Wellfounded Setoids Program Classes"
 
 rm -f library.files.ls.tmp
 (cd $COQTOP/theories; find $LIBDIR -name "*.v" -ls) > library.files.ls.tmp
diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index
index ddbcd09f..04bcff91 100755
--- a/doc/stdlib/make-library-index
+++ b/doc/stdlib/make-library-index
@@ -7,27 +7,31 @@ FILE=$1
 cp -f $FILE.template tmp
 echo -n Building file index-list.prehtml ...
 
-for i in ../theories/*; do
-    echo $i
+LIBDIRS="Init Logic Bool Arith NArith ZArith QArith Relations Sets Classes Setoids Lists Sorting Wellfounded FSets Reals Program Numbers Numbers/Natural/Abstract Numbers/Natural/Peano Numbers/Natural/Binary Numbers/Natural/BigN Numbers/Natural/SpecViaZ Numbers/Integer/Abstract Numbers/Integer/NatPairs Numbers/Integer/Binary Numbers/Integer/SpecViaZ Numbers/Integer/BigZ Numbers/NatInt Numbers/Cyclic/Abstract Numbers/Cyclic/Int31 Numbers/Cyclic/ZModulo Numbers/Cyclic/DoubleCyclic Numbers/Rational/BigQ Numbers/Rational/SpecViaQ Strings" 
 
-  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
+for k in $LIBDIRS; do
+    i=theories/$k
+    echo $i
+    
+    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/$k/$b.v tmp
+	    a=$?
+	    if [ $a = 0 ]; then
+		p=`echo $k | sed 's:/:.:g'`
+		sed -e "s:theories/$k/$b.v:<a href=\"Coq.$p.$b.html\">$b</a>:g" tmp > tmp2
+		mv -f tmp2 tmp
+	    else
+		echo Warning: theories/$k/$b.v is missing in the template file
+	    fi
+	done
     fi
-  done
-  fi
-  rm -f tmp2
-  sed -e "s/#$d#//" tmp > tmp2
-  mv -f tmp2 tmp
+    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