documentation automatique de la bibliothèque standard

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1578 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 24 insertions, 0 deletions

diff --git a/theories/Sets/intro.tex b/theories/Sets/intro.tex
new file mode 100755
index 000000000..83c2177fd
--- /dev/null
+++ b/theories/Sets/intro.tex
@@ -0,0 +1,24 @@
+\section{Sets}\label{Sets}
+
+This is a library on sets defined by their characteristic predicate.
+It contains the following modules:
+
+\begin{itemize}
+\item {\tt Ensembles.v}
+\item {\tt Constructive\_sets.v}, {\tt Classical\_sets.v}
+\item {\tt Relations\_1.v}, {\tt Relations\_2.v}, 
+ {\tt Relations\_3.v}, {\tt Relations\_1\_facts.v},  \\
+ {\tt Relations\_2\_facts.v}, {\tt Relations\_3\_facts.v}
+\item {\tt Partial\_Order.v}, {\tt Cpo.v}
+\item {\tt Powerset.v}, {\tt Powerset\_facts.v}, 
+ {\tt Powerset\_Classical\_facts.v}
+\item {\tt Finite\_sets.v}, {\tt Finite\_sets\_facts.v}
+\item {\tt Image.v}
+\item {\tt Infinite\_sets.v}
+\item {\tt Integers.v}
+\end{itemize}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: t
+%%% End: