From 4ef543b711e2e066c8e3378667371ba4c7c5099b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 9 Jun 2006 16:06:14 +0000
Subject: MAJ liste fichiers doc stdlib

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8937 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/Makefile                        |   2 +-
 doc/stdlib/index-list.html.template | 149 +++++++++++++++++++++---------------
 2 files changed, 89 insertions(+), 62 deletions(-)

diff --git a/doc/Makefile b/doc/Makefile
index 7ded383f9b..fd508e070c 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -207,7 +207,7 @@ faq/html/index.html: faq/FAQ.v.html
 
 GLOBDUMP=$(COQTOP)/glob.dump
 
-LIBDIRS= Logic Bool Arith ZArith Reals Lists Sets Relations Sorting Wellfounded IntMap FSets
+LIBDIRS= Logic Bool Arith ZArith QArith Reals Lists Sets Relations Sorting Wellfounded IntMap FSets
 
 ### Standard library (browsable html format)
 
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index fd91ca26dd..10744fe4fe 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -41,16 +41,20 @@ through the <tt>Require Import</tt> command.</p>
     theories/Logic/Classical_Prop.v
     theories/Logic/Classical_Type.v
     (theories/Logic/Classical.v)
+    theories/Logic/ClassicalFacts.v
     theories/Logic/Decidable.v
+    theories/Logic/DecidableType.v
+    theories/Logic/DecidableTypeEx.v
     theories/Logic/Eqdep_dec.v
     theories/Logic/EqdepFacts.v
     theories/Logic/Eqdep.v
     theories/Logic/JMeq.v
+    theories/Logic/ChoiceFacts.v
     theories/Logic/RelationalChoice.v
     theories/Logic/ClassicalChoice.v
-    theories/Logic/ChoiceFacts.v
     theories/Logic/ClassicalDescription.v
-    theories/Logic/ClassicalFacts.v
+    theories/Logic/ClassicalEpsilon.v
+    theories/Logic/ClassicalUniqueChoice.v
     theories/Logic/Berardi.v
     theories/Logic/Diaconescu.v
     theories/Logic/Hurkens.v
@@ -93,7 +97,11 @@ through the <tt>Require Import</tt> command.</p>
     theories/NArith/BinNat.v
     (theories/NArith/NArith.v)
     theories/NArith/Pnat.v
-  </dd>
+    theories/NArith/Nnat.v
+    theories/NArith/Ndigits.v
+    theories/NArith/Ndist.v
+    theories/NArith/Ndec.v
+.  </dd>
 
   <dt> <b>ZArith</b>:
        Binary integers
@@ -124,6 +132,18 @@ through the <tt>Require Import</tt> command.</p>
     theories/ZArith/Zwf.v
     theories/ZArith/Zbinary.v
     theories/ZArith/Znumtheory.v
+    theories/ZArith/Int.v
+  </dd>
+
+  <dt> <b>Reals</b>:
+    Rational numbers
+  </dt>
+  <dd>
+    theories/QArith/QArith_base.v
+    theories/QArith/Qreduction.v
+    theories/QArith/Qring.v
+    (theories/QArith/QArith.v)
+    theories/QArith/Qreals.v
   </dd>
     
   <dt> <b>Reals</b>:
@@ -185,31 +205,6 @@ through the <tt>Require Import</tt> command.</p>
     (theories/Reals/Reals.v)
   </dd>
     
-  <dt> <b>Bool</b>:
-       Booleans (basic functions and results)
-  </dt>
-  <dd> 
-    theories/Bool/Bool.v
-    theories/Bool/BoolEq.v
-    theories/Bool/DecBool.v
-    theories/Bool/IfProp.v
-    theories/Bool/Sumbool.v
-    theories/Bool/Zerob.v
-    theories/Bool/Bvector.v
-  </dd>
-    
-  <dt> <b>Lists</b>:
-    Polymorphic lists, Streams (infinite sequences)
-  </dt>
-  <dd> 
-    theories/Lists/List.v
-    theories/Lists/ListSet.v
-    theories/Lists/MonoList.v
-    theories/Lists/SetoidList.v
-    theories/Lists/Streams.v
-    theories/Lists/TheoryList.v
-  </dd>
-  
   <dt> <b>Sets</b>:
        Sets (classical, constructive, finite, infinite, powerset, etc.)
   </dt>
@@ -265,67 +260,89 @@ through the <tt>Require Import</tt> command.</p>
     theories/Wellfounded/Well_Ordering.v
   </dd>
     
-  <dt> <b>Sorting</b>:
-    Axiomatizations of sorts
-  </dt>
-  <dd> 
-    theories/Sorting/Heap.v
-    theories/Sorting/Permutation.v
-    theories/Sorting/Sorting.v
-  </dd>
-  
   <dt> <b>Setoids</b>:
   <dd> 
     theories/Setoids/Setoid.v
   </dd>
     
-  <dt> <b>IntMap</b>:
-    Finite sets/maps as trees indexed by addresses
+  <dt> <b>Bool</b>:
+       Booleans (basic functions and results)
   </dt>
   <dd> 
-    theories/IntMap/Addr.v
-    theories/IntMap/Adist.v
-    theories/IntMap/Addec.v
-    theories/IntMap/Adalloc.v
-    theories/IntMap/Map.v
-    theories/IntMap/Fset.v
-    theories/IntMap/Mapaxioms.v
-    theories/IntMap/Mapiter.v
-    theories/IntMap/Mapcanon.v
-    theories/IntMap/Mapsubset.v
-    theories/IntMap/Lsort.v
-    theories/IntMap/Mapfold.v
-    theories/IntMap/Mapcard.v
-    theories/IntMap/Mapc.v
-    theories/IntMap/Maplists.v
-    theories/IntMap/Allmaps.v
+    theories/Bool/Bool.v
+    theories/Bool/BoolEq.v
+    theories/Bool/DecBool.v
+    theories/Bool/IfProp.v
+    theories/Bool/Sumbool.v
+    theories/Bool/Zerob.v
+    theories/Bool/Bvector.v
   </dd>
     
+  <dt> <b>Lists</b>:
+    Polymorphic lists, Streams (infinite sequences)
+  </dt>
+  <dd> 
+    theories/Lists/List.v
+    theories/Lists/ListSet.v
+    theories/Lists/MonoList.v
+    theories/Lists/SetoidList.v
+    theories/Lists/Streams.v
+    theories/Lists/TheoryList.v
+  </dd>
+
   <dt> <b>FSets</b>:
     Modular implementation of finite sets/maps using lists
   </dt>
   <dd>
-    theories/FSets/DecidableType.v
     theories/FSets/OrderedType.v
+    theories/FSets/OrderedTypeAlt.v
+    theories/FSets/OrderedTypeEx.v
     theories/FSets/FSetInterface.v
     theories/FSets/FSetBridge.v
     theories/FSets/FSetProperties.v
     theories/FSets/FSetEqProperties.v
-    theories/FSets/FSetFacts.v
     theories/FSets/FSetList.v
-    theories/FSets/FSet.v
-    theories/FSets/FMapInterface.v
-    theories/FSets/FMapList.v
-    theories/FSets/FMap.v
+    (theories/FSets/FSets.v)
+    theories/FSets/FSetFacts.v
+    theories/FSets/FSetAVL.v
+    theories/FSets/FSetToFiniteSet.v
+    theories/FSets/FSetWeakProperties.v
     theories/FSets/FSetWeakInterface.v
     theories/FSets/FSetWeakFacts.v
     theories/FSets/FSetWeakList.v
     theories/FSets/FSetWeak.v
+    theories/FSets/FMapInterface.v
+    theories/FSets/FMapList.v
+    theories/FSets/FMapPositive.v
+    theories/FSets/FMapIntMap.v
+    theories/FSets/FMapFacts.v
+    (theories/FSets/FMaps.v)
+    theories/FSets/FMapAVL.v
     theories/FSets/FMapWeakInterface.v
     theories/FSets/FMapWeakList.v
     theories/FSets/FMapWeak.v
+    theories/FSets/FMapWeakFacts.v
   </dd>
 
+  <dt> <b>IntMap</b>:
+    An implementation of finite sets/maps as trees indexed by addresses
+  </dt>
+  <dd> 
+    theories/IntMap/Adalloc.v
+    theories/IntMap/Map.v
+    theories/IntMap/Fset.v
+    theories/IntMap/Mapaxioms.v
+    theories/IntMap/Mapiter.v
+    theories/IntMap/Mapcanon.v
+    theories/IntMap/Mapsubset.v
+    theories/IntMap/Lsort.v
+    theories/IntMap/Mapfold.v
+    theories/IntMap/Mapcard.v
+    theories/IntMap/Mapc.v
+    theories/IntMap/Maplists.v
+    theories/IntMap/Allmaps.v
+  </dd>
+    
   <dt> <b>Strings</b>
     Implementation of string as list of ascii characters
   </dt>
@@ -334,5 +351,15 @@ through the <tt>Require Import</tt> command.</p>
     theories/Strings/String.v
   </dd>
     
+  <dt> <b>Sorting</b>:
+    Axiomatizations of sorts
+  </dt>
+  <dd> 
+    theories/Sorting/Heap.v
+    theories/Sorting/Permutation.v
+    theories/Sorting/Sorting.v
+    theories/Sorting/PermutEq.v
+    theories/Sorting/PermutSetoid.v
   </dd>
+
 </dl>
-- 
cgit v1.2.3