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 67121590e..1b70e1512 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 2f100ebc5..ff502af94 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 bcbe0f714..f9c5e3976 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 e91b3fb1a..9c6cd1f42 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 abbe45081..72ad3d986 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 debaed16c..026b0ef16 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 f5d40e66f..4e545af7b 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 a9093f08d..05f5612ab 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 4dbab94c1..c9052de6c 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 675a346e2..ae62962ea 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 9dc01f0a1..16c88e598 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 5fbbc9338..a97f54901 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 2930326e1..344bba59a 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 898783cbc..4b4ab6351 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 1bd1e5ec7..b5ac6e1f9 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 4f4899f40..b8eef3a25 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 966a755c5..e7829b00e 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 a5ee00157..a5c81e2e3 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 0df3af6b4..a0aaed9ad 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 0ddad8578..40389087e 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 9e79ee3a0..31d4c9430 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 699c5f362..3e1837078 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 c7e8e7d05..90c055775 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 12f267873..ced2a75f9 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 ffe56c0da..bc87acd98 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 d9cf77c75..27c760194 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 663fe535c..dc9e69e17 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 4e92f7cd7..1981080a2 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 7a4ebae68..5e554edab 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 856082b92..72b66c494 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 
 *)