Modifications de la construction de la documentation de la librairie

standard:
  - ajout d'une entrée dans le Makefile principal pour le fichier de
    globalisations glob.dump
  - modifications de doc/Makefile et de l'index html pour gérer les
    nouveaux fichiers de la librairie standard (en part. ceux dans
    Ints)



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10049 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 177 insertions, 138 deletions

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 7599db6dc..2a8693438 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -64,12 +64,27 @@ through the <tt>Require Import</tt> command.</p>
     theories/Logic/Hurkens.v
     theories/Logic/ProofIrrelevance.v
     theories/Logic/ProofIrrelevanceFacts.v
+    theories/Logic/ConstructiveEpsilon.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>Arith</b>:
     Basic Peano arithmetic
   </dt>
   <dd> 
+    theories/Arith/Arith_base.v
     theories/Arith/Le.v
     theories/Arith/Lt.v
     theories/Arith/Plus.v
@@ -84,7 +99,6 @@ through the <tt>Require Import</tt> command.</p>
     theories/Arith/Max.v
     theories/Arith/Compare.v
     theories/Arith/Div2.v
-    theories/Arith/Div.v
     theories/Arith/EqNat.v
     theories/Arith/Euclid.v
     theories/Arith/Even.v
@@ -129,6 +143,7 @@ through the <tt>Require Import</tt> command.</p>
     (theories/ZArith/ZArith_base.v)
     theories/ZArith/Zcomplements.v
     theories/ZArith/Zsqrt.v
+    theories/ZArith/Zpow_def.v
     theories/ZArith/Zpower.v
     theories/ZArith/Zdiv.v
     theories/ZArith/Zlogarithm.v
@@ -144,70 +159,27 @@ through the <tt>Require Import</tt> command.</p>
   </dt>
   <dd>
     theories/QArith/QArith_base.v
+    theories/QArith/Qabs.v
+    theories/QArith/Qpower.v
     theories/QArith/Qreduction.v
     theories/QArith/Qring.v
+    theories/QArith/Qfield.v
     (theories/QArith/QArith.v)
     theories/QArith/Qreals.v
     theories/QArith/Qcanon.v
   </dd>
     
-  <dt> <b>Reals</b>:
-    Formalization of real numbers
+    
+  <dt> <b>Relations</b>:
+       Relations (definitions and basic results)
   </dt>
   <dd> 
-    theories/Reals/Rdefinitions.v
-    theories/Reals/Raxioms.v
-    theories/Reals/RIneq.v
-    theories/Reals/DiscrR.v
-    (theories/Reals/Rbase.v)
-    theories/Reals/RList.v
-    theories/Reals/Ranalysis.v
-    theories/Reals/Rbasic_fun.v
-    theories/Reals/Rderiv.v
-    theories/Reals/Rfunctions.v
-    theories/Reals/Rgeom.v
-    theories/Reals/R_Ifp.v
-    theories/Reals/Rlimit.v
-    theories/Reals/Rseries.v
-    theories/Reals/Rsigma.v
-    theories/Reals/R_sqr.v
-    theories/Reals/Rtrigo_fun.v
-    theories/Reals/Rtrigo.v
-    theories/Reals/SplitAbsolu.v
-    theories/Reals/SplitRmult.v
-    theories/Reals/Alembert.v
-    theories/Reals/AltSeries.v
-    theories/Reals/ArithProp.v
-    theories/Reals/Binomial.v
-    theories/Reals/Cauchy_prod.v
-    theories/Reals/Cos_plus.v
-    theories/Reals/Cos_rel.v
-    theories/Reals/Exp_prop.v
-    theories/Reals/Integration.v
-    theories/Reals/MVT.v
-    theories/Reals/NewtonInt.v
-    theories/Reals/PSeries_reg.v
-    theories/Reals/PartSum.v
-    theories/Reals/R_sqrt.v
-    theories/Reals/Ranalysis1.v
-    theories/Reals/Ranalysis2.v
-    theories/Reals/Ranalysis3.v
-    theories/Reals/Ranalysis4.v
-    theories/Reals/Rcomplete.v
-    theories/Reals/RiemannInt.v
-    theories/Reals/RiemannInt_SF.v
-    theories/Reals/Rpower.v
-    theories/Reals/Rprod.v
-    theories/Reals/Rsqrt_def.v
-    theories/Reals/Rtopology.v
-    theories/Reals/Rtrigo_alt.v
-    theories/Reals/Rtrigo_calc.v
-    theories/Reals/Rtrigo_def.v
-    theories/Reals/Rtrigo_reg.v
-    theories/Reals/SeqProp.v
-    theories/Reals/SeqSeries.v
-    theories/Reals/Sqrt_reg.v
-    (theories/Reals/Reals.v)
+    theories/Relations/Relation_Definitions.v
+    theories/Relations/Relation_Operators.v
+    theories/Relations/Relations.v
+    theories/Relations/Operators_Properties.v
+    theories/Relations/Rstar.v
+    theories/Relations/Newman.v
   </dd>
     
   <dt> <b>Sets</b>:
@@ -238,18 +210,35 @@ through the <tt>Require Import</tt> command.</p>
     theories/Sets/Uniset.v
   </dd>
     
-  <dt> <b>Relations</b>:
-       Relations (definitions and basic results)
-  </dt>
+  <dt> <b>Setoids</b>:
   <dd> 
-    theories/Relations/Relation_Definitions.v
-    theories/Relations/Relation_Operators.v
-    theories/Relations/Relations.v
-    theories/Relations/Operators_Properties.v
-    theories/Relations/Rstar.v
-    theories/Relations/Newman.v
+    theories/Setoids/Setoid.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
+    theories/Lists/ListTactics.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>
+
   <dt> <b>Wellfounded</b>:
        Well-founded Relations
   </dt>
@@ -265,36 +254,26 @@ through the <tt>Require Import</tt> command.</p>
     theories/Wellfounded/Well_Ordering.v
   </dd>
     
-  <dt> <b>Setoids</b>:
-  <dd> 
-    theories/Setoids/Setoid.v
-  </dd>
-    
-  <dt> <b>Bool</b>:
-       Booleans (basic functions and results)
+
+  <dt> <b>IntMap</b>:
+    An implementation of finite sets/maps as trees indexed by addresses
   </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
+    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>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>
@@ -329,42 +308,99 @@ through the <tt>Require Import</tt> command.</p>
     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>
+<!--  <dt> <b>Strings</b>
     Implementation of string as list of ascii characters
   </dt>
   <dd>
     theories/Strings/Ascii.v
     theories/Strings/String.v
-  </dd>
+  </dd> -->
     
-  <dt> <b>Sorting</b>:
-    Axiomatizations of sorts
+  <dt> <b>Reals</b>:
+    Formalization of real numbers
   </dt>
   <dd> 
-    theories/Sorting/Heap.v
-    theories/Sorting/Permutation.v
-    theories/Sorting/Sorting.v
-    theories/Sorting/PermutEq.v
-    theories/Sorting/PermutSetoid.v
+    theories/Reals/Rdefinitions.v
+    theories/Reals/Raxioms.v
+    theories/Reals/RIneq.v
+    theories/Reals/DiscrR.v
+    (theories/Reals/Rbase.v)
+    theories/Reals/RList.v
+    theories/Reals/Ranalysis.v
+    theories/Reals/Rbasic_fun.v
+    theories/Reals/Rderiv.v
+    theories/Reals/Rfunctions.v
+    theories/Reals/Rgeom.v
+    theories/Reals/R_Ifp.v
+    theories/Reals/Rlimit.v
+    theories/Reals/Rseries.v
+    theories/Reals/Rsigma.v
+    theories/Reals/R_sqr.v
+    theories/Reals/Rtrigo_fun.v
+    theories/Reals/Rtrigo.v
+    theories/Reals/SplitAbsolu.v
+    theories/Reals/SplitRmult.v
+    theories/Reals/Alembert.v
+    theories/Reals/AltSeries.v
+    theories/Reals/ArithProp.v
+    theories/Reals/Binomial.v
+    theories/Reals/Cauchy_prod.v
+    theories/Reals/Cos_plus.v
+    theories/Reals/Cos_rel.v
+    theories/Reals/Exp_prop.v
+    theories/Reals/Integration.v
+    theories/Reals/MVT.v
+    theories/Reals/NewtonInt.v
+    theories/Reals/PSeries_reg.v
+    theories/Reals/PartSum.v
+    theories/Reals/R_sqrt.v
+    theories/Reals/Ranalysis1.v
+    theories/Reals/Ranalysis2.v
+    theories/Reals/Ranalysis3.v
+    theories/Reals/Ranalysis4.v
+    theories/Reals/Rcomplete.v
+    theories/Reals/RiemannInt.v
+    theories/Reals/RiemannInt_SF.v
+    theories/Reals/Rpow_def.v
+    theories/Reals/Rpower.v
+    theories/Reals/Rprod.v
+    theories/Reals/Rsqrt_def.v
+    theories/Reals/Rtopology.v
+    theories/Reals/Rtrigo_alt.v
+    theories/Reals/Rtrigo_calc.v
+    theories/Reals/Rtrigo_def.v
+    theories/Reals/Rtrigo_reg.v
+    theories/Reals/SeqProp.v
+    theories/Reals/SeqSeries.v
+    theories/Reals/Sqrt_reg.v
+    theories/Reals/LegacyRfield.v
+    (theories/Reals/Reals.v)
   </dd>
 
+  <dt> <b>Ints</b>:
+    Machine efficient large integers
+  </dt>
+  <dd> 
+    theories/Ints/Basic_type.v
+    theories/Ints/BigN.v
+    theories/Ints/BigZ.v
+    theories/Ints/Int31.v
+    theories/Ints/Tactic.v
+    theories/Ints/num/GenAdd.v
+    theories/Ints/num/GenBase.v
+    theories/Ints/num/GenDivn1.v
+    theories/Ints/num/GenDiv.v
+    theories/Ints/num/GenLift.v
+    theories/Ints/num/GenMul.v
+    theories/Ints/num/GenSqrt.v
+    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
+  </dd>
+
+
 </dl>
diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index
index ddbcd09fd..cbcd15ef3 100755
--- a/doc/stdlib/make-library-index
+++ b/doc/stdlib/make-library-index
@@ -7,27 +7,30 @@ FILE=$1
 cp -f $FILE.template tmp
 echo -n Building file index-list.prehtml ...
 
-for i in ../theories/*; do
-    echo $i
+LIBDIRS="Init Logic Bool Arith NArith ZArith QArith Relations Sets Setoids Lists Sorting Wellfounded IntMap FSets Reals Ints Ints/num"
 
-  d=`basename $i`
-  if [ "$d" != "Num" -a "$d" != "CVS" ]; then
-  for j in $i/*.v; do
-    b=`basename $j .v`
-    rm -f tmp2
-    grep -q theories/$d/$b.v tmp
-    a=$?
-    if [ $a = 0 ]; then
-      sed -e "s:theories/$d/$b.v:<a href=\"Coq.$d.$b.html\">$b</a>:g" tmp > tmp2
-      mv -f tmp2 tmp
-    else
-      echo Warning: theories/$d/$b.v is missing in the template file
+for k in $LIBDIRS; do
+    i=../theories/$k
+    echo $i
+    
+    d=`basename $i`
+    if [ "$d" != "Num" -a "$d" != "CVS" ]; then
+	for j in $i/*.v; do
+	    b=`basename $j .v`
+	    rm -f tmp2
+	    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
+		mv -f tmp2 tmp
+	    else
+		echo Warning: theories/$k/$b.v is missing in the template file
+	    fi
+	done
     fi
-  done
-  fi
-  rm -f tmp2
-  sed -e "s/#$d#//" tmp > tmp2
-  mv -f tmp2 tmp
+    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