aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/stdlib/index-list.html.template
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-11-28 18:07:28 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-11-28 18:07:28 +0000
commitc6d34ae80622b409733776c3cc4ecf5fce6a8378 (patch)
tree2e7626809950d881f9bd2446815d9acf358c7fff /doc/stdlib/index-list.html.template
parent109e85dee481b9a00e6c27648ea62fc4048b0208 (diff)
Ajout de l'axiomatisation des entiers à la documentation de la librairie standard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10343 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/stdlib/index-list.html.template')
-rw-r--r--doc/stdlib/index-list.html.template69
1 files changed, 64 insertions, 5 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 65d69a1d8..ba306b887 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -65,6 +65,9 @@ through the <tt>Require Import</tt> command.</p>
theories/Logic/ProofIrrelevance.v
theories/Logic/ProofIrrelevanceFacts.v
theories/Logic/ConstructiveEpsilon.v
+ theories/Logic/Description.v
+ theories/Logic/Epsilon.v
+ theories/Logic/IndefiniteDescription.v
</dd>
<dt> <b>Bool</b>:
@@ -119,7 +122,7 @@ through the <tt>Require Import</tt> command.</p>
theories/NArith/Ndigits.v
theories/NArith/Ndist.v
theories/NArith/Ndec.v
-. </dd>
+ </dd>
<dt> <b>ZArith</b>:
Binary integers
@@ -152,6 +155,9 @@ through the <tt>Require Import</tt> command.</p>
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
</dd>
<dt> <b>QArith</b>:
@@ -167,9 +173,54 @@ through the <tt>Require Import</tt> command.</p>
(theories/QArith/QArith.v)
theories/QArith/Qreals.v
theories/QArith/Qcanon.v
+ theories/QArith/Qround.v
</dd>
-
-
+
+ <dt> <b>Numbers</b>:
+ A modular axiomatic construction for numbers
+ </dt>
+ <dd>
+ theories/Numbers/NumPrelude.v
+ theories/Numbers/QRewrite.v
+ theories/Numbers/NatInt/NZBase.v
+ theories/Numbers/NatInt/NZAxioms.v
+ theories/Numbers/NatInt/NZPlus.v
+ theories/Numbers/NatInt/NZTimes.v
+ theories/Numbers/NatInt/NZOrder.v
+ theories/Numbers/NatInt/NZTimesOrder.v
+ theories/Numbers/NatInt/NZPlusOrder.v
+ </dd>
+
+ <dd>
+ theories/Numbers/Natural/Abstract/NOrder.v
+ theories/Numbers/Natural/Abstract/NPlus.v
+ theories/Numbers/Natural/Abstract/NMinus.v
+ theories/Numbers/Natural/Abstract/NTimesOrder.v
+ theories/Numbers/Natural/Abstract/NPlusOrder.v
+ theories/Numbers/Natural/Abstract/NIso.v
+ theories/Numbers/Natural/Abstract/NStrongRec.v
+ theories/Numbers/Natural/Abstract/NBase.v
+ theories/Numbers/Natural/Abstract/NAxioms.v
+ theories/Numbers/Natural/Abstract/NTimes.v
+ theories/Numbers/Natural/Abstract/NDefOps.v
+ theories/Numbers/Natural/Peano/NPeano.v
+ theories/Numbers/Natural/Binary/NBinDefs.v
+ theories/Numbers/Natural/Binary/NBinary.v
+ </dd>
+
+ <dd>
+ theories/Numbers/Integer/Abstract/ZPlus.v
+ theories/Numbers/Integer/Abstract/ZPlusOrder.v
+ theories/Numbers/Integer/Abstract/ZLt.v
+ theories/Numbers/Integer/Abstract/ZDomain.v
+ theories/Numbers/Integer/Abstract/ZAxioms.v
+ theories/Numbers/Integer/Abstract/ZTimes.v
+ theories/Numbers/Integer/Abstract/ZBase.v
+ theories/Numbers/Integer/Abstract/ZTimesOrder.v
+ theories/Numbers/Integer/Binary/ZBinary.v
+ theories/Numbers/Integer/NatPairs/ZNatPairs.v
+ </dd>
+
<dt> <b>Relations</b>:
Relations (definitions and basic results)
</dt>
@@ -213,6 +264,8 @@ through the <tt>Require Import</tt> command.</p>
<dt> <b>Setoids</b>:
<dd>
theories/Setoids/Setoid.v
+ theories/Setoids/Setoid_Prop.v
+ theories/Setoids/Setoid_tac.v
</dd>
<dt> <b>Lists</b>:
@@ -385,7 +438,7 @@ through the <tt>Require Import</tt> command.</p>
theories/Ints/BigN.v
theories/Ints/BigZ.v
theories/Ints/Int31.v
- theories/Ints/Tactic.v
+ theories/Ints/Z/ZAux.v
theories/Ints/num/GenAdd.v
theories/Ints/num/GenBase.v
theories/Ints/num/GenDivn1.v
@@ -396,10 +449,16 @@ through the <tt>Require Import</tt> command.</p>
theories/Ints/num/GenSub.v
theories/Ints/num/Nbasic.v
theories/Ints/num/NMake.v
- theories/Ints/num/QMake.v
theories/Ints/num/ZMake.v
theories/Ints/num/Zn2Z.v
theories/Ints/num/ZnZ.v
+ theories/Ints/num/BigQ.v
+ theories/Ints/num/QMake_base.v
+ theories/Ints/num/Q0Make.v
+ theories/Ints/num/QbiMake.v
+ theories/Ints/num/QifMake.v
+ theories/Ints/num/QpMake.v
+ theories/Ints/num/QvMake.v
</dd>