From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001
From: Stephane Glondu
Date: Sun, 1 Feb 2009 00:54:40 +0100
Subject: Imported Upstream version 8.2~rc2+dfsg
---
doc/stdlib/Library.tex | 4 ++--
doc/stdlib/index-list.html.template | 15 ++++++++-------
doc/stdlib/make-library-files | 6 +++---
3 files changed, 13 insertions(+), 12 deletions(-)
(limited to 'doc')
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 Require Import command.
theories/Logic/Description.v
theories/Logic/Epsilon.v
theories/Logic/IndefiniteDescription.v
+ theories/Logic/FunctionalExtensionality.v
Bool:
@@ -256,12 +257,7 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
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
@@ -273,8 +269,10 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
theories/Relations/Relation_Operators.v
theories/Relations/Relations.v
theories/Relations/Operators_Properties.v
+
Sets:
@@ -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
Setoids:
+
theories/Setoids/Setoid.v
+ theories/Setoids/Setoid_tac.v
+ theories/Setoids/Setoid_Prop.v
Lists:
@@ -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
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
--
cgit v1.2.3