Library doc adjustments (until page 140)

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

30 files changed, 114 insertions, 99 deletions

diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 67121590ee..1b70e1512b 100755
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -22,8 +22,7 @@ Intros y H ; Elim (plus_n_Sm m y) ; Auto with arith.
 Qed.
 Hints Immediate plus_sym : arith v62.
 
-Lemma plus_Snm_nSm : 
-  (n,m:nat)(plus (S n) m)=(plus n (S m)).
+Lemma plus_Snm_nSm : (n,m:nat)(plus (S n) m)=(plus n (S m)).
 Intros.
 Simpl.
 Rewrite -> (plus_sym n m).
@@ -143,7 +142,8 @@ Proof.
   Intros. Discriminate H.
 Qed.
 
-Lemma plus_is_one : (m,n:nat) (plus m n)=(S O) -> {m=O /\ n=(S O)}+{m=(S O) /\ n=O}.
+Lemma plus_is_one : 
+      (m,n:nat) (plus m n)=(S O) -> {m=O /\ n=(S O)}+{m=(S O) /\ n=O}.
 Proof.
   Destruct m; Auto.
   Destruct n; Auto.
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index 2f100ebc52..ff502af946 100755
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -55,7 +55,8 @@ the ML-like program for [induction_ltof2] is :
 \end{verbatim}
 *)
 
-Theorem induction_ltof1 : (P:A->Set)((x:A)((y:A)(ltof y x)->(P y))->(P x))->(a:A)(P a).
+Theorem induction_ltof1 
+  : (P:A->Set)((x:A)((y:A)(ltof y x)->(P y))->(P x))->(a:A)(P a).
 Proof.
 Intros P F; Cut (n:nat)(a:A)(lt (f a) n)->(P a).
 Intros H a;  Apply (H (S (f a))); Auto with arith.
@@ -68,14 +69,16 @@ Apply Hm.
 Apply lt_le_trans with (f a); Auto with arith.
 Qed. 
 
-Theorem induction_gtof1 : (P:A->Set)((x:A)((y:A)(gtof y x)->(P y))->(P x))->(a:A)(P a).
+Theorem induction_gtof1 
+  : (P:A->Set)((x:A)((y:A)(gtof y x)->(P y))->(P x))->(a:A)(P a).
 Proof induction_ltof1.
 
 Theorem induction_ltof2 
-   : (P:A->Set)((x:A)((y:A)(ltof y x)->(P y))->(P x))->(a:A)(P a).
+  : (P:A->Set)((x:A)((y:A)(ltof y x)->(P y))->(P x))->(a:A)(P a).
 Proof (well_founded_induction A ltof well_founded_ltof).
 
-Theorem induction_gtof2 : (P:A->Set)((x:A)((y:A)(gtof y x)->(P y))->(P x))->(a:A)(P a).
+Theorem induction_gtof2 
+  : (P:A->Set)((x:A)((y:A)(gtof y x)->(P y))->(P x))->(a:A)(P a).
 Proof induction_ltof2.
 
 
diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v
index bcbe0f7140..f9c5e39763 100755
--- a/theories/Bool/IfProp.v
+++ b/theories/Bool/IfProp.v
@@ -32,7 +32,7 @@ Inversion H.
 Assumption.
 Save.
 
-Lemma Ifprop_false : (A,B:Prop)(IfProp A B false) -> B.
+Lemma IfProp_false : (A,B:Prop)(IfProp A B false) -> B.
 Intros.
 Inversion H.
 Assumption.
diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v
index e91b3fb1a6..9c6cd1f427 100644
--- a/theories/Bool/Sumbool.v
+++ b/theories/Bool/Sumbool.v
@@ -9,8 +9,7 @@
 (*i $Id$ i*)
 
 (* Here are collected some results about the type sumbool (see INIT/Specif.v)
- * 
- * (sumbool A B), which is written {A}+{B}, is the informative
+ * [sumbool A B], which is written [{A}+{B}], is the informative
  * disjunction "A or B", where A and B are logical propositions.
  * Its extraction is isomorphic to the type of booleans.
  *)
@@ -24,7 +23,7 @@ Save.
 
 Hints Resolve sumbool_of_bool : bool.
 
-(* pourquoi ce machin-la est dans BOOL et pas dans LOGIC ?  Papageno *)
+(*i pourquoi ce machin-la est dans BOOL et pas dans LOGIC ?  Papageno i*)
 
 (* Logic connectives on type sumbool *)
 
diff --git a/theories/IntMap/Addec.v b/theories/IntMap/Addec.v
index abbe450816..72ad3d9866 100644
--- a/theories/IntMap/Addec.v
+++ b/theories/IntMap/Addec.v
@@ -73,7 +73,8 @@ Proof.
   Intros. Rewrite (ad_xor_eq a a' H). Apply ad_eq_correct.
 Qed.
 
-Lemma ad_xor_eq_false : (a,a':ad) (p:positive) (ad_xor a a')=(ad_x p) -> (ad_eq a a')=false.
+Lemma ad_xor_eq_false 
+  : (a,a':ad) (p:positive) (ad_xor a a')=(ad_x p) -> (ad_eq a a')=false.
 Proof.
   Intros. Elim (sumbool_of_bool (ad_eq a a')). Intro H0.
   Rewrite (ad_eq_complete a a' H0) in H. Rewrite (ad_xor_nilpotent a') in H. Discriminate H.
@@ -115,14 +116,16 @@ Proof.
   Intro H0. Rewrite ad_eq_comm. Assumption.
 Qed.
 
-Lemma ad_bit_0_neq : (a,a':ad) (ad_bit_0 a)=false -> (ad_bit_0 a')=true -> (ad_eq a a')=false.
+Lemma ad_bit_0_neq 
+  : (a,a':ad) (ad_bit_0 a)=false -> (ad_bit_0 a')=true -> (ad_eq a a')=false.
 Proof.
   Intros. Elim (sumbool_of_bool (ad_eq a a')). Intro H1. Rewrite (ad_eq_complete ? ? H1) in H.
   Rewrite H in H0. Discriminate H0.
   Trivial.
 Qed.
 
-Lemma ad_div_eq : (a,a':ad) (ad_eq a a')=true -> (ad_eq (ad_div_2 a) (ad_div_2 a'))=true.
+Lemma ad_div_eq 
+  : (a,a':ad) (ad_eq a a')=true -> (ad_eq (ad_div_2 a) (ad_div_2 a'))=true.
 Proof.
   Intros. Cut a=a'. Intros. Rewrite H0. Apply ad_eq_correct.
   Apply ad_eq_complete. Exact H.
diff --git a/theories/IntMap/Addr.v b/theories/IntMap/Addr.v
index debaed16cf..026b0ef16d 100644
--- a/theories/IntMap/Addr.v
+++ b/theories/IntMap/Addr.v
@@ -7,7 +7,7 @@
 (***********************************************************************)
 (*i 	$Id$	 i*)
 
-(*s Representation of adresses by [positive] the type of binary numbers *)
+(*s Representation of adresses by the [positive] type of binary numbers *)
 
 Require Bool.
 Require ZArith.
@@ -200,7 +200,8 @@ Proof.
   Case p; Trivial.
 Qed.
 
-Lemma ad_xor_sem_3 : (p:positive) (a':ad) (ad_bit (ad_xor (ad_x (xO p)) a') O)=(ad_bit a' O).
+Lemma ad_xor_sem_3 
+  : (p:positive) (a':ad) (ad_bit (ad_xor (ad_x (xO p)) a') O)=(ad_bit a' O).
 Proof.
   Intros. Case a'. Trivial.
   Simpl. Intro. 
@@ -219,7 +220,8 @@ Proof.
   Case (p_xor p p1); Trivial.
 Qed.
 
-Lemma ad_xor_sem_5 : (a,a':ad) (ad_bit (ad_xor a a') O)=(adf_xor (ad_bit a) (ad_bit a') O).
+Lemma ad_xor_sem_5 
+  : (a,a':ad) (ad_bit (ad_xor a a') O)=(adf_xor (ad_bit a) (ad_bit a') O).
 Proof.
   Induction a. Intro. Change (ad_bit a' O)=(xorb false (ad_bit a' O)). Rewrite false_xorb. Trivial.
   Intro. Case p. Exact ad_xor_sem_4.
@@ -258,7 +260,8 @@ Proof.
   Unfold adf_xor. Unfold 2 ad_bit. Unfold ad_bit_1. Rewrite false_xorb. Simpl.   Case p; Trivial.
 Qed.
 
-Lemma ad_xor_semantics : (a,a':ad) (eqf (ad_bit (ad_xor a a')) (adf_xor (ad_bit a) (ad_bit a'))).
+Lemma ad_xor_semantics 
+  : (a,a':ad) (eqf (ad_bit (ad_xor a a')) (adf_xor (ad_bit a) (ad_bit a'))).
 Proof.
   Unfold eqf. Intros. Generalize a a'. Elim n. Exact ad_xor_sem_5.
   Exact ad_xor_sem_6.
@@ -303,7 +306,8 @@ Proof.
   Unfold eqf. Intros. Unfold adf_xor. Rewrite H. Rewrite H0. Reflexivity.
 Qed.
 
-Lemma ad_xor_assoc : (a,a',a'':ad) (ad_xor (ad_xor a a') a'')=(ad_xor a (ad_xor a' a'')).
+Lemma ad_xor_assoc 
+  : (a,a',a'':ad) (ad_xor (ad_xor a a') a'')=(ad_xor a (ad_xor a' a'')).
 Proof.
   Intros. Apply ad_faithful.
   Apply eqf_trans with f':=(adf_xor (adf_xor (ad_bit a) (ad_bit a')) (ad_bit a'')).
@@ -354,7 +358,8 @@ Proof.
   Intros. Rewrite <- (ad_double_div_2 a0). Rewrite H. Apply ad_double_div_2.
 Qed.
 
-Lemma ad_double_plus_un_inj : (a0,a1:ad) (ad_double_plus_un a0)=(ad_double_plus_un a1) -> a0=a1.
+Lemma ad_double_plus_un_inj 
+  : (a0,a1:ad) (ad_double_plus_un a0)=(ad_double_plus_un a1) -> a0=a1.
 Proof.
   Intros. Rewrite <- (ad_double_plus_un_div_2 a0). Rewrite H. Apply ad_double_plus_un_div_2.
 Qed.
@@ -383,7 +388,8 @@ Proof.
   Intro. Discriminate H.
 Qed.
 
-Lemma ad_div_2_double_plus_un : (a:ad) (ad_bit_0 a)=true -> (ad_double_plus_un (ad_div_2 a))=a.
+Lemma ad_div_2_double_plus_un 
+  : (a:ad) (ad_bit_0 a)=true -> (ad_double_plus_un (ad_div_2 a))=a.
 Proof.
   Induction a. Intro. Discriminate H.
   Induction p. Intros. Reflexivity.
@@ -403,13 +409,15 @@ Proof.
   Induction p; Trivial.
 Qed.
 
-Lemma ad_xor_bit_0 : (a,a':ad) (ad_bit_0 (ad_xor a a'))=(xorb (ad_bit_0 a) (ad_bit_0 a')).
+Lemma ad_xor_bit_0 
+  : (a,a':ad) (ad_bit_0 (ad_xor a a'))=(xorb (ad_bit_0 a) (ad_bit_0 a')).
 Proof.
   Intros. Rewrite <- ad_bit_0_correct. Rewrite (ad_xor_semantics a a' O).
   Unfold adf_xor. Rewrite ad_bit_0_correct. Rewrite ad_bit_0_correct. Reflexivity.
 Qed.
 
-Lemma ad_xor_div_2 : (a,a':ad) (ad_div_2 (ad_xor a a'))=(ad_xor (ad_div_2 a) (ad_div_2 a')).
+Lemma ad_xor_div_2 
+  : (a,a':ad) (ad_div_2 (ad_xor a a'))=(ad_xor (ad_div_2 a) (ad_div_2 a')).
 Proof.
   Intros. Apply ad_faithful. Unfold eqf. Intro.
   Rewrite (ad_xor_semantics (ad_div_2 a) (ad_div_2 a') n).
@@ -426,7 +434,8 @@ Proof.
   Rewrite xorb_assoc. Rewrite xorb_nilpotent. Rewrite xorb_false. Reflexivity.
 Qed.
 
-Lemma ad_neg_bit_0_1 : (a,a':ad) (ad_xor a a')=(ad_x xH) -> (ad_bit_0 a)=(negb (ad_bit_0 a')).
+Lemma ad_neg_bit_0_1 
+  : (a,a':ad) (ad_xor a a')=(ad_x xH) -> (ad_bit_0 a)=(negb (ad_bit_0 a')).
 Proof.
   Intros. Apply ad_neg_bit_0. Rewrite H. Reflexivity.
 Qed.
diff --git a/theories/IntMap/Adist.v b/theories/IntMap/Adist.v
index f5d40e66f8..4e545af7b6 100644
--- a/theories/IntMap/Adist.v
+++ b/theories/IntMap/Adist.v
@@ -59,7 +59,8 @@ Proof.
 Qed.
 
 Lemma ad_plength_first_one : (a:ad) (n:nat)
-    ((k:nat) (lt k n) -> (ad_bit a k)=false) -> (ad_bit a n)=true -> (ad_plength a)=(ni n).
+    ((k:nat) (lt k n) -> (ad_bit a k)=false) -> (ad_bit a n)=true 
+     -> (ad_plength a)=(ni n).
 Proof.
   Induction a. Intros. Simpl in H0. Discriminate H0.
   Induction p. Intros. Generalize H0. Case n. Intros. Reflexivity.
diff --git a/theories/IntMap/Map.v b/theories/IntMap/Map.v
index a9093f08d7..05f5612ab4 100644
--- a/theories/IntMap/Map.v
+++ b/theories/IntMap/Map.v
@@ -78,12 +78,14 @@ Section MapDefs.
     Unfold MapGet. Intros. Rewrite (ad_eq_correct a). Reflexivity.
   Qed.
 
-  Lemma M1_semantics_2 : (a,a':ad) (y:A) (ad_eq a a')=false -> (MapGet (M1 a y) a')=NONE.
+  Lemma M1_semantics_2 
+    : (a,a':ad) (y:A) (ad_eq a a')=false -> (MapGet (M1 a y) a')=NONE.
   Proof.
     Intros. Simpl. Rewrite H. Reflexivity.
   Qed.
 
-  Lemma Map2_semantics_1 : (m,m':Map) (eqm (MapGet m) [a:ad] (MapGet (M2 m m') (ad_double a))).
+  Lemma Map2_semantics_1 
+    : (m,m':Map) (eqm (MapGet m) [a:ad] (MapGet (M2 m m') (ad_double a))).
   Proof.
     Unfold eqm. Induction a; Trivial.
   Qed.
@@ -97,7 +99,8 @@ Section MapDefs.
     Exact (Map2_semantics_1 m m' a).
   Qed.
 
-  Lemma Map2_semantics_2 : (m,m':Map) (eqm (MapGet m') [a:ad] (MapGet (M2 m m') (ad_double_plus_un a))).
+  Lemma Map2_semantics_2 
+    : (m,m':Map) (eqm (MapGet m') [a:ad] (MapGet (M2 m m') (ad_double_plus_un a))).
   Proof.
     Unfold eqm. Induction a; Trivial.
   Qed.
@@ -646,7 +649,8 @@ Section MapDefs.
   Qed.
 
   Lemma MapDelta_semantics_1_1 : (a:ad) (y:A) (m':Map) (a0:ad)
-    (MapGet (M1 a y) a0)=NONE -> (MapGet m' a0)=NONE -> (MapGet (MapDelta (M1 a y) m') a0)=NONE.
+    (MapGet (M1 a y) a0)=NONE -> (MapGet m' a0)=NONE -> 
+      (MapGet (MapDelta (M1 a y) m') a0)=NONE.
   Proof.
     Intros. Unfold MapDelta. Elim (sumbool_of_bool (ad_eq a a0)). Intro H1.
     Rewrite (ad_eq_complete ? ? H1) in H. Rewrite (M1_semantics_1 a0 y) in H. Discriminate H.
@@ -692,7 +696,8 @@ Section MapDefs.
   Qed.
 
   Lemma MapDelta_semantics_2 : (m,m':Map) (a:ad) (y:A)
-    (MapGet m a)=NONE -> (MapGet m' a)=(SOME y) -> (MapGet (MapDelta m m') a)=(SOME y).
+    (MapGet m a)=NONE -> (MapGet m' a)=(SOME y) -> 
+      (MapGet (MapDelta m m') a)=(SOME y).
   Proof.
     Induction m. Trivial.
     Exact MapDelta_semantics_2_1.
@@ -718,7 +723,8 @@ Section MapDefs.
   Qed.
 
   Lemma MapDelta_semantics_3 : (m,m':Map) (a:ad) (y,y':A)
-    (MapGet m a)=(SOME y) -> (MapGet m' a)=(SOME y') -> (MapGet (MapDelta m m') a)=NONE.
+    (MapGet m a)=(SOME y) -> (MapGet m' a)=(SOME y') -> 
+      (MapGet (MapDelta m m') a)=NONE.
   Proof.
     Induction m. Intros. Discriminate H.
     Exact MapDelta_semantics_3_1.
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 4dbab94c15..c9052de6c5 100755
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -6,9 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* i$Id$ i*)
+(*i $Id$ i*)
 
-(*** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED *)
+(*** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***)
 
 Require Le.
 
diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index 675a346e22..ae62962ea8 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -10,7 +10,7 @@
 
 (* A Library for finite sets, implemented as lists *)
 (* A Library with similar interface will soon be available under
-  the name TreeSet in the theories/TREES directory *)
+  the name TreeSet in the theories/Trees directory *)
 
 (* PolyList is loaded, but not exported *)
 (* This allow to "hide" the definitions, functions and theorems of PolyList
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index 9dc01f0a1f..16c88e598d 100755
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -125,11 +125,11 @@ Section Stream_Properties.
 
 Variable P : Stream->Prop.
 
-(*
+(*i
 Inductive   Exists :  Stream -> Prop :=
    Here    : (x:Stream)(P x) ->(Exists x) |
    Further : (x:Stream)~(P x)->(Exists (tl x))->(Exists x).
-*)
+i*)
 
 Inductive   Exists :  Stream -> Prop :=
    Here    : (x:Stream)(P x) ->(Exists x) |
diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v
index 5fbbc93389..a97f549017 100755
--- a/theories/Lists/TheoryList.v
+++ b/theories/Lists/TheoryList.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Some programs and results about lists following CAML Manual *)
 
diff --git a/theories/Lists/intro.tex b/theories/Lists/intro.tex
index 2930326e19..344bba59ab 100755
--- a/theories/Lists/intro.tex
+++ b/theories/Lists/intro.tex
@@ -1,13 +1,13 @@
 \section{Lists}\label{Lists}
 
-The LISTS library includes the following files:
+This library includes the following files:
 
 \begin{itemize}
 
-\item {\tt Lists.v} THIS OLD LIBRARY IS HERE ONLY FOR COMPATIBILITY
+\item {\tt List.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, 
+\item {\tt PolyList.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
diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
index 898783cbc8..4b4ab63514 100644
--- a/theories/Reals/Rbase.v
+++ b/theories/Reals/Rbase.v
@@ -286,13 +286,14 @@ Lemma Rplus_Ropp:(x,y:R)``x+y==0``->``y== -x``.
   | Ring ].
 Save.
 
-(* New *)
+(*i New i*)
 Hint eqT_R_congr : real := Resolve (congr_eqT R).
 
 Lemma Rplus_plus_r:(r,r1,r2:R)(r1==r2)->``r+r1==r+r2``.
   Auto with real.
 Save.
-(* Old *) Hints Resolve Rplus_plus_r : v62.
+
+(*i Old i*)Hints Resolve Rplus_plus_r : v62.
 
 (**********)
 Lemma r_Rplus_plus:(r,r1,r2:R)``r+r1==r+r2``->r1==r2.
@@ -358,7 +359,8 @@ Hints Resolve Rmult_1r : real.
 Lemma Rmult_mult_r:(r,r1,r2:R)r1==r2->``r*r1==r*r2``.
   Auto with real.
 Save.
-(* OLD *) Hints Resolve Rmult_mult_r : v62.
+
+(*i OLD i*)Hints Resolve Rmult_mult_r : v62.
 
 (**********)
 Lemma r_Rmult_mult:(r,r1,r2:R)(``r*r1==r*r2``)->``r<>0``->(r1==r2).
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index 1bd1e5ec7d..b5ac6e1f9c 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -25,7 +25,8 @@ Parameter Ropp:R->R.
 Parameter Rinv:R->R. 
 Parameter Rlt:R->R->Prop.    
 Parameter up:R->Z.
-(*********************************************************)
+
+(*i*******************************************************i*)
 
 (**********)
 Definition Rgt:R->R->Prop:=[r1,r2:R](Rlt r2 r1).
diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v
index 4f4899f402..b8eef3a253 100644
--- a/theories/Reals/Rsyntax.v
+++ b/theories/Reals/Rsyntax.v
@@ -71,9 +71,9 @@ Grammar command command0 :=
 Grammar command atomic_pattern :=
   r_in_pattern [ "``" rnatural:rnumber($c) "``" ] -> [$c].   
 
-(** pp **)
+(*i* pp **)
 (* pb: on rajoute des () lorsque les constantes terminent par 1 lors de
-l'appel avec NRplus *)
+l'appel avec NRplus i*)
 
 
 
diff --git a/theories/Relations/Newman.v b/theories/Relations/Newman.v
index 966a755c50..e7829b00e3 100755
--- a/theories/Relations/Newman.v
+++ b/theories/Relations/Newman.v
@@ -85,14 +85,14 @@ Proof     (* We draw the diagram ! *)
 Theorem caseRxy : (coherence y z).
 Proof (Rstar_Rstar' x z h2 
       ([v:A][w:A](coherence y w))
-      (coherence_sym x y (Rstar_coherence x y h1))  (* case x=z *)
-      Diagram).                                     (* case x->v->*z *)
+      (coherence_sym x y (Rstar_coherence x y h1))  (*i case x=z i*)
+      Diagram).                                     (*i case x->v->*z i*)
 End Newman_.
 
 Theorem Ind_proof : (coherence y z).
 Proof (Rstar_Rstar' x y h1 ([u:A][v:A](coherence v z))
-        (Rstar_coherence x z h2)                    (* case x=y*)
-        caseRxy).                                   (* case x->u->*z *)
+        (Rstar_coherence x z h2)                    (*i case x=y i*)
+        caseRxy).                                   (*i case x->u->*z i*)
 End Induct.
 
 Theorem Newman : (x:A)(confluence x).
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index a5ee001573..a5c81e2e37 100755
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -9,7 +9,7 @@
 (*i $Id$ i*)
 
 (****************************************************************************)
-(*                      Bruno Barras Cristina Cornes                        *)
+(*                      Bruno Barras, Cristina Cornes                       *)
 (*                                                                          *)
 (*  Some of these definitons were taken from :                              *)
 (*     Constructing Recursion Operators in Type Theory                      *)
diff --git a/theories/Relations/Rstar.v b/theories/Relations/Rstar.v
index 0df3af6b40..a0aaed9add 100755
--- a/theories/Relations/Rstar.v
+++ b/theories/Relations/Rstar.v
@@ -10,8 +10,8 @@
 
 (* Properties of a binary relation R on type A *)
 
-  Parameter A : Type.  
-  Parameter R : A->A->Prop.  
+Parameter A : Type.  
+Parameter R : A->A->Prop.  
 
 (* Definition of the reflexive-transitive closure R* of R *)
 (* Smallest reflexive P containing R o P *)
diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v
index 0ddad85787..40389087ef 100755
--- a/theories/Sets/Ensembles.v
+++ b/theories/Sets/Ensembles.v
@@ -43,10 +43,10 @@ Inductive Full_set : Ensemble :=
      Full_intro: (x: U) (In Full_set x).
 
 (* NB The following definition builds-in equality of elements in U as 
-   Leibniz equality.
+   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)]. *)
+   equality eqs, with  
+     [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 9e79ee3a0c..31d4c94302 100755
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -170,12 +170,12 @@ Apply multiset_twist2.
 Qed.
 
 
-(* theory of minter to do similarly 
+(*i theory of minter to do similarly 
 Require Min.
 (* multiset intersection *)
 Definition minter := [m1,m2:multiset]
     (Bag [a:A](min (multiplicity m1 a)(multiplicity m2 a))).
-*)
+i*)
 
 End multiset_defs.
 
diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v
index 699c5f3628..3e1837078a 100755
--- a/theories/Sets/Powerset_facts.v
+++ b/theories/Sets/Powerset_facts.v
@@ -274,4 +274,3 @@ Hints Resolve Empty_set_zero Empty_set_zero' Union_associative Union_add
 	singlx incl_add : sets v62.
 
 
-(* $Id$ *)
diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v
index c7e8e7d05f..90c055775b 100755
--- a/theories/Sets/Relations_3.v
+++ b/theories/Sets/Relations_3.v
@@ -61,6 +61,3 @@ Hints Resolve definition_of_noetherian : sets v62.
 Hints Unfold  Noetherian : sets v62.
 
 
-
-
-(* $Id$ *)
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
index 12f267873b..ced2a75f95 100644
--- a/theories/Sets/Uniset.v
+++ b/theories/Sets/Uniset.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Sets  as characteristic functions *)
 
@@ -199,12 +199,12 @@ Apply uniset_twist2.
 Qed.
 
 
-(* theory of minter to do similarly 
+(*i theory of minter to do similarly 
 Require Min.
 (* uniset intersection *)
 Definition minter := [m1,m2:uniset]
     (Charac [a:A](andb (charac m1 a)(charac m2 a))).
-*)
+i*)
 
 End defs.
 
diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v
index ffe56c0dab..bc87acd980 100644
--- a/theories/Wellfounded/Inverse_Image.v
+++ b/theories/Wellfounded/Inverse_Image.v
@@ -38,15 +38,3 @@ Section Inverse_Image.
 End Inverse_Image.
 
 
-
-
-
-
-
-
-
-
-
-
-
-(* $Id$ *)
diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v
index d9cf77c750..27c7601949 100644
--- a/theories/ZArith/Wf_Z.v
+++ b/theories/ZArith/Wf_Z.v
@@ -20,8 +20,8 @@ Require Zsyntax.
  (n:nat)(Q n)==(n:nat)(P (inject_nat n)) ===> (x:Z)`x > 0) -> (P x)
 
        	     /\
-	     ||
-	     ||
+             ||
+             ||
 
   (Q O) (n:nat)(Q n)->(Q (S n)) <=== (P 0) (x:Z) (P x) -> (P (Zs x))
 
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index 663fe535c1..dc9e69e17e 100644
--- a/theories/ZArith/Zmisc.v
+++ b/theories/ZArith/Zmisc.v
@@ -21,20 +21,24 @@ Require auxiliary.
 Require Zsyntax.
 Require Bool.
 
-(**********************************************************************
+(************************************************************************)
+(*
  Overview of the sections of this file :
-
- - logic : Logic complements.
- - numbers : a few very simple lemmas for manipulating the
+ \begin{itemize}
+ \item logic : Logic complements.
+ \item numbers : a few very simple lemmas for manipulating the
    constructors [POS], [NEG], [ZERO] and [xI], [xO], [xH]
- - registers : defining arrays of bits and their relation with integers.
- - iter : the n-th iterate of a function is defined for n:nat and n:positive.
+ \item registers : defining arrays of bits and their relation with integers.
+ \item iter : the n-th iterate of a function is defined for n:nat and 
+   n:positive.
+   
    The two notions are identified and an invariant conservation theorem
    is proved.
- - recursors : Here a nat-like recursor is built.
- - arith : lemmas about [< <= ?= + *] ...
-
-************************************************************************)
+ \item recursors : Here a nat-like recursor is built.
+ \item arith : lemmas about [< <= ?= + *] ...
+ \end{itemize}
+*)
+(************************************************************************)
 
 Section logic.
 
@@ -83,7 +87,7 @@ End numbers.
 
 Section iterate.
 
-(* l'itere n-ieme d'une fonction f*)
+(* [n]th iteration of the function [f] *)
 Fixpoint iter_nat[n:nat]  : (A:Set)(f:A->A)A->A :=
   [A:Set][f:A->A][x:A]
     Cases n of
diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v
index 4e92f7cd7b..1981080a2b 100644
--- a/theories/ZArith/Zsyntax.v
+++ b/theories/ZArith/Zsyntax.v
@@ -78,14 +78,15 @@ Grammar constr pattern :=
   to avoid printings like |``x` + `y`` < `45`| 
   for |x + y < 45|.
   So when a Z-expression is to be printed, its sub-expresssions are
-  enclosed into an ast (ZEXPR $subexpr). (ZEXPR $s) is printed like $s
-  but without symbols "`" "`" around. *)
+  enclosed into an ast (ZEXPR \$subexpr). (ZEXPR \$s) is printed like \$s
+  but without symbols "`" "`" around. 
 
-(* There is just one problem: NEG and Zopp have the same printing rules.
+   There is just one problem: NEG and Zopp have the same printing rules.
    If Zopp is opaque, we may not be able to solve a goal like
     ` -5 = -5 ` by reflexivity. (In fact, this precise Goal is solved
-  by the Reflexivity tactic, but more complex problems may arise *)
-(* SOLUTION : Print (Zopp 5) for constants and -x for variables *)
+  by the Reflexivity tactic, but more complex problems may arise 
+
+  SOLUTION : Print (Zopp 5) for constants and -x for variables *)
 
 Syntax constr
   level 0:
diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v
index 7a4ebae686..5e554edab2 100644
--- a/theories/ZArith/auxiliary.v
+++ b/theories/ZArith/auxiliary.v
@@ -558,7 +558,8 @@ Theorem OMEGA2 : (x,y:Z) (Zle ZERO x) -> (Zle ZERO y) -> (Zle ZERO (Zplus x y)).
 Intros x y H1 H2;Rewrite <- (Zero_left ZERO); Apply Zle_plus_plus; Assumption.
 Save. 
 
-Theorem OMEGA3 : (x,y,k:Z)(Zgt k ZERO)-> (x=(Zmult y k)) -> (x=ZERO) -> (y=ZERO).
+Theorem OMEGA3 : 
+  (x,y,k:Z)(Zgt k ZERO)-> (x=(Zmult y k)) -> (x=ZERO) -> (y=ZERO).
 
 Intros x y k H1 H2 H3; Apply (Zmult_eq k); [
   Unfold not ; Intros H4; Absurd (Zgt k ZERO); [
@@ -605,7 +606,8 @@ Intros x y z t H1 H2 H3 H4; Rewrite <- (Zero_left ZERO);
 Apply Zle_plus_plus; Apply Zle_mult; Assumption.
 Save.
 
-Theorem OMEGA8: (x,y:Z) (Zle ZERO x) -> (Zle ZERO y) -> x = (Zopp y) -> x = ZERO.
+Theorem OMEGA8: 
+  (x,y:Z) (Zle ZERO x) -> (Zle ZERO y) -> x = (Zopp y) -> x = ZERO.
 
 Intros x y H1 H2 H3; Elim (Zle_lt_or_eq ZERO x H1); [
   Intros H4; Absurd (Zlt ZERO x); [
@@ -694,7 +696,7 @@ Rewrite H2; Auto with arith.
 Save.
 
 Theorem OMEGA18:
-(x,y,k:Z) (x=(Zmult y k)) -> (Zne x ZERO) -> (Zne y ZERO).
+  (x,y,k:Z) (x=(Zmult y k)) -> (Zne x ZERO) -> (Zne y ZERO).
 
 Unfold Zne not; Intros x y k H1 H2 H3; Apply H2; Rewrite H1; Rewrite H3; Auto with arith.
 Save.
diff --git a/theories/ZArith/zarith_aux.v b/theories/ZArith/zarith_aux.v
index 856082b926..72b66c4945 100644
--- a/theories/ZArith/zarith_aux.v
+++ b/theories/ZArith/zarith_aux.v
@@ -733,7 +733,7 @@ Save.
 
 
 (* 
-  Just for compatibility with previous versions 
+  Just for compatibility with previous versions. 
   Use [Zmult_plus_distr_r] and [Zmult_plus_distr_l] rather than
   their synomymous 
 *)