diff options
| author |  Stephane Glondu <steph@glondu.net> | 2012-06-04 12:07:52 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:07:52 +0200 |
| commit | 61dc740ed1c3780cccaec00d059a28f0d31d0052 (patch) | |
| tree | d88d05baf35b9b09a034233300f35a694f9fa6c2 /doc/stdlib | |
| parent | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff) | |
Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2
Diffstat (limited to 'doc/stdlib')
| -rw-r--r-- | doc/stdlib/hidden-files | 0 | ||||
| -rw-r--r-- | doc/stdlib/index-list.html.template | 36 | ||||
| -rw-r--r-- | doc/stdlib/index-trailer.html | 2 | ||||
| -rwxr-xr-x | doc/stdlib/make-library-index | 34 |
4 files changed, 49 insertions, 23 deletions
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files new file mode 100644 index 00000000..e69de29b --- /dev/null +++ b/doc/stdlib/hidden-files diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 35c13f3b..0ee101c8 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -1,17 +1,5 @@ -<!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="css/context.css" type="text/css"/> -<title>The Coq Standard Library</title> -</head> - -<body> - -<H1>The Coq Standard Library</H1> +<h1>The Coq Standard Library</h1> <p>Here is a short description of the Coq standard library, which is distributed with the system. @@ -68,6 +56,7 @@ through the <tt>Require Import</tt> command.</p> theories/Logic/Epsilon.v theories/Logic/IndefiniteDescription.v theories/Logic/FunctionalExtensionality.v + theories/Logic/ExtensionalityFacts.v </dd> <dt> <b>Structures</b>: @@ -184,6 +173,8 @@ through the <tt>Require Import</tt> command.</p> theories/ZArith/Zpow_def.v theories/ZArith/Zpow_alt.v theories/ZArith/Zpower.v + theories/ZArith/ZOdiv_def.v + theories/ZArith/ZOdiv.v theories/ZArith/Zdiv.v theories/ZArith/Zquot.v theories/ZArith/Zeuclid.v @@ -414,6 +405,16 @@ through the <tt>Require Import</tt> command.</p> theories/Lists/ListTactics.v </dd> + <dt> <b>Vectors</b>: + Dependent datastructures storing their length + </dt> + <dd> + theories/Vectors/Fin.v + theories/Vectors/VectorDef.v + theories/Vectors/VectorSpec.v + (theories/Vectors/Vector.v) + </dd> + <dt> <b>Sorting</b>: Axiomatizations of sorts </dt> @@ -454,7 +455,9 @@ through the <tt>Require Import</tt> command.</p> theories/MSets/MSetEqProperties.v theories/MSets/MSetWeakList.v theories/MSets/MSetList.v + theories/MSets/MSetGenTree.v theories/MSets/MSetAVL.v + theories/MSets/MSetRBT.v theories/MSets/MSetPositive.v theories/MSets/MSetToFiniteSet.v (theories/MSets/MSets.v) @@ -576,4 +579,11 @@ through the <tt>Require Import</tt> command.</p> theories/Program/Combinators.v </dd> + <dt> <b>Unicode</b>: + Unicode-based notations + </dt> + <dd> + theories/Unicode/Utf8_core.v + theories/Unicode/Utf8.v + </dd> </dl> diff --git a/doc/stdlib/index-trailer.html b/doc/stdlib/index-trailer.html deleted file mode 100644 index 308b1d01..00000000 --- a/doc/stdlib/index-trailer.html +++ /dev/null @@ -1,2 +0,0 @@ -</body> -</html> diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index index 8e496fdd..1a70567f 100755 --- a/doc/stdlib/make-library-index +++ b/doc/stdlib/make-library-index @@ -3,37 +3,55 @@ # Instantiate links to library files in index template FILE=$1 +HIDDEN=$2 cp -f $FILE.template tmp echo -n Building file index-list.prehtml ... -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" +#LIBDIRS="Init Logic Structures Bool Arith PArith NArith ZArith QArith Relations Sets Classes Setoids Lists Vectors 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=`find theories/* -type d | sed -e "s:^theories/::"` for k in $LIBDIRS; do i=theories/$k echo $i d=`basename $i` - if [ "$d" != "Num" -a "$d" != "CVS" ]; then + if [ "$d" != "CVS" ]; then + ls $i | grep -q \.v'$' + if [ $? = 0 ]; then for j in $i/*.v; do b=`basename $j .v` rm -f tmp2 grep -q theories/$k/$b.v tmp a=$? + grep -q theories/$k/$b.v $HIDDEN + h=$? 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 + if [ $h = 0 ]; then + echo Error: $FILE and $HIDDEN both mention theories/$k/$b.v; exit 1 + else + 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 + fi else - echo Warning: theories/$k/$b.v is missing in the template file - fi + if [ $h = 0 ]; then + echo Error: theories/$k/$b.v is missing in the template file + exit 1 + else + echo Error: none of $FILE and $HIDDEN mention theories/$k/$b.v + exit 1 + fi + + fi done + fi 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 +if [ $? = 0 ]; then echo Error: extra files:; echo $a; exit 1; fi mv tmp $FILE echo Done |