Imported Upstream version 8.5~beta1+dfsg

5 files changed, 59 insertions, 83 deletions

diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex
index cb32adfc..44a0b1d3 100755
--- a/doc/stdlib/Library.tex
+++ b/doc/stdlib/Library.tex
@@ -1,9 +1,11 @@
 \documentclass[11pt]{report}
 
+\usepackage[mathletters]{ucs}
 \usepackage[utf8x]{inputenc}
 \usepackage[T1]{fontenc}
 \usepackage{fullpage}
 \usepackage{amsfonts}
+\usepackage{url}
 \usepackage[color]{../../coqdoc}
 
 \input{../common/version}
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index e69de29b..8b137891 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -0,0 +1 @@
+
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 833b5c4c..854c786c 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -3,7 +3,7 @@
 
 <p>Here is a short description of the Coq standard library, which is
 distributed with the system.
-It provides a set of modules directly available 
+It provides a set of modules directly available
 through the <tt>Require Import</tt> command.</p>
 
 <p>The standard library is composed of the following subdirectories:</p>
@@ -12,27 +12,26 @@ through the <tt>Require Import</tt> command.</p>
   <dt> <b>Init</b>:
     The core library (automatically loaded when starting Coq)
   </dt>
-  <dd> 
+  <dd>
     theories/Init/Notations.v
     theories/Init/Datatypes.v
     theories/Init/Logic.v
     theories/Init/Logic_Type.v
+    theories/Init/Nat.v
     theories/Init/Peano.v
     theories/Init/Specif.v
     theories/Init/Tactics.v
     theories/Init/Wf.v
     (theories/Init/Prelude.v)
   </dd>
-  
+
   <dt> <b>Logic</b>:
-      Classical logic and dependent equality
+      Classical logic, dependent equality, extensionality, choice axioms
   </dt>
   <dd>
     theories/Logic/SetIsType.v
-    theories/Logic/Classical_Pred_Set.v
     theories/Logic/Classical_Pred_Type.v
     theories/Logic/Classical_Prop.v
-    theories/Logic/Classical_Type.v
     (theories/Logic/Classical.v)
     theories/Logic/ClassicalFacts.v
     theories/Logic/Decidable.v
@@ -57,8 +56,11 @@ through the <tt>Require Import</tt> command.</p>
     theories/Logic/IndefiniteDescription.v
     theories/Logic/FunctionalExtensionality.v
     theories/Logic/ExtensionalityFacts.v
+    theories/Logic/WeakFan.v
+    theories/Logic/WKL.v
+    theories/Logic/FinFun.v
   </dd>
-    
+
   <dt> <b>Structures</b>:
        Algebraic structures (types with equality, with order, ...).
        DecidableType* and OrderedType* are there only for compatibility.
@@ -83,7 +85,7 @@ through the <tt>Require Import</tt> command.</p>
   <dt> <b>Bool</b>:
        Booleans (basic functions and results)
   </dt>
-  <dd> 
+  <dd>
     theories/Bool/Bool.v
     theories/Bool/BoolEq.v
     theories/Bool/DecBool.v
@@ -92,12 +94,12 @@ through the <tt>Require Import</tt> command.</p>
     theories/Bool/Zerob.v
     theories/Bool/Bvector.v
   </dd>
-    
+
   <dt> <b>Arith</b>:
     Basic Peano arithmetic
   </dt>
-  <dd> 
-    theories/Arith/Arith_base.v
+  <dd>
+    theories/Arith/PeanoNat.v
     theories/Arith/Le.v
     theories/Arith/Lt.v
     theories/Arith/Plus.v
@@ -107,6 +109,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Arith/Between.v
     theories/Arith/Peano_dec.v
     theories/Arith/Compare_dec.v
+    (theories/Arith/Arith_base.v)
     (theories/Arith/Arith.v)
     theories/Arith/Min.v
     theories/Arith/Max.v
@@ -173,8 +176,6 @@ through the <tt>Require Import</tt> command.</p>
     theories/ZArith/Zpow_def.v
     theories/ZArith/Zpow_alt.v
     theories/ZArith/Zpower.v
-    theories/ZArith/ZOdiv_def.v
-    theories/ZArith/ZOdiv.v
     theories/ZArith/Zdiv.v
     theories/ZArith/Zquot.v
     theories/ZArith/Zeuclid.v
@@ -206,10 +207,13 @@ through the <tt>Require Import</tt> command.</p>
     theories/QArith/Qminmax.v
   </dd>
 
-  <dt> <b>Numbers</b>: 
+  <dt> <b>Numbers</b>:
     An experimental modular architecture for arithmetic
   </dt>
-    <dt> <b>&nbsp;&nbsp;Prelude</b>: 
+  <dd>
+    <dl>
+    <dt> <b>&nbsp;&nbsp;Prelude</b>:
+    </dt>
     <dd>
     theories/Numbers/BinNums.v
     theories/Numbers/NumPrelude.v
@@ -219,6 +223,7 @@ through the <tt>Require Import</tt> command.</p>
 
     <dt> <b>&nbsp;&nbsp;NatInt</b>:
        Abstract mixed natural/integer/cyclic arithmetic
+    </dt>
     <dd>
     theories/Numbers/NatInt/NZAdd.v
     theories/Numbers/NatInt/NZAddOrder.v
@@ -237,10 +242,10 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/NatInt/NZGcd.v
     theories/Numbers/NatInt/NZBits.v
     </dd>
-    </dt>
 
-    <dt> <b>&nbsp;&nbsp;Cyclic</b>: 
+    <dt> <b>&nbsp;&nbsp;Cyclic</b>:
        Abstract and 31-bits-based cyclic arithmetic
+    </dt>
     <dd>
     theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
     theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -259,10 +264,10 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/Cyclic/Int31/Int31.v
     theories/Numbers/Cyclic/ZModulo/ZModulo.v
     </dd>
-    </dt>
 
-    <dt> <b>&nbsp;&nbsp;Natural</b>: 
+    <dt> <b>&nbsp;&nbsp;Natural</b>:
        Abstract and 31-bits-words-based natural arithmetic
+    </dt>
     <dd>
     theories/Numbers/Natural/Abstract/NAdd.v
     theories/Numbers/Natural/Abstract/NAddOrder.v
@@ -293,10 +298,11 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/Natural/BigN/NMake.v
     theories/Numbers/Natural/BigN/NMake_gen.v
     </dd>
-    </dt>
 
-    <dt> <b>&nbsp;&nbsp;Integer</b>: 
-       Abstract and concrete (especially 31-bits-words-based) integer arithmetic
+    <dt> <b>&nbsp;&nbsp;Integer</b>:
+       Abstract and concrete (especially 31-bits-words-based) integer
+       arithmetic
+    </dt>
     <dd>
     theories/Numbers/Integer/Abstract/ZAdd.v
     theories/Numbers/Integer/Abstract/ZAddOrder.v
@@ -323,32 +329,32 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/Integer/BigZ/BigZ.v
     theories/Numbers/Integer/BigZ/ZMake.v
     </dd>
-    </dt>
 
     <dt><b>&nbsp;&nbsp;Rational</b>:
        Abstract and 31-bits-words-based rational arithmetic
+    </dt>
     <dd>
     theories/Numbers/Rational/SpecViaQ/QSig.v
     theories/Numbers/Rational/BigQ/BigQ.v
     theories/Numbers/Rational/BigQ/QMake.v
     </dd>
-    </dt>
-  </dt>
-  
+    </dl>
+  </dd>
+
   <dt> <b>Relations</b>:
        Relations (definitions and basic results)
   </dt>
-  <dd> 
+  <dd>
     theories/Relations/Relation_Definitions.v
     theories/Relations/Relation_Operators.v
     theories/Relations/Relations.v
     theories/Relations/Operators_Properties.v
   </dd>
-    
+
   <dt> <b>Sets</b>:
        Sets (classical, constructive, finite, infinite, powerset, etc.)
   </dt>
-  <dd> 
+  <dd>
     theories/Sets/Classical_sets.v
     theories/Sets/Constructive_sets.v
     theories/Sets/Cpo.v
@@ -372,32 +378,39 @@ through the <tt>Require Import</tt> command.</p>
     theories/Sets/Relations_3.v
     theories/Sets/Uniset.v
   </dd>
-    
+
   <dt> <b>Classes</b>:
-  <dd> 
+  </dt>
+  <dd>
     theories/Classes/Init.v
     theories/Classes/RelationClasses.v
     theories/Classes/Morphisms.v
     theories/Classes/Morphisms_Prop.v
     theories/Classes/Morphisms_Relations.v
     theories/Classes/Equivalence.v
+    theories/Classes/CRelationClasses.v
+    theories/Classes/CMorphisms.v
+    theories/Classes/CEquivalence.v
     theories/Classes/EquivDec.v
     theories/Classes/SetoidTactics.v
     theories/Classes/SetoidClass.v
     theories/Classes/SetoidDec.v
     theories/Classes/RelationPairs.v
+    theories/Classes/DecidableClass.v
   </dd>
 
   <dt> <b>Setoids</b>:
-  <dd> 
+  </dt>
+  <dd>
     theories/Setoids/Setoid.v
   </dd>
-    
+
   <dt> <b>Lists</b>:
     Polymorphic lists, Streams (infinite sequences)
   </dt>
-  <dd> 
+  <dd>
     theories/Lists/List.v
+    theories/Lists/ListDec.v
     theories/Lists/ListSet.v
     theories/Lists/SetoidList.v
     theories/Lists/SetoidPermutation.v
@@ -413,13 +426,14 @@ through the <tt>Require Import</tt> command.</p>
     theories/Vectors/Fin.v
     theories/Vectors/VectorDef.v
     theories/Vectors/VectorSpec.v
+    theories/Vectors/VectorEq.v
     (theories/Vectors/Vector.v)
   </dd>
 
   <dt> <b>Sorting</b>:
     Axiomatizations of sorts
   </dt>
-  <dd> 
+  <dd>
     theories/Sorting/Heap.v
     theories/Sorting/Permutation.v
     theories/Sorting/Sorting.v
@@ -432,7 +446,7 @@ through the <tt>Require Import</tt> command.</p>
   <dt> <b>Wellfounded</b>:
        Well-founded Relations
   </dt>
-  <dd> 
+  <dd>
     theories/Wellfounded/Disjoint_Union.v
     theories/Wellfounded/Inclusion.v
     theories/Wellfounded/Inverse_Image.v
@@ -500,11 +514,11 @@ through the <tt>Require Import</tt> command.</p>
     theories/Strings/Ascii.v
     theories/Strings/String.v
   </dd>
-    
+
   <dt> <b>Reals</b>:
     Formalization of real numbers
   </dt>
-  <dd> 
+  <dd>
     theories/Reals/Rdefinitions.v
     theories/Reals/Raxioms.v
     theories/Reals/RIneq.v
@@ -566,14 +580,13 @@ through the <tt>Require Import</tt> command.</p>
     theories/Reals/SeqSeries.v
     theories/Reals/Sqrt_reg.v
     theories/Reals/Rlogic.v
-    theories/Reals/LegacyRfield.v
     (theories/Reals/Reals.v)
   </dd>
-    
+
   <dt> <b>Program</b>:
     Support for dependently-typed programming.
   </dt>
-  <dd> 
+  <dd>
     theories/Program/Basics.v
     theories/Program/Wf.v
     theories/Program/Subset.v
diff --git a/doc/stdlib/make-library-files b/doc/stdlib/make-library-files
deleted file mode 100755
index c071c4a2..00000000
--- a/doc/stdlib/make-library-files
+++ /dev/null
@@ -1,36 +0,0 @@
-#!/bin/sh
-
-# 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
-# on fabrique des .g (si besoin) et la liste library.files dans 
-# l'ordre de ls -tr des *.vo
-# Ce dernier trie les fichiers dans l'ordre inverse de leur date de création
-# En supposant que make fait son boulot, ca fait un tri topologique du
-# graphe des dépendances
-
-LIBDIRS="Arith PArith NArith ZArith Reals Logic Bool Lists Relations Sets Sorting Wellfounded Setoids Program Classes Numbers"
-
-rm -f 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 $COQSRC/theories
-  echo $LIBDIRS
-  for rep in $LIBDIRS ; do
-    (cd $rep
-     echo $rep/intro.tex >> $ABSOLUTE
-     VOFILES=`ls -tr *.vo`
-     for file in $VOFILES ; do
-       VF=`basename $file \.vo`
-       if [ \( ! -e $VF.g \) -o \( $VF.v -nt $VF.g \) ] ; then
-          $GALLINA $VF.v
-       fi
-       echo $rep/$VF.g >> $ABSOLUTE
-     done
-    )
-  done
-fi
diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index
index 1a70567f..43802efa 100755
--- a/doc/stdlib/make-library-index
+++ b/doc/stdlib/make-library-index
@@ -6,17 +6,14 @@ FILE=$1
 HIDDEN=$2
 
 cp -f $FILE.template tmp
-echo -n Building file index-list.prehtml ...
+echo -n "Building file index-list.prehtml... "
 
 #LIBDIRS="Init Logic Structures Bool Arith PArith NArith ZArith QArith Relations Sets Classes Setoids Lists Vectors Sorting Wellfounded MSets FSets Reals Program Numbers Numbers/Natural/Abstract Numbers/Natural/Peano Numbers/Natural/Binary Numbers/Natural/BigN Numbers/Natural/SpecViaZ Numbers/Integer/Abstract Numbers/Integer/NatPairs Numbers/Integer/Binary Numbers/Integer/SpecViaZ Numbers/Integer/BigZ Numbers/NatInt Numbers/Cyclic/Abstract Numbers/Cyclic/Int31 Numbers/Cyclic/ZModulo Numbers/Cyclic/DoubleCyclic Numbers/Rational/BigQ Numbers/Rational/SpecViaQ Strings"
-LIBDIRS=`find theories/* -type d | sed -e "s:^theories/::"`
+LIBDIRS=`find theories/* -type d ! -name .coq-native | sed -e "s:^theories/::"`
 
 for k in $LIBDIRS; do
     i=theories/$k
-    echo $i
-    
     d=`basename $i`
-    if [ "$d" != "CVS" ]; then
       ls $i | grep -q \.v'$'
       if [ $? = 0 ]; then
 	for j in $i/*.v; do
@@ -46,7 +43,6 @@ for k in $LIBDIRS; do
             fi
 	done
       fi
-    fi
     rm -f tmp2
     sed -e "s/#$d#//" tmp > tmp2
     mv -f tmp2 tmp