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

8 files changed, 31 insertions, 7 deletions

diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v
index 42cf98496..d92865c5d 100755
--- a/theories/Sets/Ensembles.v
+++ b/theories/Sets/Ensembles.v
@@ -46,7 +46,7 @@ Inductive Full_set : Ensemble :=
    Leibniz equality.
    This may have to be changed if we replace U by a Setoid on U with its own
    equality eqs, with 
-      In_singleton: (y: U)(eqs x y) -> (In (Singleton x) y). *)
+      [In_singleton: (y: U)(eqs x y) -> (In (Singleton x) y)]. *)
 
 Inductive Singleton [x:U] : Ensemble :=
       In_singleton: (In (Singleton x) x).
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index 5c37b0fd9..cd7b1e23e 100755
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -78,7 +78,7 @@ Unfold meq; Unfold munion; Simpl; Auto.
 Qed.
 
 
-Require Plus. (* comm & ass of plus *)
+Require Plus. (* comm. and ass. of plus *)
 
 Lemma munion_comm : (x,y:multiset)(meq (munion x y) (munion y x)).
 Proof.
diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v
index baf28a53f..e19f73a8c 100755
--- a/theories/Sets/Permut.v
+++ b/theories/Sets/Permut.v
@@ -29,7 +29,7 @@ Hypothesis cong_right : (x,y,z:U)(cong x y)->(cong (op z x) (op z y)).
 Hypothesis cong_trans : (x,y,z:U)(cong x y)->(cong y z)->(cong x z).
 Hypothesis cong_sym : (x,y:U)(cong x y)->(cong y x).
 
-(* Remark. we do not need: Hypothesis cong_refl : (x:U)(cong x x). *)
+(* Remark. we do not need: [Hypothesis cong_refl : (x:U)(cong x x)]. *)
 
 Lemma cong_congr :
  (x,y,z,t:U)(cong x y)->(cong z t)->(cong (op x z) (op y t)).
diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v
index ddcc433b8..b490fa7a0 100755
--- a/theories/Sets/Relations_1_facts.v
+++ b/theories/Sets/Relations_1_facts.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 Require Export Relations_1.
 
diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v
index ec90057aa..588b7f431 100755
--- a/theories/Sets/Relations_2_facts.v
+++ b/theories/Sets/Relations_2_facts.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 Require Export Relations_1.
 Require Export Relations_1_facts.
diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v
index 3fe27af99..a57487d1e 100755
--- a/theories/Sets/Relations_3_facts.v
+++ b/theories/Sets/Relations_3_facts.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 Require Export Relations_1.
 Require Export Relations_1_facts.
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
index b18b5634a..12f267873 100644
--- a/theories/Sets/Uniset.v
+++ b/theories/Sets/Uniset.v
@@ -137,7 +137,7 @@ Qed.
 Hints Resolve seq_right.
 
 
-(* All the proofs that follow duplicate Multiset_of_A *)
+(* All the proofs that follow duplicate [Multiset_of_A] *)
 
 (* Here we should make uniset an abstract datatype, by hiding Charac,
    union, charac; all further properties are proved abstractly *)
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: