From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta
---
doc/stdlib/Library.tex | 2 +-
doc/stdlib/index-list.html.template | 107 ++++++++++++++++++++++++------------
doc/stdlib/index-trailer.html | 2 +
doc/stdlib/make-library-files | 2 +-
doc/stdlib/make-library-index | 2 +-
5 files changed, 77 insertions(+), 38 deletions(-)
create mode 100644 doc/stdlib/index-trailer.html
(limited to 'doc/stdlib')
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 @@
+
-The Coq Standard Library
+
+
+
+
+The Coq Standard Library
+
+
+
+
+The Coq Standard Library
Here is a short description of the Coq standard library, which is
distributed with the system.
@@ -109,7 +121,6 @@ through the Require Import command.
(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 Require Import command.
theories/Arith/Bool_nat.v
theories/Arith/Factorial.v
theories/Arith/Wf_nat.v
- theories/Arith/NatOrderedType.v
-
- NArith:
+
+ PArith:
Binary positive integers
-
- theories/NArith/BinPos.v
+
+ theories/PArith/BinPosDef.v
+ theories/PArith/BinPos.v
+ theories/PArith/Pnat.v
+ theories/PArith/POrderedType.v
+ (theories/PArith/PArith.v)
+
+
+ NArith:
+ Binary natural numbers
+
+
+ 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)
ZArith:
Binary integers
-
+
+ theories/ZArith/BinIntDef.v
theories/ZArith/BinInt.v
theories/ZArith/Zorder.v
theories/ZArith/Zcompare.v
@@ -160,20 +180,20 @@ through the Require Import command.
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
@@ -198,10 +218,9 @@ through the Require Import command.
Numbers:
An experimental modular architecture for arithmetic
-
-
- - Prelude:
+ - Prelude:
-
+ theories/Numbers/BinNums.v
theories/Numbers/NumPrelude.v
theories/Numbers/BigNumPrelude.v
theories/Numbers/NaryFunctions.v
@@ -209,7 +228,6 @@ through the Require Import command.
- NatInt:
Abstract mixed natural/integer/cyclic arithmetic
-
-
theories/Numbers/NatInt/NZAdd.v
theories/Numbers/NatInt/NZAddOrder.v
@@ -221,11 +239,17 @@ through the Require Import command.
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
+
- - Cyclic:
+
- Cyclic:
Abstract and 31-bits-based cyclic arithmetic
-
-
theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -244,10 +268,10 @@ through the Require Import command.
theories/Numbers/Cyclic/Int31/Int31.v
theories/Numbers/Cyclic/ZModulo/ZModulo.v
+
- - Natural:
+
- Natural:
Abstract and 31-bits-words-based natural arithmetic
-
-
theories/Numbers/Natural/Abstract/NAdd.v
theories/Numbers/Natural/Abstract/NAddOrder.v
@@ -260,6 +284,14 @@ through the Require Import command.
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 Require Import command.
theories/Numbers/Natural/BigN/NMake.v
theories/Numbers/Natural/BigN/NMake_gen.v
+
- Integer:
Abstract and concrete (especially 31-bits-words-based) integer arithmetic
-
-
theories/Numbers/Integer/Abstract/ZAdd.v
theories/Numbers/Integer/Abstract/ZAddOrder.v
@@ -282,11 +314,17 @@ through the Require Import command.
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 Require Import command.
theories/Numbers/Integer/BigZ/BigZ.v
theories/Numbers/Integer/BigZ/ZMake.v
+
- Rational:
Abstract and 31-bits-words-based rational arithmetic
-
-
theories/Numbers/Rational/SpecViaQ/QSig.v
theories/Numbers/Rational/BigQ/BigQ.v
theories/Numbers/Rational/BigQ/QMake.v
-
-
+
+
Relations:
Relations (definitions and basic results)
@@ -344,7 +382,7 @@ through the Require Import command.
theories/Sets/Uniset.v
- Classes:
+ Classes:
theories/Classes/Init.v
theories/Classes/RelationClasses.v
@@ -359,7 +397,7 @@ through the Require Import command.
theories/Classes/RelationPairs.v
- Setoids:
+ Setoids:
theories/Setoids/Setoid.v
@@ -373,7 +411,6 @@ through the Require Import command.
theories/Lists/SetoidList.v
theories/Lists/Streams.v
theories/Lists/StreamMemo.v
- theories/Lists/TheoryList.v
theories/Lists/ListTactics.v
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 @@
+
+
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
--
cgit v1.2.3