Library doc adjustments (until page 140)

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

5 files changed, 29 insertions, 22 deletions

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 
 *)