diff options
Diffstat (limited to 'doc/stdlib')
| -rwxr-xr-x | doc/stdlib/Library.tex | 2 | ||||
| -rw-r--r-- | doc/stdlib/index-list.html.template | 107 | ||||
| -rw-r--r-- | doc/stdlib/index-trailer.html | 2 | ||||
| -rwxr-xr-x | doc/stdlib/make-library-files | 2 | ||||
| -rwxr-xr-x | doc/stdlib/make-library-index | 2 |
5 files changed, 77 insertions, 38 deletions
diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex index bfd7f3f2..cb32adfc 100755 --- a/doc/stdlib/Library.tex +++ b/doc/stdlib/Library.tex @@ -3,6 +3,7 @@ \usepackage[utf8x]{inputenc} \usepackage[T1]{fontenc} \usepackage{fullpage} +\usepackage{amsfonts} \usepackage[color]{../../coqdoc} \input{../common/version} @@ -61,4 +62,3 @@ you can access from the \Coq\ home page at \end{document} -% $Id: Library.tex 12363 2009-09-28 15:04:07Z letouzey $ diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 541fa1b9..35c13f3b 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. @@ -109,7 +121,6 @@ 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 @@ -118,31 +129,40 @@ 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>: + + <dt> <b>PArith</b>: Binary positive integers </dt> - <dd> - theories/NArith/BinPos.v + <dd> + theories/PArith/BinPosDef.v + theories/PArith/BinPos.v + theories/PArith/Pnat.v + theories/PArith/POrderedType.v + (theories/PArith/PArith.v) + </dd> + + <dt> <b>NArith</b>: + Binary natural numbers + </dt> + <dd> + theories/NArith/BinNatDef.v theories/NArith/BinNat.v - (theories/NArith/NArith.v) - theories/NArith/Pnat.v theories/NArith/Nnat.v 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 + theories/NArith/Ndiv_def.v + theories/NArith/Ngcd_def.v + theories/NArith/Nsqrt_def.v + (theories/NArith/NArith.v) </dd> <dt> <b>ZArith</b>: Binary integers </dt> - <dd> + <dd> + theories/ZArith/BinIntDef.v theories/ZArith/BinInt.v theories/ZArith/Zorder.v theories/ZArith/Zcompare.v @@ -160,20 +180,20 @@ through the <tt>Require Import</tt> command.</p> theories/ZArith/Zhints.v (theories/ZArith/ZArith_base.v) theories/ZArith/Zcomplements.v - theories/ZArith/Zsqrt.v + theories/ZArith/Zsqrt_compat.v theories/ZArith/Zpow_def.v + theories/ZArith/Zpow_alt.v theories/ZArith/Zpower.v theories/ZArith/Zdiv.v + theories/ZArith/Zquot.v + theories/ZArith/Zeuclid.v theories/ZArith/Zlogarithm.v (theories/ZArith/ZArith.v) theories/ZArith/Zgcd_alt.v theories/ZArith/Zwf.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> @@ -198,10 +218,9 @@ through the <tt>Require Import</tt> command.</p> <dt> <b>Numbers</b>: An experimental modular architecture for arithmetic </dt> - <dd> - <dl> - <dt> <b> Prelude</b>:</dt> + <dt> <b> Prelude</b>: <dd> + theories/Numbers/BinNums.v theories/Numbers/NumPrelude.v theories/Numbers/BigNumPrelude.v theories/Numbers/NaryFunctions.v @@ -209,7 +228,6 @@ through the <tt>Require Import</tt> command.</p> <dt> <b> NatInt</b>: Abstract mixed natural/integer/cyclic arithmetic - </dt> <dd> theories/Numbers/NatInt/NZAdd.v theories/Numbers/NatInt/NZAddOrder.v @@ -221,11 +239,17 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/NatInt/NZOrder.v theories/Numbers/NatInt/NZDomain.v theories/Numbers/NatInt/NZProperties.v + theories/Numbers/NatInt/NZParity.v + theories/Numbers/NatInt/NZPow.v + theories/Numbers/NatInt/NZSqrt.v + theories/Numbers/NatInt/NZLog.v + theories/Numbers/NatInt/NZGcd.v + theories/Numbers/NatInt/NZBits.v </dd> + </dt> - <dt> <b> Cyclic</b>: + <dt> <b> Cyclic</b>: Abstract and 31-bits-based cyclic arithmetic - </dt> <dd> theories/Numbers/Cyclic/Abstract/CyclicAxioms.v theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -244,10 +268,10 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Cyclic/Int31/Int31.v theories/Numbers/Cyclic/ZModulo/ZModulo.v </dd> + </dt> - <dt> <b> Natural</b>: + <dt> <b> Natural</b>: Abstract and 31-bits-words-based natural arithmetic - </dt> <dd> theories/Numbers/Natural/Abstract/NAdd.v theories/Numbers/Natural/Abstract/NAddOrder.v @@ -260,6 +284,14 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Natural/Abstract/NStrongRec.v theories/Numbers/Natural/Abstract/NSub.v theories/Numbers/Natural/Abstract/NDiv.v + theories/Numbers/Natural/Abstract/NMaxMin.v + theories/Numbers/Natural/Abstract/NParity.v + theories/Numbers/Natural/Abstract/NPow.v + theories/Numbers/Natural/Abstract/NSqrt.v + theories/Numbers/Natural/Abstract/NLog.v + theories/Numbers/Natural/Abstract/NGcd.v + theories/Numbers/Natural/Abstract/NLcm.v + theories/Numbers/Natural/Abstract/NBits.v theories/Numbers/Natural/Abstract/NProperties.v theories/Numbers/Natural/Binary/NBinary.v theories/Numbers/Natural/Peano/NPeano.v @@ -270,10 +302,10 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Natural/BigN/NMake.v theories/Numbers/Natural/BigN/NMake_gen.v </dd> + </dt> <dt> <b> Integer</b>: Abstract and concrete (especially 31-bits-words-based) integer arithmetic - </dt> <dd> theories/Numbers/Integer/Abstract/ZAdd.v theories/Numbers/Integer/Abstract/ZAddOrder.v @@ -282,11 +314,17 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Integer/Abstract/ZLt.v theories/Numbers/Integer/Abstract/ZMul.v theories/Numbers/Integer/Abstract/ZMulOrder.v + theories/Numbers/Integer/Abstract/ZSgnAbs.v + theories/Numbers/Integer/Abstract/ZMaxMin.v + theories/Numbers/Integer/Abstract/ZParity.v + theories/Numbers/Integer/Abstract/ZPow.v + theories/Numbers/Integer/Abstract/ZGcd.v + theories/Numbers/Integer/Abstract/ZLcm.v + theories/Numbers/Integer/Abstract/ZBits.v + theories/Numbers/Integer/Abstract/ZProperties.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 @@ -294,17 +332,17 @@ through the <tt>Require Import</tt> command.</p> 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 - </dt> <dd> theories/Numbers/Rational/SpecViaQ/QSig.v theories/Numbers/Rational/BigQ/BigQ.v theories/Numbers/Rational/BigQ/QMake.v </dd> - </dl> - </dd> + </dt> + </dt> <dt> <b>Relations</b>: Relations (definitions and basic results) @@ -344,7 +382,7 @@ through the <tt>Require Import</tt> command.</p> theories/Sets/Uniset.v </dd> - <dt> <b>Classes</b>:</dt> + <dt> <b>Classes</b>: <dd> theories/Classes/Init.v theories/Classes/RelationClasses.v @@ -359,7 +397,7 @@ through the <tt>Require Import</tt> command.</p> theories/Classes/RelationPairs.v </dd> - <dt> <b>Setoids</b>:</dt> + <dt> <b>Setoids</b>: <dd> theories/Setoids/Setoid.v </dd> @@ -373,7 +411,6 @@ through the <tt>Require Import</tt> command.</p> theories/Lists/SetoidList.v theories/Lists/Streams.v theories/Lists/StreamMemo.v - theories/Lists/TheoryList.v theories/Lists/ListTactics.v </dd> diff --git a/doc/stdlib/index-trailer.html b/doc/stdlib/index-trailer.html new file mode 100644 index 00000000..308b1d01 --- /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 index 39cedbec..c071c4a2 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 Numbers" +LIBDIRS="Arith PArith 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 c8782e93..8e496fdd 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 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" +LIBDIRS="Init Logic Structures Bool Arith PArith 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 |