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

33 files changed, 271 insertions, 90 deletions

diff --git a/contrib/correctness/Arrays.v b/contrib/correctness/Arrays.v
index 794131428..10ba81719 100644
--- a/contrib/correctness/Arrays.v
+++ b/contrib/correctness/Arrays.v
@@ -10,9 +10,9 @@
 
 (* $Id$ *)
 
-(*******************************************)
-(* Functional arrays, for use in Programs. *)
-(*******************************************)
+(**********************************************)
+(* Functional arrays, for use in Correctness. *)
+(**********************************************)
 
 (* This is an axiomatization of arrays.
  *
@@ -77,4 +77,4 @@ Grammar constr constr0 :=
 
 Syntax constr level 0 :
   array_access
-    [ << (APPLIST access ($VAR $t) $c) >> ] -> [ $t "#[" $c:L "]" ].
+    [ << (access ($VAR $t) $c) >> ] -> [ "#" $t "[" $c:L "]" ].
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 80399858c..a91bceb8e 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -12,6 +12,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
+open Options
 open Names
 open Vernacentries
 open Reduction
@@ -483,12 +484,12 @@ open Declare
 
 let is_assumed global ids =
   if List.length ids = 1 then
-    mSGNL [< 'sTR(if global then "A global variable " else ""); 
-	     pr_id (List.hd ids); 'sTR" is assumed" >]
+    mSGNL [< 'sTR (if global then "A global variable " else ""); 
+	     pr_id (List.hd ids); 'sTR " is assumed" >]
   else
-    mSGNL [< 'sTR(if global then "Some global variables " else "");
-	     (prlist_with_sep (fun () -> [< 'sTR", " >]) pr_id ids);
-	     'sTR" are assumed" >]
+    mSGNL [< 'sTR (if global then "Some global variables " else "");
+	     prlist_with_sep (fun () -> [< 'sTR ", " >]) pr_id ids;
+	     'sTR " are assumed" >]
 
 let add = vinterp_add
 
@@ -507,44 +508,47 @@ let _ = add "CORRECTNESS"
 	   fun () -> Ptactic.correctness s (out_prog d) (Some tac)
        | _ -> assert false)
 
-let _ = add "SHOWPROGRAMS"
-     (function
-	 [] -> fun () ->
-	   fold_all 
-	     (fun (id,v) _ -> 
-		mSGNL [< 'sTR(string_of_id id); 'sTR" : "; 
-			 hOV 2 (match v with TypeV v -> pp_type_v v
-				           | Set -> [< 'sTR"Set" >]);
-			 'fNL >])
-	     Penv.empty ()
+let _ = 
+  add "SHOWPROGRAMS"
+    (function
+       | [] -> 
+	   (fun () ->
+	      fold_all 
+		(fun (id,v) _ -> 
+		   mSGNL [< pr_id id; 'sTR " : "; 
+			    hOV 2 (match v with TypeV v -> pp_type_v v
+				     | Set -> [< 'sTR "Set" >]);
+			    'fNL >])
+		Penv.empty ())
        | _ -> assert false)
 
-let _ = add "PROGVARIABLE"
-     (function
-	 [ VARG_VARGLIST l; VARG_DYN d ] ->
-	   fun () ->
-	     let ids = List.map (function VARG_IDENTIFIER id -> id 
-				   | _ -> assert false) l in
-	     List.iter
-	       (fun id -> if Penv.is_global id then
-		  Util.errorlabstrm "PROGVARIABLE"
-		    [< 'sTR"Clash with previous constant "; pr_id id >])
-	       ids;
-	     let v = Pdb.db_type_v [] (out_typev d) in
-	     let env = empty in
-	     let ren = update empty_ren "" [] in
-	     let v = Ptyping.cic_type_v env ren v in
-	     if not (is_mutable v) then begin
-	       let c = trad_ml_type_v ren env v in
-	       List.iter 
-		 (fun id -> ignore (Declare.declare_parameter id c)) ids;
-	       is_assumed false ids
-	     end;
-	     if not (is_pure v) then begin
-	       List.iter (fun id -> ignore (Penv.add_global id v None)) ids;
-	       is_assumed true ids
-	     end
-  
+let id_of_varg = function VARG_IDENTIFIER id -> id | _ -> assert false
+    
+let _ = 
+  add "PROGVARIABLE"
+    (function
+       | [ VARG_VARGLIST l; VARG_DYN d ] ->
+	   (fun () ->
+	      let ids = List.map id_of_varg l in
+	      List.iter
+		(fun id -> if Penv.is_global id then
+		   Util.errorlabstrm "PROGVARIABLE"
+		     [< 'sTR"Clash with previous constant "; pr_id id >])
+		ids;
+	      let v = Pdb.db_type_v [] (out_typev d) in
+	      let env = empty in
+	      let ren = update empty_ren "" [] in
+	      let v = Ptyping.cic_type_v env ren v in
+	      if not (is_mutable v) then begin
+		let c = trad_ml_type_v ren env v in
+		List.iter 
+		  (fun id -> ignore (Declare.declare_parameter id c)) ids;
+		if_verbose (is_assumed false) ids
+	      end;
+	      if not (is_pure v) then begin
+		List.iter (fun id -> ignore (Penv.add_global id v None)) ids;
+		if_verbose (is_assumed true) ids
+	      end)
        | _ -> assert false)
 
 open Vernac
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index 3e8d174c8..041d24349 100755
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -38,17 +38,21 @@ Theorem  well_founded_gtof : (well_founded A gtof).
 Proof well_founded_ltof.
 
 (* It is possible to directly prove the induction principle going
-   back to primitive recursion on natural numbers (induction_ltof1)
+   back to primitive recursion on natural numbers ([induction_ltof1])
    or to use the previous lemmas to extract a program with a fixpoint
-   (induction_ltof2) 
-the ML-like program for induction_ltof1 is :
+   ([induction_ltof2]) 
+the ML-like program for [induction_ltof1] is :
+\begin{verbatim}
    let induction_ltof1 F a = indrec ((f a)+1) a 
    where rec indrec = 
         function 0    -> (function a -> error)
                |(S m) -> (function a -> (F a (function y -> indrec y m)));;
-the ML-like program for induction_ltof2 is :
+\end{verbatim}
+the ML-like program for [induction_ltof2] is :
+\begin{verbatim}
    let induction_ltof2 F a = indrec a
    where rec indrec a = F a indrec;;
+\end{verbatim}
 *)
 
 Theorem induction_ltof1 : (P:A->Set)((x:A)((y:A)(ltof y x)->(P y))->(P x))->(a:A)(P a).
diff --git a/theories/Arith/intro.tex b/theories/Arith/intro.tex
new file mode 100755
index 000000000..7d922c5b6
--- /dev/null
+++ b/theories/Arith/intro.tex
@@ -0,0 +1,55 @@
+\section{Arith}\label{Arith}
+
+The {\tt Arith} library deals with various arithmetical notions and 
+their properties.
+
+\subsection*{Standard {\tt Arith} library}
+
+The following files are automatically loaded by {\tt Require Arith}.
+
+\begin{itemize}
+
+\item {\tt Le.v} states and proves properties of the large order {\tt le}.
+
+\item {\tt Lt.v} states and proves properties of the strict order {\tt 
+lt} (especially, the relationship with {\tt le}).
+
+\item {\tt Plus.v} states and proves properties on the addition.
+
+\item {\tt Gt.v} states and proves properties on the strict order {\tt gt}.
+
+\item {\tt Minus.v} defines the difference on 
+{\tt nat} and proves properties of it. On {\tt nat}, {\tt (minus n p)} is 
+{\tt O} if {\tt n} $<$ {\tt p}.
+
+\item {\tt Mult.v} states and proves properties on the multiplication.
+
+\item {\tt Between.v} defines modalities on {\tt nat} and proves properties 
+of them.
+
+\end{itemize}
+
+\subsection*{Additional {\tt Arith} library}
+
+\begin{itemize}
+
+\item {\tt Compare.v}, {\tt Compare\_dec.v} and {\tt Peano\_dec.v} state
+and prove various decidability results on {\tt nat}.
+
+\item {\tt Wf\_nat.v} states and proves various induction and recursion 
+principles on {\tt nat}. Especially, recursion for objects measurable by 
+a natural number and recursion on {\tt nat * nat} are provided.
+
+\item {\tt Min.v} defines the minimum of two natural numbers and proves 
+properties of it. 
+
+\item {\tt Eqnat.v} defines a specific equality on {\tt nat} and shows 
+the equivalence with Leibniz' equality.
+
+\item {\tt Euclid\_def.v} and {\tt Euclid\_prog.v} prove that the euclidean
+division specification is realisable. Conversely, {\tt Div.v} exhibits
+two different algorithms and semi-automatically reconstruct the proof of
+their correctness. These files emphasize the extraction of program vs
+reconstruction of proofs paradigm.
+
+\end{itemize}
diff --git a/theories/Bool/intro.tex b/theories/Bool/intro.tex
new file mode 100644
index 000000000..22ee38aab
--- /dev/null
+++ b/theories/Bool/intro.tex
@@ -0,0 +1,16 @@
+\section{Bool}\label{Bool}
+
+The BOOL library includes the following files:
+
+\begin{itemize}
+
+\item {\tt Bool.v} defines standard operations on booleans and states
+  and proves simple facts on them.
+\item {\tt IfProp.v} defines a disjunction which contains its proof
+  and states its properties.
+\item {\tt Zerob.v} defines the test against 0 on natural numbers and
+  states and proves properties of it.
+\item {\tt Orb.v} states and proves facts on the boolean or.
+\item {\tt DecBool.v} defines a conditional from a proof of
+  decidability and states its properties.
+\end{itemize}
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index 08a054900..35a25a46f 100755
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -99,11 +99,13 @@ Definition eqT_ind_r : (A:Type)(x:A)(P:A->Prop)(P x)->(y:A)(eqT ? y x)->(P y).
 Intros A x P H y H0; Case sym_eqT with 1:=H0; Trivial.
 Defined.
 
-(*** not allowed because of dependencies 
+(* not allowed because of dependencies:
+\begin{verbatim}
 Definition eqT_rec_r : (A:Type)(x:A)(P:A->Set)(P x)->(y:A)y==x -> (P y).
 Intros A x P H y H0; Case sym_eqT with 1:=H0; Trivial.
 Defined.
-****)
+\end{verbatim}
+*)
 
 (* Some datatypes at the [Type] level *)
 
diff --git a/theories/Init/Logic_TypeSyntax.v b/theories/Init/Logic_TypeSyntax.v
index a1cce77a5..1c3f23dac 100644
--- a/theories/Init/Logic_TypeSyntax.v
+++ b/theories/Init/Logic_TypeSyntax.v
@@ -10,7 +10,7 @@
 
 Require Logic_Type.
 
-(* Parsing of things in Logic_type.v *)
+(* Parsing of things in [Logic_type.v] *)
 
 Grammar command command1 :=
   eqT_expl [ "<" lcommand($l1) ">" command0($c1) "==" command0($c2) ] ->
@@ -34,7 +34,7 @@ with command10 :=
 | exT2implicit [ "EXT" ident($v) "|" command($c1) "&" 
            command($c2) ] -> [<<(exT2 ? [$v]$c1 [$v]$c2)>>].
 
-(* Pretty-printing of things in Logic_type.v *)
+(* Pretty-printing of things in [Logic_type.v] *)
 
 Syntax constr
   level 10:
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index fc99d1a48..dcfbe5e99 100755
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -131,7 +131,7 @@ Inductive le [n:nat] : nat -> Prop
      | le_S : (m:nat)(le n m)->(le n (S m)).
 
 Hint constr_le : core v62 := Constructors le.
-(* equivalent to : "Hints Resolve le_n le_S : core v62." *)
+(*i equivalent to : "Hints Resolve le_n le_S : core v62." i*)
 
 Definition lt := [n,m:nat](le (S n) m).
 Hints Unfold lt : core v62.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 1f1ad6ce5..eb7edad11 100755
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -94,12 +94,12 @@ Syntactic Definition ProjS2 := (projS2 ? ?).
 
 Section Extended_booleans.
 
-  (* Syntax sumbool "{_}+{_}". *)
+  (* Syntax sumbool ["{_}+{_}"]. *)
   Inductive sumbool [A,B:Prop] : Set
       := left  : A -> (sumbool A B) 
        | right : B -> (sumbool A B).
 
-  (* Syntax sumor "_+{_}". *)
+  (* Syntax sumor ["_+{_}"]. *)
   Inductive sumor [A:Set;B:Prop] : Set
       := inleft  : A -> (sumor A B) 
        | inright : B -> (sumor A B).
@@ -210,9 +210,9 @@ Proof.
   Intros A B C F AB; Apply F; Elim AB; Auto.
 Qed.
 
-(** is now a theorem
+(*i is now a theorem
 Axiom eq_rec : (A:Set)(a:A)(P:A->Set)(P a)->(b:A) a=b -> (P b).
-**)
+i*)
 
 Hints Resolve left right inleft inright : core v62.
 
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index eb0be95cf..214c33117 100755
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -33,7 +33,7 @@ Chapter Well_founded.
  Defined.
 
   (* the informative elimination :
-     let Acc_rec F = let rec wf x = F x wf in wf *)
+     [let Acc_rec F = let rec wf x = F x wf in wf] *)
 
  Section AccRec.
   Variable P : A -> Set.
@@ -76,7 +76,7 @@ Fixpoint Fix_F [x:A;r:(Acc x)] : (P x) :=
 
 Definition fix := [x:A](Fix_F x (Rwf x)).
 
-(* Proof that well_founded_induction satisfies the fixpoint equation. 
+(* Proof that [well_founded_induction] satisfies the fixpoint equation. 
    It requires an extra property of the functional *)
 
 Hypothesis F_ext : 
diff --git a/theories/IntMap/Adalloc.v b/theories/IntMap/Adalloc.v
index 58d02676e..47cff4f8e 100644
--- a/theories/IntMap/Adalloc.v
+++ b/theories/IntMap/Adalloc.v
@@ -209,7 +209,8 @@ Section AdAlloc.
     Unfold in_dom. Intro. Rewrite (ad_alloc_opt_allocates_1 m). Reflexivity.
   Qed.
 
-  (* Moreover, this is optimal: all addresses below (ad_alloc_opt m) are in dom m: *)
+  (* Moreover, this is optimal: all addresses below [(ad_alloc_opt m)]
+     are in [dom m]: *)
 
   Lemma convert_xH : (convert xH)=(1).
   Proof.
diff --git a/theories/IntMap/Adist.v b/theories/IntMap/Adist.v
index b9cee92ef..ec08fb35f 100644
--- a/theories/IntMap/Adist.v
+++ b/theories/IntMap/Adist.v
@@ -258,10 +258,10 @@ Qed.
 (*s $d$ is an ultrametric distance, that is, not only $d(a,a')\leq d(a,a'')+d(a'',a')$,
   but in fact $d(a,a')\leq max(d(a,a''),d(a'',a'))$.
   This means that $min(pd(a,a''),pd(a'',a'))<=pd(a,a')$ (lemma [ad_pdist_ultra] below).
-  This follows from the fact that $a \Ra |a| = 1/2^\TT{ad\_plength}(a))$
+  This follows from the fact that $a \Ra |a| = 1/2^\texttt{ad\_plength}(a))$
   is an ultrametric norm, i.e. that $|a-a'| \leq max (|a-a''|, |a''-a'|)$,
   or equivalently that $|a+b|<=max(|a|,|b|)$, i.e. that
-  min $(\TT{ad\_plength}(a), \TT{ad\_plength}(b)) \leq \TT{ad\_plength} (a~\TT{xor}~ b)$
+  min $(\texttt{ad\_plength}(a), \texttt{ad\_plength}(b)) \leq \texttt{ad\_plength} (a~\texttt{xor}~ b)$
   (lemma [ad_plength_ultra]).
 *)
 
diff --git a/theories/IntMap/Map.v b/theories/IntMap/Map.v
index 2f1c47bb6..ca436cddb 100644
--- a/theories/IntMap/Map.v
+++ b/theories/IntMap/Map.v
@@ -181,7 +181,7 @@ Section MapDefs.
     Intros. Case b; Trivial.
   Qed.
 
-  (*
+  (*i
   Lemma MapGet_M2_bit_0_1' : (m,m',m'',m''':Map)
       (a:ad) (MapGet (if (ad_bit_0 a) then (M2 m m') else (M2 m'' m''')) a)=
              (MapGet (if (ad_bit_0 a) then m' else m'') (ad_div_2 a)).
@@ -192,7 +192,7 @@ Section MapDefs.
     Intros. Rewrite H0. Apply MapGet_M2_bit_0_1. Assumption.
     Case (ad_bit_0 a); Auto.
   Qed.
-  *)
+  i*)
 
   Lemma MapGet_if_same : (m:Map) (b:bool) (a:ad) (MapGet (if b then m else m) a)=(MapGet m a).
   Proof.
diff --git a/theories/IntMap/intro.tex b/theories/IntMap/intro.tex
new file mode 100644
index 000000000..cfaae2468
--- /dev/null
+++ b/theories/IntMap/intro.tex
@@ -0,0 +1,5 @@
+\section{IntMap}\label{IntMap}
+
+This library contains a data structure for finite sets implemented by
+an efficient structure of map (trees indexed by binary integers).
+
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}
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index 0b5c56ae1..a35993acd 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -8,14 +8,14 @@
 
 (* $Id$ *)
 
-(* We prove that there is only one proof of x=x, i.e (refl_equal ? x).
-   This holds if the equality upon the set of x is decidable.
+(* We prove that there is only one proof of [x=x], i.e [(refl_equal ? x)].
+   This holds if the equality upon the set of [x] is decidable.
    A corollary of this theorem is the equality of the right projections
    of two equal dependent pairs.
 
-   Author:   Thomas Kleymann <tms@dcs.ed.ac.uk> in Lego
+   Author:   Thomas Kleymann \verb!<tms@dcs.ed.ac.uk>! in Lego
              adapted to Coq by B. Barras
-   Credit:   Proofs up to K_dec follows an outline by Michael Hedberg
+   Credit:   Proofs up to [K_dec] follows an outline by Michael Hedberg
 *)
 
 
@@ -26,7 +26,7 @@ Scheme or_indd := Induction for or Sort Prop.
 
 Implicit Arguments On.
 
-  (* Bijection between eq and eqT *)
+  (* Bijection between [eq] and [eqT] *)
   Definition eq2eqT: (A:Set)(x,y:A)x=y->x==y :=
     [A,x,_,eqxy]<[y:A]x==y>Cases eqxy of refl_equal => (refl_eqT ? x) end.
 
diff --git a/theories/Logic/intro.tex b/theories/Logic/intro.tex
new file mode 100755
index 000000000..23f43a78c
--- /dev/null
+++ b/theories/Logic/intro.tex
@@ -0,0 +1,8 @@
+\section{Logic}\label{Logic}
+
+This library deals with classical logic and its properties.
+The main file is {\tt Classical.v}.
+
+This library also provides some facts on an equality which contains its
+own proof. See the file {\tt Eqdep.v}.
+
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 3e92a2a2f..910fda861 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -26,9 +26,11 @@ Fixpoint fact [n:nat]:nat:=
   end.
 
 (*********)
-(*Lemma mult_neq_O:(n,m:nat)~n=O->~m=O->~(mult n m)=O.
+(*i
+Lemma mult_neq_O:(n,m:nat)~n=O->~m=O->~(mult n m)=O.
 Double Induction 1 2;Simpl;Auto.
-Save.*)
+Save.
+i*)
  
 (*********)
 Lemma fact_neq_0:(n:nat)~(fact n)=O.
diff --git a/theories/Reals/intro.tex b/theories/Reals/intro.tex
new file mode 100644
index 000000000..433172585
--- /dev/null
+++ b/theories/Reals/intro.tex
@@ -0,0 +1,4 @@
+\section{Reals}\label{Reals}
+
+This library contains an axiomatization of real numbers.
+The main file is \texttt{Reals.v}.
diff --git a/theories/Relations/intro.tex b/theories/Relations/intro.tex
new file mode 100755
index 000000000..5056f36f9
--- /dev/null
+++ b/theories/Relations/intro.tex
@@ -0,0 +1,23 @@
+\section{Relations}\label{Relations}
+
+This library develops closure properties of relations.
+
+\begin{itemize}
+\item {\tt Relation\_Definitions.v} deals with the general notions
+  about binary relations (orders, equivalences, ...)
+
+\item {\tt Relation\_Operators.v} and {\tt Rstar.v} define various
+  closures of relations (by symmetry, by transitivity, ...) and
+  lexicographic orderings.
+
+\item {\tt Operators\_Properties.v} states and proves facts on the
+  various closures of a relation.
+
+\item {\tt Relations.v} puts {\tt Relation\_Definitions.v}, {\tt
+    Relation\_Operators.v} and \\
+    {\tt Operators\_Properties.v} together.
+
+\item {\tt Newman.v} proves Newman's lemma on noetherian and locally
+  confluent relations.
+
+\end{itemize}
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: 
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v
index a51b876ab..419f545f5 100644
--- a/theories/Wellfounded/Lexicographic_Product.v
+++ b/theories/Wellfounded/Lexicographic_Product.v
@@ -91,7 +91,7 @@ Section Wf_Symmetric_Product.
 
   Syntactic Definition Symprod := (symprod A B leA leB).
 
-(*
+(*i
   Local sig_prod:=
          [x:A*B]<{_:A&B}>Case x of [a:A][b:B](existS A [_:A]B a b) end.
 
@@ -108,7 +108,7 @@ Proof.
 
  (Apply right_lex;Auto with sets).
 Save.
-*)
+i*)
 
   Lemma Acc_symprod: (x:A)(Acc A leA x)->(y:B)(Acc B leB y)
                         ->(Acc (A*B) Symprod (x,y)).
diff --git a/theories/Wellfounded/intro.tex b/theories/Wellfounded/intro.tex
new file mode 100755
index 000000000..126071e28
--- /dev/null
+++ b/theories/Wellfounded/intro.tex
@@ -0,0 +1,4 @@
+\section{Well-founded relations}\label{Wellfounded}
+
+This library gives definitions and results about well-founded relations.
+
diff --git a/theories/Zarith/intro.tex b/theories/Zarith/intro.tex
new file mode 100755
index 000000000..9694eaac8
--- /dev/null
+++ b/theories/Zarith/intro.tex
@@ -0,0 +1,5 @@
+The {\tt ZArith} library deals with binary integers (those used
+by the {\tt Omega} decision tactic).
+Here are defined various arithmetical notions and their properties,
+similar to those of {\tt Arith}.
+