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

3 files changed, 33 insertions, 9 deletions

diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index 565a32404..9af874a3f 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -81,12 +81,12 @@ Section first_definitions.
 		      else (set_add a1 (set_diff x1 y))
     end.
    
-  (** 
+  (*i
   Inductive set_In : A -> set -> Prop :=
     set_In_singl : (a:A)(x:set)(set_In a (cons a (nil A))) 
   | set_In_add : (a,b:A)(x:set)(set_In a x)->(set_In a (set_add b x))
   .
-  **)
+  i*)
 
   Definition set_In : A -> set -> Prop := (In 1!A).
 
@@ -324,7 +324,7 @@ Section other_definitions.
 
   Definition set_prod : (set A) -> (set B) -> (set A*B) := (list_prod 1!A 2!B).
 
-  (* B^A, set of applications from A to B *)
+  (* [B^A], set of applications from [A] to [B] *)
   Definition set_power : (set A) -> (set B) -> (set (set A*B)) := 
     (list_power 1!A 2!B).
 
diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v
index 7c11eb489..267988cdb 100644
--- a/theories/Lists/PolyList.v
+++ b/theories/Lists/PolyList.v
@@ -407,7 +407,7 @@ Lemma nth_S_cons :
 Simpl; Auto.
 Save.
 
-(***** 
+(*i
 Lemma nth_In :
   (n:nat)(l:list)(d:A)(lt n (length l))->(In (nth n l d) l).
 
@@ -421,7 +421,7 @@ Unfold lt; Induction l;
 [ Simpl; Intros; Inversion H
 | Simpl; Intros;
 ].
-******)
+i*)
 
 
 (*********************************************)
@@ -575,8 +575,8 @@ Induction l;
 ].
 Save.
 
-(* (list_power x y) is y^x, or the set of sequences of elts of y
-  indexed by elts of x, sorted in lexicographic order. *)
+(* [(list_power x y)] is [y^x], or the set of sequences of elts of [y]
+  indexed by elts of [x], sorted in lexicographic order. *)
 
 Fixpoint list_power [A,B:Set; l:(list A)] : (list B)->(list (list A*B)) :=
   [l']Cases l of
@@ -606,7 +606,7 @@ Fixpoint fold_right [l:(list B)] : A :=
   end.
 End Fold_Right_Recursor.
 
-(*
+(*i
 Theorem fold_symmetric :
   (A:Set)(f:A->A->A)
    ((x,y,z:A)(f x (f y z))=(f (f x y) z))
@@ -625,7 +625,7 @@ Do 2 Rewrite H.
 Rewrite (H0 a1 a3).
 Reflexivity.
 Save.
-*)
+i*)
 
 End Functions_on_lists.
 
diff --git a/theories/Lists/intro.tex b/theories/Lists/intro.tex
new file mode 100755
index 000000000..2930326e1
--- /dev/null
+++ b/theories/Lists/intro.tex
@@ -0,0 +1,24 @@
+\section{Lists}\label{Lists}
+
+The LISTS library includes the following files:
+
+\begin{itemize}
+
+\item {\tt Lists.v} THIS OLD LIBRARY IS HERE ONLY FOR COMPATIBILITY
+  WITH OLDER VERSIONS OF COQS. THE USER SHOULD USE POLYLIST INSTEAD.
+
+\item {\tt PolyLists.v} contains definitions of (polymorphic) lists, 
+  functions on lists such as head, tail, map, append and prove some
+  properties of these functions. Implicit arguments are used in this
+  library, so you should read the Referance Manual about implicit
+  arguments before using it.
+
+\item {\tt TheoryList.v} contains complementary results on lists. Here
+  a more theoric point of view is assumed : one extracts functions
+  from propositions, rather than defining functions and then prove them.
+
+\item {\tt Streams.v} defines the type of infinite lists (streams). It is a
+  coinductive type. Basic facts are stated and proved. The streams are
+  also polymorphic.
+
+\end{itemize}