From c6d34ae80622b409733776c3cc4ecf5fce6a8378 Mon Sep 17 00:00:00 2001
From: notin
Date: Wed, 28 Nov 2007 18:07:28 +0000
Subject: 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
---
 doc/stdlib/index-list.html.template | 69 ++++++++++++++++++++++++++++++++++---
 doc/stdlib/make-library-index       |  5 +--
 2 files changed, 67 insertions(+), 7 deletions(-)

(limited to 'doc/stdlib')

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 65d69a1d8e..ba306b8871 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>
 
     
diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index
index 27dfc434f1..a2aed15f36 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 Setoids Lists Sorting Wellfounded IntMap FSets Reals Ints Ints/num Program"
+LIBDIRS="Init Logic Bool Arith NArith ZArith QArith Relations Sets Setoids Lists Sorting Wellfounded IntMap FSets Reals Ints Ints/num Ints/Z Program Numbers Numbers/Natural/Abstract Numbers/Natural/Peano Numbers/Natural/Binary Numbers/Integer/Abstract Numbers/Integer/NatPairs Numbers/Integer/Binary Numbers/NatInt Strings" 
 
 for k in $LIBDIRS; do
     i=../theories/$k
@@ -21,7 +21,8 @@ for k in $LIBDIRS; do
 	    grep -q theories/$k/$b.v tmp
 	    a=$?
 	    if [ $a = 0 ]; then
-		sed -e "s:theories/$k/$b.v:<a href=\"Coq.$d.$b.html\">$b</a>:g" tmp > tmp2
+		p=${k//\//.}
+		sed -e "s:theories/$k/$b.v:<a href=\"Coq.$p.$b.html\">$b</a>:g" tmp > tmp2
 		mv -f tmp2 tmp
 	    else
 		echo Warning: theories/$k/$b.v is missing in the template file
-- 
cgit v1.2.3