diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
| commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
| tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /doc | |
| parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) | |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/common/styles/html/simple/header.html | 13 | ||||
| -rwxr-xr-x | doc/stdlib/Library.tex | 4 | ||||
| -rw-r--r-- | doc/stdlib/index-list.html.template | 264 | ||||
| -rw-r--r-- | doc/stdlib/index-trailer.html (renamed from doc/common/styles/html/simple/footer.html) | 0 | ||||
| -rwxr-xr-x | doc/stdlib/make-library-files | 2 | ||||
| -rwxr-xr-x | doc/stdlib/make-library-index | 2 |
6 files changed, 176 insertions, 109 deletions
diff --git a/doc/common/styles/html/simple/header.html b/doc/common/styles/html/simple/header.html deleted file mode 100644 index 14d2f988..00000000 --- a/doc/common/styles/html/simple/header.html +++ /dev/null @@ -1,13 +0,0 @@ -<!DOCTYPE html - PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" - "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="coqdoc.css" type="text/css"/> -<title>The Coq Standard Library</title> -</head> - -<body> - diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex index 61fa253c..f5509c3a 100755 --- a/doc/stdlib/Library.tex +++ b/doc/stdlib/Library.tex @@ -1,6 +1,6 @@ \documentclass[11pt]{report} -\usepackage[latin1]{inputenc} +\usepackage[utf8x]{inputenc} \usepackage[T1]{fontenc} \usepackage{fullpage} \usepackage[color]{../../coqdoc} @@ -61,4 +61,4 @@ you can access from the \Coq\ home page at \end{document} -% $Id: Library.tex 11576 2008-11-10 19:13:15Z msozeau $ +% $Id$ diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 484002c3..7a24846b 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -1,5 +1,17 @@ +<!DOCTYPE html + PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" + "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> -<h1>The Coq Standard Library</h1> +<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"/> +<title>The Coq Standard Library</title> +</head> + +<body> + +<H1>The Coq Standard Library</H1> <p>Here is a short description of the Coq standard library, which is distributed with the system. @@ -36,8 +48,6 @@ through the <tt>Require Import</tt> command.</p> (theories/Logic/Classical.v) theories/Logic/ClassicalFacts.v theories/Logic/Decidable.v - theories/Logic/DecidableType.v - theories/Logic/DecidableTypeEx.v theories/Logic/Eqdep_dec.v theories/Logic/EqdepFacts.v theories/Logic/Eqdep.v @@ -60,6 +70,27 @@ through the <tt>Require Import</tt> command.</p> theories/Logic/FunctionalExtensionality.v </dd> + <dt> <b>Structures</b>: + Algebraic structures (types with equality, with order, ...). + DecidableType* and OrderedType* are there only for compatibility. + </dt> + <dd> + theories/Structures/Equalities.v + theories/Structures/EqualitiesFacts.v + theories/Structures/Orders.v + theories/Structures/OrdersTac.v + theories/Structures/OrdersAlt.v + theories/Structures/OrdersEx.v + theories/Structures/OrdersFacts.v + theories/Structures/OrdersLists.v + theories/Structures/GenericMinMax.v + theories/Structures/DecidableType.v + theories/Structures/DecidableTypeEx.v + theories/Structures/OrderedType.v + theories/Structures/OrderedTypeAlt.v + theories/Structures/OrderedTypeEx.v + </dd> + <dt> <b>Bool</b>: Booleans (basic functions and results) </dt> @@ -90,6 +121,7 @@ through the <tt>Require Import</tt> command.</p> (theories/Arith/Arith.v) theories/Arith/Min.v theories/Arith/Max.v + theories/Arith/MinMax.v theories/Arith/Compare.v theories/Arith/Div2.v theories/Arith/EqNat.v @@ -98,6 +130,7 @@ through the <tt>Require Import</tt> command.</p> theories/Arith/Bool_nat.v theories/Arith/Factorial.v theories/Arith/Wf_nat.v + theories/Arith/NatOrderedType.v </dd> <dt> <b>NArith</b>: @@ -112,6 +145,10 @@ through the <tt>Require Import</tt> command.</p> theories/NArith/Ndigits.v theories/NArith/Ndist.v theories/NArith/Ndec.v + theories/NArith/NOrderedType.v + theories/NArith/Nminmax.v + theories/NArith/POrderedType.v + theories/NArith/Pminmax.v </dd> <dt> <b>ZArith</b>: @@ -143,12 +180,13 @@ through the <tt>Require Import</tt> command.</p> (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 + theories/ZArith/ZOrderedType.v + theories/ZArith/Zdigits.v </dd> <dt> <b>QArith</b>: @@ -165,89 +203,117 @@ through the <tt>Require Import</tt> command.</p> theories/QArith/Qreals.v theories/QArith/Qcanon.v theories/QArith/Qround.v + theories/QArith/QOrderedType.v + theories/QArith/Qminmax.v </dd> <dt> <b>Numbers</b>: - A modular axiomatic construction for numbers + An experimental modular architecture for arithmetic </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> + <dt> <b> Prelude</b>: + <dd> + theories/Numbers/NumPrelude.v + theories/Numbers/BigNumPrelude.v + theories/Numbers/NaryFunctions.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> + <dt> <b> NatInt</b>: + Abstract mixed natural/integer/cyclic arithmetic + <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/NZDiv.v + theories/Numbers/NatInt/NZMulOrder.v + theories/Numbers/NatInt/NZOrder.v + theories/Numbers/NatInt/NZDomain.v + theories/Numbers/NatInt/NZProperties.v + </dd> + </dt> - <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> + <dt> <b> Cyclic</b>: + Abstract and 31-bits-based cyclic arithmetic + <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/Ring31.v + theories/Numbers/Cyclic/Int31/Int31.v + theories/Numbers/Cyclic/ZModulo/ZModulo.v + </dd> + </dt> - <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> + <dt> <b> Natural</b>: + Abstract and 31-bits-words-based natural arithmetic + <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/NMulOrder.v + theories/Numbers/Natural/Abstract/NOrder.v + theories/Numbers/Natural/Abstract/NStrongRec.v + theories/Numbers/Natural/Abstract/NSub.v + theories/Numbers/Natural/Abstract/NDiv.v + theories/Numbers/Natural/Abstract/NProperties.v + theories/Numbers/Natural/Binary/NBinary.v + theories/Numbers/Natural/Peano/NPeano.v + theories/Numbers/Natural/SpecViaZ/NSig.v + theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v + theories/Numbers/Natural/BigN/BigN.v + theories/Numbers/Natural/BigN/Nbasic.v + theories/Numbers/Natural/BigN/NMake.v + theories/Numbers/Natural/BigN/NMake_gen.v + </dd> + </dt> - <dd> + <dt> <b> Integer</b>: + Abstract and concrete (especially 31-bits-words-based) integer arithmetic + <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/ZLt.v + theories/Numbers/Integer/Abstract/ZMul.v + theories/Numbers/Integer/Abstract/ZMulOrder.v + theories/Numbers/Integer/Abstract/ZDivEucl.v + theories/Numbers/Integer/Abstract/ZDivFloor.v + theories/Numbers/Integer/Abstract/ZDivTrunc.v + theories/Numbers/Integer/Abstract/ZProperties.v + theories/Numbers/Integer/Abstract/ZSgnAbs.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/Integer/BigZ/BigZ.v + theories/Numbers/Integer/BigZ/ZMake.v + </dd> + </dt> + + <dt><b> Rational</b>: + Abstract and 31-bits-words-based rational arithmetic + <dd> + theories/Numbers/Rational/SpecViaQ/QSig.v theories/Numbers/Rational/BigQ/BigQ.v theories/Numbers/Rational/BigQ/QMake.v - theories/Numbers/Rational/SpecViaQ/QSig.v - </dd> + </dd> + </dt> + </dt> <dt> <b>Relations</b>: Relations (definitions and basic results) @@ -257,10 +323,6 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v theories/Relations/Relation_Operators.v theories/Relations/Relations.v theories/Relations/Operators_Properties.v -<!-- Deprecated - theories/Relations/Rstar.v - theories/Relations/Newman.v ---> </dd> <dt> <b>Sets</b>: @@ -300,15 +362,13 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v theories/Classes/Morphisms_Relations.v theories/Classes/Equivalence.v theories/Classes/EquivDec.v - theories/Classes/Functions.v theories/Classes/SetoidTactics.v theories/Classes/SetoidClass.v theories/Classes/SetoidDec.v - theories/Classes/SetoidAxioms.v + theories/Classes/RelationPairs.v </dd> <dt> <b>Setoids</b>: - <dd> theories/Setoids/Setoid.v </dd> @@ -319,7 +379,6 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v <dd> theories/Lists/List.v theories/Lists/ListSet.v - theories/Lists/MonoList.v theories/Lists/SetoidList.v theories/Lists/Streams.v theories/Lists/StreamMemo.v @@ -336,6 +395,8 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v theories/Sorting/Sorting.v theories/Sorting/PermutEq.v theories/Sorting/PermutSetoid.v + theories/Sorting/Mergesort.v + theories/Sorting/Sorted.v </dd> <dt> <b>Wellfounded</b>: @@ -352,15 +413,31 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v theories/Wellfounded/Wellfounded.v theories/Wellfounded/Well_Ordering.v </dd> - + + <dt> <b>MSets</b>: + Modular implementation of finite sets using lists or + efficient trees. This is a modernization of FSets. + </dt> + <dd> + theories/MSets/MSetInterface.v + theories/MSets/MSetFacts.v + theories/MSets/MSetDecide.v + theories/MSets/MSetProperties.v + theories/MSets/MSetEqProperties.v + theories/MSets/MSetWeakList.v + theories/MSets/MSetList.v + theories/MSets/MSetAVL.v + theories/MSets/MSetPositive.v + theories/MSets/MSetToFiniteSet.v + (theories/MSets/MSets.v) + </dd> + <dt> <b>FSets</b>: Modular implementation of finite sets/maps using lists or - efficient trees + efficient trees. For sets, please consider the more + modern MSets. </dt> <dd> - theories/FSets/OrderedType.v - theories/FSets/OrderedTypeAlt.v - theories/FSets/OrderedTypeEx.v theories/FSets/FSetInterface.v theories/FSets/FSetBridge.v theories/FSets/FSetFacts.v @@ -369,8 +446,10 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v theories/FSets/FSetEqProperties.v theories/FSets/FSetList.v theories/FSets/FSetWeakList.v - (theories/FSets/FSets.v) + theories/FSets/FSetCompat.v theories/FSets/FSetAVL.v + theories/FSets/FSetPositive.v + (theories/FSets/FSets.v) theories/FSets/FSetToFiniteSet.v theories/FSets/FMapInterface.v theories/FSets/FMapWeakList.v @@ -379,7 +458,6 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v theories/FSets/FMapFacts.v (theories/FSets/FMaps.v) theories/FSets/FMapAVL.v - theories/FSets/FSetFullAVL.v theories/FSets/FMapFullAVL.v </dd> @@ -399,6 +477,8 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v theories/Reals/Raxioms.v theories/Reals/RIneq.v theories/Reals/DiscrR.v + theories/Reals/ROrderedType.v + theories/Reals/Rminmax.v (theories/Reals/Rbase.v) theories/Reals/RList.v theories/Reals/Ranalysis.v diff --git a/doc/common/styles/html/simple/footer.html b/doc/stdlib/index-trailer.html index 308b1d01..308b1d01 100644 --- a/doc/common/styles/html/simple/footer.html +++ b/doc/stdlib/index-trailer.html diff --git a/doc/stdlib/make-library-files b/doc/stdlib/make-library-files index 9516a19f..39cedbec 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 Relations Sets Sorting Wellfounded Setoids Program Classes" +LIBDIRS="Arith NArith ZArith Reals Logic Bool Lists Relations Sets Sorting Wellfounded Setoids Program Classes Numbers" rm -f library.files.ls.tmp (cd $COQSRC/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 04bcff91..c8782e93 100755 --- a/doc/stdlib/make-library-index +++ b/doc/stdlib/make-library-index @@ -7,7 +7,7 @@ FILE=$1 cp -f $FILE.template tmp echo -n Building file index-list.prehtml ... -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" +LIBDIRS="Init Logic Structures Bool Arith NArith ZArith QArith Relations Sets Classes Setoids Lists Sorting Wellfounded MSets 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" for k in $LIBDIRS; do i=theories/$k |