Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

1 files changed, 26 insertions, 8 deletions

diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index
index 8e496fdd..1a70567f 100755
--- a/doc/stdlib/make-library-index
+++ b/doc/stdlib/make-library-index
@@ -3,37 +3,55 @@
 # Instantiate links to library files in index template
 
 FILE=$1
+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 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="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/::"`
 
 for k in $LIBDIRS; do
     i=theories/$k
     echo $i
     
     d=`basename $i`
-    if [ "$d" != "Num" -a "$d" != "CVS" ]; then
+    if [ "$d" != "CVS" ]; then
+      ls $i | grep -q \.v'$'
+      if [ $? = 0 ]; then
 	for j in $i/*.v; do
 	    b=`basename $j .v`
 	    rm -f tmp2
 	    grep -q theories/$k/$b.v tmp
 	    a=$?
+	    grep -q theories/$k/$b.v $HIDDEN
+	    h=$?
 	    if [ $a = 0 ]; then
-		p=`echo $k | sed 's:/:.:g'`
-		sed -e "s:theories/$k/$b.v:<a href=\"Coq.$p.$b.html\">$b</a>:g" tmp > tmp2
-		mv -f tmp2 tmp
+	        if [ $h = 0 ]; then
+                    echo Error: $FILE and $HIDDEN both mention theories/$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
+		    mv -f tmp2 tmp
+                fi
 	    else
-		echo Warning: theories/$k/$b.v is missing in the template file
-	    fi
+	        if [ $h = 0 ]; then
+		    echo Error: theories/$k/$b.v is missing in the template file
+                    exit 1
+                else
+                    echo Error: none of $FILE and $HIDDEN mention theories/$k/$b.v
+                    exit 1
+	        fi
+
+            fi
 	done
+      fi
     fi
     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
+if [ $? = 0 ]; then echo Error: extra files:; echo $a; exit 1; fi
 mv tmp $FILE
 echo Done