From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- doc/Makefile | 307 ---------------------------- doc/stdlib/Library.tex | 10 +- doc/stdlib/index-list.html.template | 387 +++++++++++++++++++++++------------- doc/stdlib/make-library-files | 2 +- doc/stdlib/make-library-index | 42 ++-- 5 files changed, 278 insertions(+), 470 deletions(-) delete mode 100644 doc/Makefile (limited to 'doc') 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>/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"> - - +The Coq Standard Library @@ -41,6 +40,7 @@ through the Require Import command.

Classical logic and dependent equality
+ 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 Require Import command.

theories/Logic/ProofIrrelevance.v theories/Logic/ProofIrrelevanceFacts.v theories/Logic/ConstructiveEpsilon.v + theories/Logic/Description.v + theories/Logic/Epsilon.v + theories/Logic/IndefiniteDescription.v +
+ +
Bool: + Booleans (basic functions and results) +
+
+ 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
Arith: Basic Peano arithmetic
+ theories/Arith/Arith_base.v theories/Arith/Le.v theories/Arith/Lt.v theories/Arith/Plus.v @@ -86,7 +103,6 @@ through the Require Import command.

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 Require Import command.

theories/NArith/Ndigits.v theories/NArith/Ndist.v theories/NArith/Ndec.v -.
+
ZArith: Binary integers @@ -131,14 +147,19 @@ through the Require Import command.

(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
QArith: @@ -146,72 +167,114 @@ through the Require Import command.

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
- -
Reals: - Formalization of real numbers + +
Numbers: + A modular axiomatic construction for numbers +
+
+ theories/Numbers/NumPrelude.v + theories/Numbers/BigNumPrelude.v + theories/Numbers/NaryFunctions.v +
+ +
+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 +
+ +
+ 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 +
+ +
+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 +
+ +
+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 +
+ +
+ 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 +
+ +
Relations: + Relations (definitions and basic results)
- 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
Sets: @@ -242,51 +305,26 @@ through the Require Import command.

theories/Sets/Uniset.v -
Relations: - Relations (definitions and basic results) -
+
Classes:
- 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
- -
Wellfounded: - Well-founded Relations -
-
- 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 -
- +
Setoids:
theories/Setoids/Setoid.v
-
Bool: - Booleans (basic functions and results) -
-
- 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 -
-
Lists: Polymorphic lists, Streams (infinite sequences)
@@ -296,12 +334,40 @@ through the Require Import command.

theories/Lists/MonoList.v theories/Lists/SetoidList.v theories/Lists/Streams.v + theories/Lists/StreamMemo.v theories/Lists/TheoryList.v theories/Lists/ListTactics.v +
Sorting: + Axiomatizations of sorts +
+
+ theories/Sorting/Heap.v + theories/Sorting/Permutation.v + theories/Sorting/Sorting.v + theories/Sorting/PermutEq.v + theories/Sorting/PermutSetoid.v +
+ +
Wellfounded: + Well-founded Relations +
+
+ 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 +
+
FSets: - Modular implementation of finite sets/maps using lists + Modular implementation of finite sets/maps using lists or + efficient trees
theories/FSets/OrderedType.v @@ -309,67 +375,110 @@ through the Require Import command.

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
-
IntMap: - An implementation of finite sets/maps as trees indexed by addresses -
-
- 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 -
- -
Strings + + +
Reals: + Formalization of real numbers +
+
+ 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)
-
Sorting: - Axiomatizations of sorts +
Program: + Support for dependently-typed programming.
- 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
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:$b: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:$b: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 -- cgit v1.2.3