Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

3 files changed, 13 insertions, 12 deletions

diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex
index f9764bea..61fa253c 100755
--- a/doc/stdlib/Library.tex
+++ b/doc/stdlib/Library.tex
@@ -3,7 +3,7 @@
 \usepackage[latin1]{inputenc}
 \usepackage[T1]{fontenc}
 \usepackage{fullpage}
-\usepackage{../../coqdoc}
+\usepackage[color]{../../coqdoc}
 
 \input{../common/version}
 \input{../common/title}
@@ -61,4 +61,4 @@ you can access from the \Coq\ home page at
 
 \end{document}
 
-% $Id: Library.tex 11091 2008-06-10 18:24:52Z notin $ 
+% $Id: Library.tex 11576 2008-11-10 19:13:15Z msozeau $ 
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 5e95a692..0ab4e47b 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -69,6 +69,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Logic/Description.v
     theories/Logic/Epsilon.v
     theories/Logic/IndefiniteDescription.v
+    theories/Logic/FunctionalExtensionality.v
   </dd>
     
   <dt> <b>Bool</b>:
@@ -256,12 +257,7 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
 
   <dd>
     theories/Numbers/Rational/BigQ/BigQ.v
-    theories/Numbers/Rational/BigQ/Q0Make.v
-    theories/Numbers/Rational/BigQ/QbiMake.v
-    theories/Numbers/Rational/BigQ/QifMake.v
-    theories/Numbers/Rational/BigQ/QMake_base.v
-    theories/Numbers/Rational/BigQ/QpMake.v
-    theories/Numbers/Rational/BigQ/QvMake.v
+    theories/Numbers/Rational/BigQ/QMake.v
     theories/Numbers/Rational/SpecViaQ/QSig.v
   </dd>
   
@@ -273,8 +269,10 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
     theories/Relations/Relation_Operators.v
     theories/Relations/Relations.v
     theories/Relations/Operators_Properties.v
+<!-- Deprecated 
     theories/Relations/Rstar.v
     theories/Relations/Newman.v
+-->
   </dd>
     
   <dt> <b>Sets</b>:
@@ -314,6 +312,7 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
     theories/Classes/Morphisms_Relations.v
     theories/Classes/Equivalence.v
     theories/Classes/EquivDec.v
+    theories/Classes/Functions.v
     theories/Classes/SetoidTactics.v
     theories/Classes/SetoidClass.v
     theories/Classes/SetoidDec.v
@@ -321,8 +320,11 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
   </dd>
 
   <dt> <b>Setoids</b>:
+
   <dd> 
     theories/Setoids/Setoid.v
+    theories/Setoids/Setoid_tac.v
+    theories/Setoids/Setoid_Prop.v
   </dd>
     
   <dt> <b>Lists</b>:
@@ -477,7 +479,6 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
     theories/Program/Utils.v
     theories/Program/Syntax.v
     theories/Program/Program.v
-    theories/Program/FunctionalExtensionality.v
     theories/Program/Combinators.v
   </dd>
 
diff --git a/doc/stdlib/make-library-files b/doc/stdlib/make-library-files
index add14a13..9516a19f 100755
--- a/doc/stdlib/make-library-files
+++ b/doc/stdlib/make-library-files
@@ -1,6 +1,6 @@
 #!/bin/sh
 
-# Needs COQTOP and GALLINA set
+# Needs COQSRC and GALLINA set
 
 # On garde la liste de tous les *.v avec dates dans library.files.ls
 # Si elle a change depuis la derniere fois ou library.files n'existe pas
@@ -13,12 +13,12 @@
 LIBDIRS="Arith NArith ZArith Reals Logic Bool Lists Relations Sets Sorting Wellfounded Setoids Program Classes"
 
 rm -f library.files.ls.tmp
-(cd $COQTOP/theories; find $LIBDIR -name "*.v" -ls) > library.files.ls.tmp
+(cd $COQSRC/theories; find $LIBDIR -name "*.v" -ls) > library.files.ls.tmp
 if ! test -e library.files || ! cmp library.files.ls library.files.ls.tmp; then
   mv -f library.files.ls.tmp library.files.ls
   rm -f library.files; touch library.files
   ABSOLUTE=`pwd`/library.files
-  cd $COQTOP/theories
+  cd $COQSRC/theories
   echo $LIBDIRS
   for rep in $LIBDIRS ; do
     (cd $rep