Library doc adjustments (until page 140)

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

4 files changed, 39 insertions, 20 deletions

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.