Imported Upstream version 8.9.0upstream/8.9.0upstream

3 files changed, 104 insertions, 16 deletions

diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index 8b137891..b58148ff 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -1 +1,77 @@
-
+plugins/btauto/Algebra.v
+plugins/btauto/Btauto.v
+plugins/btauto/Reflect.v
+plugins/derive/Derive.v
+plugins/extraction/ExtrHaskellBasic.v
+plugins/extraction/ExtrHaskellNatInt.v
+plugins/extraction/ExtrHaskellNatInteger.v
+plugins/extraction/ExtrHaskellNatNum.v
+plugins/extraction/ExtrHaskellString.v
+plugins/extraction/ExtrHaskellZInt.v
+plugins/extraction/ExtrHaskellZInteger.v
+plugins/extraction/ExtrHaskellZNum.v
+plugins/extraction/ExtrOcamlBasic.v
+plugins/extraction/ExtrOcamlBigIntConv.v
+plugins/extraction/ExtrOcamlIntConv.v
+plugins/extraction/ExtrOcamlNatBigInt.v
+plugins/extraction/ExtrOcamlNatInt.v
+plugins/extraction/ExtrOcamlString.v
+plugins/extraction/ExtrOcamlZBigInt.v
+plugins/extraction/ExtrOcamlZInt.v
+plugins/extraction/Extraction.v
+plugins/funind/FunInd.v
+plugins/funind/Recdef.v
+plugins/ltac/Ltac.v
+plugins/micromega/Env.v
+plugins/micromega/EnvRing.v
+plugins/micromega/Fourier.v
+plugins/micromega/Fourier_util.v
+plugins/micromega/Lia.v
+plugins/micromega/Lqa.v
+plugins/micromega/Lra.v
+plugins/micromega/MExtraction.v
+plugins/micromega/OrderedRing.v
+plugins/micromega/Psatz.v
+plugins/micromega/QMicromega.v
+plugins/micromega/RMicromega.v
+plugins/micromega/Refl.v
+plugins/micromega/RingMicromega.v
+plugins/micromega/Tauto.v
+plugins/micromega/VarMap.v
+plugins/micromega/ZCoeff.v
+plugins/micromega/ZMicromega.v
+plugins/nsatz/Nsatz.v
+plugins/omega/Omega.v
+plugins/omega/OmegaLemmas.v
+plugins/omega/OmegaPlugin.v
+plugins/omega/OmegaTactic.v
+plugins/omega/PreOmega.v
+plugins/quote/Quote.v
+plugins/romega/ROmega.v
+plugins/romega/ReflOmegaCore.v
+plugins/rtauto/Bintree.v
+plugins/rtauto/Rtauto.v
+plugins/setoid_ring/Algebra_syntax.v
+plugins/setoid_ring/ArithRing.v
+plugins/setoid_ring/BinList.v
+plugins/setoid_ring/Cring.v
+plugins/setoid_ring/Field.v
+plugins/setoid_ring/Field_tac.v
+plugins/setoid_ring/Field_theory.v
+plugins/setoid_ring/InitialRing.v
+plugins/setoid_ring/Integral_domain.v
+plugins/setoid_ring/NArithRing.v
+plugins/setoid_ring/Ncring.v
+plugins/setoid_ring/Ncring_initial.v
+plugins/setoid_ring/Ncring_polynom.v
+plugins/setoid_ring/Ncring_tac.v
+plugins/setoid_ring/RealField.v
+plugins/setoid_ring/Ring.v
+plugins/setoid_ring/Ring_base.v
+plugins/setoid_ring/Ring_polynom.v
+plugins/setoid_ring/Ring_tac.v
+plugins/setoid_ring/Ring_theory.v
+plugins/setoid_ring/Rings_Q.v
+plugins/setoid_ring/Rings_R.v
+plugins/setoid_ring/Rings_Z.v
+plugins/setoid_ring/ZArithRing.v
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 8c09b23a..e502cb1b 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -226,6 +226,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/BinNums.v
     theories/Numbers/NumPrelude.v
     theories/Numbers/NaryFunctions.v
+    theories/Numbers/AltBinNotations.v
     theories/Numbers/DecimalFacts.v
     theories/Numbers/DecimalNat.v
     theories/Numbers/DecimalPos.v
@@ -498,6 +499,9 @@ through the <tt>Require Import</tt> command.</p>
   <dd>
     theories/Strings/Ascii.v
     theories/Strings/String.v
+    theories/Strings/BinaryString.v
+    theories/Strings/HexString.v
+    theories/Strings/OctalString.v
   </dd>
 
   <dt> <b>Reals</b>:
@@ -583,6 +587,17 @@ through the <tt>Require Import</tt> command.</p>
     theories/Program/Combinators.v
   </dd>
 
+  <dt> <b>SSReflect</b>:
+    Base libraries for the SSReflect proof language and the
+    small scale reflection formalization technique
+  </dt>
+  <dd>
+    plugins/ssrmatching/ssrmatching.v
+    plugins/ssr/ssreflect.v
+    plugins/ssr/ssrbool.v
+    plugins/ssr/ssrfun.v
+  </dd>
+
   <dt> <b>Unicode</b>:
     Unicode-based notations
   </dt>
@@ -596,8 +611,8 @@ through the <tt>Require Import</tt> command.</p>
   </dt>
   <dd>
     theories/Compat/AdmitAxiom.v
-    theories/Compat/Coq86.v
     theories/Compat/Coq87.v
     theories/Compat/Coq88.v
+    theories/Compat/Coq89.v
   </dd>
 </dl>
diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index
index 43802efa..bea6f240 100755
--- a/doc/stdlib/make-library-index
+++ b/doc/stdlib/make-library-index
@@ -8,35 +8,32 @@ HIDDEN=$2
 cp -f $FILE.template tmp
 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 ! -name .coq-native | sed -e "s:^theories/::"`
+LIBDIRS=`find theories/* plugins/* -type d ! -name .coq-native`
 
 for k in $LIBDIRS; do
-    i=theories/$k
-    d=`basename $i`
-      ls $i | grep -q \.v'$'
+    d=`basename $k`
+      ls $k | grep -q \.v'$'
       if [ $? = 0 ]; then
-	for j in $i/*.v; do
+	for j in $k/*.v; do
 	    b=`basename $j .v`
 	    rm -f tmp2
-	    grep -q theories/$k/$b.v tmp
+	    grep -q $k/$b.v tmp
 	    a=$?
-	    grep -q theories/$k/$b.v $HIDDEN
+	    grep -q $k/$b.v $HIDDEN
 	    h=$?
 	    if [ $a = 0 ]; then
 	        if [ $h = 0 ]; then
-                    echo Error: $FILE and $HIDDEN both mention theories/$k/$b.v; exit 1
+                    echo Error: $FILE and $HIDDEN both mention $k/$b.v; exit 1
                 else
-		    p=`echo $k | sed 's:/:.:g'`
-		    sed -e "s:theories/$k/$b.v:<a href=\"Coq.$p.$b.html\">$b</a>:g" tmp > tmp2
+		    p=`echo $k | sed 's:^[^/]*/::' | sed 's:/:.:g'`
+		    sed -e "s:$k/$b.v:<a href=\"Coq.$p.$b.html\">$b</a>:g" tmp > tmp2
 		    mv -f tmp2 tmp
                 fi
 	    else
 	        if [ $h = 0 ]; then
-		    echo Error: theories/$k/$b.v is missing in the template file
-                    exit 1
+		    echo Warning: $k/$b.v will be hidden from the index
                 else
-                    echo Error: none of $FILE and $HIDDEN mention theories/$k/$b.v
+                    echo Error: none of $FILE and $HIDDEN mention $k/$b.v
                     exit 1
 	        fi