Minor layout adjustments for Library doc

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

19 files changed, 262 insertions, 186 deletions

diff --git a/theories/IntMap/Adalloc.v b/theories/IntMap/Adalloc.v
index 63c2f2ad4b..ab7f19a07f 100644
--- a/theories/IntMap/Adalloc.v
+++ b/theories/IntMap/Adalloc.v
@@ -93,28 +93,32 @@ Section AdAlloc.
     Rewrite (le_antisym ? ? (nat_le_complete ? ? H) (nat_le_complete ? ? H0)). Reflexivity.
   Qed.
 
-  Lemma ad_le_trans : (a,b,c:ad) (ad_le a b)=true -> (ad_le b c)=true -> (ad_le a c)=true.
+  Lemma ad_le_trans : (a,b,c:ad) (ad_le a b)=true -> (ad_le b c)=true -> 
+      (ad_le a c)=true.
   Proof.
     Unfold ad_le. Intros. Apply nat_le_correct. Apply le_trans with m:=(nat_of_ad b).
     Apply nat_le_complete. Assumption.
     Apply nat_le_complete. Assumption.
   Qed.
 
-  Lemma ad_le_lt_trans : (a,b,c:ad) (ad_le a b)=true -> (ad_le c b)=false -> (ad_le c a)=false.
+  Lemma ad_le_lt_trans : (a,b,c:ad) (ad_le a b)=true -> (ad_le c b)=false -> 
+      (ad_le c a)=false.
   Proof.
     Unfold ad_le. Intros. Apply nat_le_correct_conv. Apply le_lt_trans with m:=(nat_of_ad b).
     Apply nat_le_complete. Assumption.
     Apply nat_le_complete_conv. Assumption.
   Qed.
 
-  Lemma ad_lt_le_trans : (a,b,c:ad) (ad_le b a)=false -> (ad_le b c)=true -> (ad_le c a)=false.
+  Lemma ad_lt_le_trans : (a,b,c:ad) (ad_le b a)=false -> (ad_le b c)=true -> 
+      (ad_le c a)=false.
   Proof.
     Unfold ad_le. Intros. Apply nat_le_correct_conv. Apply lt_le_trans with m:=(nat_of_ad b).
     Apply nat_le_complete_conv. Assumption.
     Apply nat_le_complete. Assumption.
   Qed.
 
-  Lemma ad_lt_trans : (a,b,c:ad) (ad_le b a)=false -> (ad_le c b)=false -> (ad_le c a)=false.
+  Lemma ad_lt_trans : (a,b,c:ad) (ad_le b a)=false -> (ad_le c b)=false -> 
+      (ad_le c a)=false.
   Proof.
     Unfold ad_le. Intros. Apply nat_le_correct_conv. Apply lt_trans with m:=(nat_of_ad b).
     Apply nat_le_complete_conv. Assumption.
@@ -277,7 +281,8 @@ Section AdAlloc.
     Exact convert_xI.
   Qed.
 
-  Lemma ad_le_double_mono : (a,b:ad) (ad_le a b)=true -> (ad_le (ad_double a) (ad_double b))=true.
+  Lemma ad_le_double_mono : (a,b:ad) (ad_le a b)=true -> 
+      (ad_le (ad_double a) (ad_double b))=true.
   Proof.
     Unfold ad_le. Intros. Rewrite nat_of_ad_double. Rewrite nat_of_ad_double. Apply nat_le_correct.
     Simpl. Apply le_plus_plus. Apply nat_le_complete. Assumption.
diff --git a/theories/IntMap/Addec.v b/theories/IntMap/Addec.v
index 72ad3d9866..64c5337288 100644
--- a/theories/IntMap/Addec.v
+++ b/theories/IntMap/Addec.v
@@ -73,8 +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.
@@ -116,22 +116,23 @@ 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.
 Qed.
 
-Lemma ad_div_neq : (a,a':ad) (ad_eq (ad_div_2 a) (ad_div_2 a'))=false -> (ad_eq a a')=false.
+Lemma ad_div_neq : (a,a':ad) (ad_eq (ad_div_2 a) (ad_div_2 a'))=false -> 
+    (ad_eq a a')=false.
 Proof.
   Intros. Elim (sumbool_of_bool (ad_eq a a')). Intro H0.
   Rewrite (ad_eq_complete ? ? H0) in H. Rewrite (ad_eq_correct (ad_div_2 a')) in H. Discriminate H.
diff --git a/theories/IntMap/Addr.v b/theories/IntMap/Addr.v
index 026b0ef16d..088b03845d 100644
--- a/theories/IntMap/Addr.v
+++ b/theories/IntMap/Addr.v
@@ -141,9 +141,9 @@ Qed.
 
 Lemma ad_faithful_3 :
     (a:ad) (p:positive)
-      ((p':positive) (eqf (ad_bit (ad_x p)) (ad_bit (ad_x p'))) -> p=p')
-      -> (eqf (ad_bit (ad_x (xO p))) (ad_bit a))
-        -> (ad_x (xO p))=a.
+      ((p':positive) (eqf (ad_bit (ad_x p)) (ad_bit (ad_x p'))) -> p=p') ->
+        (eqf (ad_bit (ad_x (xO p))) (ad_bit a)) ->
+          (ad_x (xO p))=a.
 Proof.
   Induction a. Intros. Cut (eqf (ad_bit ad_z) (ad_bit (ad_x (xO p)))).
   Intro. Rewrite (ad_faithful_1 (ad_x (xO p)) H1). Reflexivity.
@@ -157,9 +157,9 @@ Qed.
 
 Lemma ad_faithful_4 :
     (a:ad) (p:positive)
-      ((p':positive) (eqf (ad_bit (ad_x p)) (ad_bit (ad_x p'))) -> p=p')
-      -> (eqf (ad_bit (ad_x (xI p))) (ad_bit a))
-        -> (ad_x (xI p))=a.
+      ((p':positive) (eqf (ad_bit (ad_x p)) (ad_bit (ad_x p'))) -> p=p') ->
+        (eqf (ad_bit (ad_x (xI p))) (ad_bit a)) ->
+          (ad_x (xI p))=a.
 Proof.
   Induction a. Intros. Cut (eqf (ad_bit ad_z) (ad_bit (ad_x (xI p)))).
   Intro. Rewrite (ad_faithful_1 (ad_x (xI p)) H1). Reflexivity.
@@ -200,8 +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. 
@@ -220,8 +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.
@@ -230,8 +230,8 @@ Proof.
 Qed.
 
 Lemma ad_xor_sem_6 : (n:nat)
-    ((a,a':ad) (ad_bit (ad_xor a a') n)=(adf_xor (ad_bit a) (ad_bit a') n))
-    -> (a,a':ad) (ad_bit (ad_xor a a') (S n))=(adf_xor (ad_bit a) (ad_bit a') (S n)).
+    ((a,a':ad) (ad_bit (ad_xor a a') n)=(adf_xor (ad_bit a) (ad_bit a') n)) ->
+      (a,a':ad) (ad_bit (ad_xor a a') (S n))=(adf_xor (ad_bit a) (ad_bit a') (S n)).
 Proof.
   Intros. Case a. Unfold adf_xor. Unfold 2 ad_bit. Rewrite false_xorb. Reflexivity.
   Case a'. Unfold adf_xor. Unfold 3 ad_bit. Intro. Rewrite xorb_false. Reflexivity.
@@ -260,8 +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.
@@ -306,8 +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'')).
@@ -358,8 +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.
@@ -388,8 +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.
@@ -409,15 +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).
@@ -434,8 +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 4e545af7b6..0361b12c80 100644
--- a/theories/IntMap/Adist.v
+++ b/theories/IntMap/Adist.v
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the      *)
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
-(*i 	$Id$	 i*)
+(*i 	     $Id$	      i*)
 
 Require Bool.
 Require ZArith.
@@ -59,8 +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.
@@ -185,9 +185,9 @@ Proof.
   Unfold ni_le. Intros. Rewrite (ni_min_comm d' d). Apply ni_min_case.
 Qed.
 
-Lemma ni_le_min_induc : (d,d',dm:natinf) (ni_le dm d) -> (ni_le dm d')
-    -> ((d'':natinf) (ni_le d'' d) -> (ni_le d'' d') -> (ni_le d'' dm))
-      -> (ni_min d d')=dm.
+Lemma ni_le_min_induc : (d,d',dm:natinf) (ni_le dm d) -> (ni_le dm d') ->
+    ((d'':natinf) (ni_le d'' d) -> (ni_le d'' d') -> (ni_le d'' dm)) ->
+      (ni_min d d')=dm.
 Proof.
   Intros. Case (ni_min_case d d'). Intro. Rewrite H2.
   Apply ni_le_antisym. Apply H1. Apply ni_le_refl.
@@ -212,8 +212,8 @@ Proof.
   Unfold ni_le. Unfold ni_min. Intros. Inversion H. Apply le_min_r.
 Qed.
 
-Lemma ad_plength_lb : (a:ad) (n:nat) ((k:nat) (lt k n) -> (ad_bit a k)=false)
-    -> (ni_le (ni n) (ad_plength a)).
+Lemma ad_plength_lb : (a:ad) (n:nat) ((k:nat) (lt k n) -> (ad_bit a k)=false) ->
+    (ni_le (ni n) (ad_plength a)).
 Proof.
   Induction a. Intros. Exact (ni_min_inf_r (ni n)).
   Intros. Unfold ad_plength. Apply le_ni_le. Case (le_or_lt n (ad_plength_1 p)). Trivial.
@@ -224,8 +224,8 @@ Proof.
   Apply H. Exact H0.
 Qed.
 
-Lemma ad_plength_ub : (a:ad) (n:nat) (ad_bit a n)=true
-    -> (ni_le (ad_plength a) (ni n)).
+Lemma ad_plength_ub : (a:ad) (n:nat) (ad_bit a n)=true ->
+    (ni_le (ad_plength a) (ni n)).
 Proof.
   Induction a. Intros. Discriminate H.
   Intros. Unfold ad_plength. Apply le_ni_le. Case (le_or_lt (ad_plength_1 p) n). Trivial.
@@ -276,8 +276,8 @@ Qed.
 *)
 
 Lemma ad_plength_ultra_1 : (a,a':ad)
-    (ni_le (ad_plength a) (ad_plength a'))
-      -> (ni_le (ad_plength a) (ad_plength (ad_xor a a'))).
+    (ni_le (ad_plength a) (ad_plength a')) ->
+      (ni_le (ad_plength a) (ad_plength (ad_xor a a'))).
 Proof.
   Induction a. Intros. Unfold ni_le in H. Unfold 1 3 ad_plength in H.
   Rewrite (ni_min_inf_l (ad_plength a')) in H.
diff --git a/theories/IntMap/Fset.v b/theories/IntMap/Fset.v
index 130e89edc4..26bb5e8f35 100644
--- a/theories/IntMap/Fset.v
+++ b/theories/IntMap/Fset.v
@@ -197,7 +197,7 @@ Section Dom.
   Qed.
 
   Lemma in_dom_delta : (m,m':(Map A)) (a:ad)
-    (in_dom a (MapDelta A m m'))=(xorb (in_dom a m) (in_dom a m')).
+      (in_dom a (MapDelta A m m'))=(xorb (in_dom a m) (in_dom a m')).
   Proof.
     Unfold in_dom. Intros. Rewrite (MapDelta_semantics A m m' a).
     Elim (option_sum A (MapGet A m' a)). Intro H. Elim H. Intros y H0. Rewrite H0.
diff --git a/theories/IntMap/Lsort.v b/theories/IntMap/Lsort.v
index 7f8e61e600..80ab704de3 100644
--- a/theories/IntMap/Lsort.v
+++ b/theories/IntMap/Lsort.v
@@ -33,7 +33,8 @@ Section LSort.
 				    | (ad_x p) => (ad_less_1 a a' p)
 				  end.
 
-  Lemma ad_bit_0_less : (a,a':ad) (ad_bit_0 a)=false -> (ad_bit_0 a')=true -> (ad_less a a')=true.
+  Lemma ad_bit_0_less : (a,a':ad) (ad_bit_0 a)=false -> (ad_bit_0 a')=true -> 
+      (ad_less a a')=true.
   Proof.
     Intros. Elim (ad_sum (ad_xor a a')). Intro H1. Elim H1. Intros p H2. Unfold ad_less.
     Rewrite H2. Generalize H2. Elim p. Intros. Simpl. Rewrite H. Rewrite H0. Reflexivity.
@@ -46,7 +47,8 @@ Section LSort.
     Rewrite H1. Reflexivity.
   Qed.
 
-  Lemma ad_bit_0_gt : (a,a':ad) (ad_bit_0 a)=true -> (ad_bit_0 a')=false -> (ad_less a a')=false.
+  Lemma ad_bit_0_gt : (a,a':ad) (ad_bit_0 a)=true -> (ad_bit_0 a')=false -> 
+      (ad_less a a')=false.
   Proof.
     Intros. Elim (ad_sum (ad_xor a a')). Intro H1. Elim H1. Intros p H2. Unfold ad_less.
     Rewrite H2. Generalize H2. Elim p. Intros. Simpl. Rewrite H. Rewrite H0. Reflexivity.
diff --git a/theories/IntMap/Map.v b/theories/IntMap/Map.v
index 05f5612ab4..245ceb558e 100644
--- a/theories/IntMap/Map.v
+++ b/theories/IntMap/Map.v
@@ -58,6 +58,7 @@ Section MapDefs.
     end.
 
   Definition newMap := M0.
+
   Definition MapSingleton := M1.
 
   Definition eqm := [g,g':ad->option] (a:ad) (g a)=(g' a).
@@ -78,14 +79,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.
@@ -99,8 +100,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.
@@ -205,7 +206,8 @@ Section MapDefs.
   Qed.
   i*)
 
-  Lemma MapGet_if_same : (m:Map) (b:bool) (a:ad) (MapGet (if b then m else m) a)=(MapGet m a).
+  Lemma MapGet_if_same : (m:Map) (b:bool) (a:ad) 
+      (MapGet (if b then m else m) a)=(MapGet m a).
   Proof.
     Induction b;Trivial.
   Qed.
@@ -240,7 +242,8 @@ Section MapDefs.
   Qed.
 
   Lemma MapGet_M2_both_NONE : (m,m':Map) (a:ad)
-      (MapGet m (ad_div_2 a))=NONE -> (MapGet m' (ad_div_2 a))=NONE -> (MapGet (M2 m m') a)=NONE.
+      (MapGet m (ad_div_2 a))=NONE -> (MapGet m' (ad_div_2 a))=NONE -> 
+        (MapGet (M2 m m') a)=NONE.
   Proof.
     Intros. Rewrite (Map2_semantics_3 m m' a). 
     Case (ad_bit_0 a); Assumption.
@@ -575,7 +578,8 @@ Section MapDefs.
       | (M2 m1 m2) => [m':Map] Cases m' of
       	                           M0 => m
 				 | (M1 a' y') => (MapPut m a' y')
-				 | (M2 m'1 m'2) => (M2 (MapMerge m1 m'1) (MapMerge m2 m'2))
+				 | (M2 m'1 m'2) => (M2 (MapMerge m1 m'1) 
+	                                               (MapMerge m2 m'2))
 			       end
     end.
 
@@ -659,7 +663,8 @@ Section MapDefs.
   Qed.
 
   Lemma MapDelta_semantics_1 : (m,m':Map) (a:ad)
-    (MapGet m a)=NONE -> (MapGet m' a)=NONE -> (MapGet (MapDelta m m') a)=NONE.
+    (MapGet m a)=NONE -> (MapGet m' a)=NONE -> 
+      (MapGet (MapDelta m m') a)=NONE.
   Proof.
     Induction m. Trivial.
     Exact MapDelta_semantics_1_1.
diff --git a/theories/IntMap/Mapaxioms.v b/theories/IntMap/Mapaxioms.v
index 957f25e1f0..7ab131c77b 100644
--- a/theories/IntMap/Mapaxioms.v
+++ b/theories/IntMap/Mapaxioms.v
@@ -137,7 +137,8 @@ Section MapAxioms.
   Qed.
 
   Lemma MapMerge_ext : (m1,m2,m'1,m'2:(Map A))
-      (eqmap m1 m'1) -> (eqmap m2 m'2) -> (eqmap (MapMerge A m1 m2) (MapMerge A m'1 m'2)).
+      (eqmap m1 m'1) -> (eqmap m2 m'2) -> 
+        (eqmap (MapMerge A m1 m2) (MapMerge A m'1 m'2)).
   Proof.
     Unfold eqmap eqm. Intros. Rewrite (MapMerge_semantics A m1 m2 a).
     Rewrite (MapMerge_semantics A m'1 m'2 a). Rewrite (H a). Rewrite (H0 a). Reflexivity.
@@ -186,22 +187,26 @@ Section MapAxioms.
     Case (ad_eq a a0); [ Reflexivity | Apply H ].
   Qed.
 
-  Lemma MapDomRestrTo_empty_m_1 : (m:(Map B)) (MapDomRestrTo A B (M0 A) m)=(M0 A).
+  Lemma MapDomRestrTo_empty_m_1 : 
+      (m:(Map B)) (MapDomRestrTo A B (M0 A) m)=(M0 A).
   Proof.
     Trivial.
   Qed.
 
-  Lemma MapDomRestrTo_empty_m : (m:(Map B)) (eqmap (MapDomRestrTo A B (M0 A) m) (M0 A)).
+  Lemma MapDomRestrTo_empty_m : 
+      (m:(Map B)) (eqmap (MapDomRestrTo A B (M0 A) m) (M0 A)).
   Proof.
     Unfold eqmap eqm. Trivial.
   Qed.
 
-  Lemma MapDomRestrTo_m_empty_1 : (m:(Map A)) (MapDomRestrTo A B m (M0 B))=(M0 A).
+  Lemma MapDomRestrTo_m_empty_1 : 
+      (m:(Map A)) (MapDomRestrTo A B m (M0 B))=(M0 A).
   Proof.
     Induction m;Trivial.
   Qed.
 
-  Lemma MapDomRestrTo_m_empty : (m:(Map A)) (eqmap (MapDomRestrTo A B m (M0 B)) (M0 A)).
+  Lemma MapDomRestrTo_m_empty : 
+      (m:(Map A)) (eqmap (MapDomRestrTo A B m (M0 B)) (M0 A)).
   Proof.
     Unfold eqmap eqm. Intros. Rewrite (MapDomRestrTo_m_empty_1 m). Reflexivity.
   Qed.
@@ -237,12 +242,14 @@ Section MapAxioms.
     Intros H0 H1. Discriminate H1.
   Qed.
 
-  Lemma MapDomRestrBy_empty_m_1 : (m:(Map B)) (MapDomRestrBy A B (M0 A) m)=(M0 A).
+  Lemma MapDomRestrBy_empty_m_1 : 
+      (m:(Map B)) (MapDomRestrBy A B (M0 A) m)=(M0 A).
   Proof.
     Trivial.
   Qed.
 
-  Lemma MapDomRestrBy_empty_m : (m:(Map B)) (eqmap (MapDomRestrBy A B (M0 A) m) (M0 A)).
+  Lemma MapDomRestrBy_empty_m : 
+      (m:(Map B)) (eqmap (MapDomRestrBy A B (M0 A) m) (M0 A)).
   Proof.
     Unfold eqmap eqm. Trivial.
   Qed.
@@ -450,7 +457,8 @@ Section MapAxioms.
   Qed.
 
   Lemma MapDelta_ext : (m1,m2,m'1,m'2:(Map A))
-      (eqmap m1 m'1) -> (eqmap m2 m'2) -> (eqmap (MapDelta A m1 m2) (MapDelta A m'1 m'2)).
+      (eqmap m1 m'1) -> (eqmap m2 m'2) -> 
+        (eqmap (MapDelta A m1 m2) (MapDelta A m'1 m'2)).
   Proof.
     Unfold eqmap eqm. Intros. Rewrite (MapDelta_semantics A m1 m2 a).
     Rewrite (MapDelta_semantics A m'1 m'2 a). Rewrite (H a). Rewrite (H0 a). Reflexivity.
@@ -491,7 +499,8 @@ Section MapAxioms.
   Qed.
 
   Lemma MapDom_Split_3 : (m:(Map A)) (m':(Map B))
-      (eqmap (MapDomRestrTo A A (MapDomRestrTo A B m m') (MapDomRestrBy A B m m')) (M0 A)).
+      (eqmap (MapDomRestrTo A A (MapDomRestrTo A B m m') (MapDomRestrBy A B m m')) 
+	(M0 A)).
   Proof.
     Unfold eqmap eqm. Intros.
     Rewrite (MapDomRestrTo_semantics A A (MapDomRestrTo A B m m') (MapDomRestrBy A B m m') a).
@@ -502,9 +511,10 @@ Section MapAxioms.
 
 End MapAxioms.
 
-Lemma MapDomRestrTo_ext : (A,B:Set) (m1:(Map A)) (m2:(Map B)) (m'1:(Map A)) (m'2:(Map B))
-    (eqmap A m1 m'1) -> (eqmap B m2 m'2) ->
-      (eqmap A (MapDomRestrTo A B m1 m2) (MapDomRestrTo A B m'1 m'2)).
+Lemma MapDomRestrTo_ext : (A,B:Set) 
+    (m1:(Map A)) (m2:(Map B)) (m'1:(Map A)) (m'2:(Map B))
+      (eqmap A m1 m'1) -> (eqmap B m2 m'2) ->
+        (eqmap A (MapDomRestrTo A B m1 m2) (MapDomRestrTo A B m'1 m'2)).
 Proof.
   Unfold eqmap eqm. Intros. Rewrite (MapDomRestrTo_semantics A B m1 m2 a).
   Rewrite (MapDomRestrTo_semantics A B m'1 m'2 a). Rewrite (H a). Rewrite (H0 a). Reflexivity.
@@ -524,9 +534,10 @@ Proof.
   Intros. Apply MapDomRestrTo_ext; [ Apply eqmap_refl | Assumption ].
 Qed.
 
-Lemma MapDomRestrBy_ext : (A,B:Set) (m1:(Map A)) (m2:(Map B)) (m'1:(Map A)) (m'2:(Map B))
-    (eqmap A m1 m'1) -> (eqmap B m2 m'2) ->
-      (eqmap A (MapDomRestrBy A B m1 m2) (MapDomRestrBy A B m'1 m'2)).
+Lemma MapDomRestrBy_ext : (A,B:Set) 
+    (m1:(Map A)) (m2:(Map B)) (m'1:(Map A)) (m'2:(Map B))
+      (eqmap A m1 m'1) -> (eqmap B m2 m'2) ->
+        (eqmap A (MapDomRestrBy A B m1 m2) (MapDomRestrBy A B m'1 m'2)).
 Proof.
   Unfold eqmap eqm. Intros. Rewrite (MapDomRestrBy_semantics A B m1 m2 a).
   Rewrite (MapDomRestrBy_semantics A B m'1 m'2 a). Rewrite (H a). Rewrite (H0 a). Reflexivity.
diff --git a/theories/IntMap/Mapc.v b/theories/IntMap/Mapc.v
index d78c05d6b9..b7cede9440 100644
--- a/theories/IntMap/Mapc.v
+++ b/theories/IntMap/Mapc.v
@@ -68,9 +68,10 @@ Section MapC.
     Apply MapMerge_idempotent.
   Qed.
 
-  Lemma MapMerge_RestrTo_l_c : (m,m',m'':(Map A)) (mapcanon A m) -> (mapcanon A m'') ->
-      (MapMerge A (MapDomRestrTo A A m m') m'')
-      =(MapDomRestrTo A A (MapMerge A m m'') (MapMerge A m' m'')).
+  Lemma MapMerge_RestrTo_l_c : (m,m',m'':(Map A)) 
+      (mapcanon A m) -> (mapcanon A m'') -> 
+        (MapMerge A (MapDomRestrTo A A m m') m'')=
+        (MapDomRestrTo A A (MapMerge A m m'') (MapMerge A m' m'')).
   Proof.
     Intros. Apply mapcanon_unique. Apply MapMerge_canon. Apply MapDomRestrTo_canon; Assumption.
     Assumption.
@@ -97,7 +98,8 @@ Section MapC.
     Apply MapDomRestrTo_assoc.
   Qed.
 
-  Lemma MapDomRestrTo_idempotent_c : (m:(Map A)) (mapcanon A m) -> (MapDomRestrTo A A m m)=m.
+  Lemma MapDomRestrTo_idempotent_c : (m:(Map A)) (mapcanon A m) -> 
+      (MapDomRestrTo A A m m)=m.
   Proof.
     Intros. Apply mapcanon_unique. (Apply MapDomRestrTo_canon; Assumption).
     Assumption.
@@ -120,9 +122,10 @@ Section MapC.
     Apply MapDomRestrBy_Dom.
   Qed.
 
-  Lemma MapDomRestrBy_By_c : (m:(Map A)) (m':(Map B)) (m'':(Map B)) (mapcanon A m) ->
-      (MapDomRestrBy A B (MapDomRestrBy A B m m') m'')=
-      (MapDomRestrBy A B m (MapMerge B m' m'')).
+  Lemma MapDomRestrBy_By_c : (m:(Map A)) (m':(Map B)) (m'':(Map B)) 
+      (mapcanon A m) -> 
+        (MapDomRestrBy A B (MapDomRestrBy A B m m') m'')=
+        (MapDomRestrBy A B m (MapMerge B m' m'')).
   Proof.
     Intros. Apply mapcanon_unique. (Apply MapDomRestrBy_canon; Try Assumption).
     (Apply MapDomRestrBy_canon; Try Assumption).
@@ -130,9 +133,10 @@ Section MapC.
     Apply MapDomRestrBy_By.
   Qed.
 
-  Lemma MapDomRestrBy_By_comm_c : (m:(Map A)) (m':(Map B)) (m'':(Map C)) (mapcanon A m) ->
-      (MapDomRestrBy A C (MapDomRestrBy A B m m') m'')=
-      (MapDomRestrBy A B (MapDomRestrBy A C m m'') m').
+  Lemma MapDomRestrBy_By_comm_c : (m:(Map A)) (m':(Map B)) (m'':(Map C)) 
+      (mapcanon A m) ->
+        (MapDomRestrBy A C (MapDomRestrBy A B m m') m'')=
+        (MapDomRestrBy A B (MapDomRestrBy A C m m'') m').
   Proof.
     Intros. Apply mapcanon_unique. Apply MapDomRestrBy_canon.
     (Apply MapDomRestrBy_canon; Assumption).
@@ -140,9 +144,10 @@ Section MapC.
     Apply MapDomRestrBy_By_comm.
   Qed.
 
-  Lemma MapDomRestrBy_To_c : (m:(Map A)) (m':(Map B)) (m'':(Map C)) (mapcanon A m) ->
-      (MapDomRestrBy A C (MapDomRestrTo A B m m') m'')=
-      (MapDomRestrTo A B m (MapDomRestrBy B C m' m'')).
+  Lemma MapDomRestrBy_To_c : (m:(Map A)) (m':(Map B)) (m'':(Map C)) 
+      (mapcanon A m) ->
+        (MapDomRestrBy A C (MapDomRestrTo A B m m') m'')=
+        (MapDomRestrTo A B m (MapDomRestrBy B C m' m'')).
   Proof.
     Intros. Apply mapcanon_unique. Apply MapDomRestrBy_canon.
     (Apply MapDomRestrTo_canon; Assumption).
@@ -150,9 +155,10 @@ Section MapC.
     Apply MapDomRestrBy_To.
   Qed.
 
-  Lemma MapDomRestrBy_To_comm_c : (m:(Map A)) (m':(Map B)) (m'':(Map C)) (mapcanon A m) ->
-      (MapDomRestrBy A C (MapDomRestrTo A B m m') m'')=
-      (MapDomRestrTo A B (MapDomRestrBy A C m m'') m').
+  Lemma MapDomRestrBy_To_comm_c : (m:(Map A)) (m':(Map B)) (m'':(Map C)) 
+      (mapcanon A m) ->
+        (MapDomRestrBy A C (MapDomRestrTo A B m m') m'')=
+        (MapDomRestrTo A B (MapDomRestrBy A C m m'') m').
   Proof.
     Intros. Apply mapcanon_unique. Apply MapDomRestrBy_canon.
     Apply MapDomRestrTo_canon; Assumption.
@@ -160,9 +166,10 @@ Section MapC.
     Apply MapDomRestrBy_To_comm.
   Qed.
 
-  Lemma MapDomRestrTo_By_c : (m:(Map A)) (m':(Map B)) (m'':(Map C)) (mapcanon A m) ->
-      (MapDomRestrTo A C (MapDomRestrBy A B m m') m'')=
-      (MapDomRestrTo A C m (MapDomRestrBy C B m'' m')).
+  Lemma MapDomRestrTo_By_c : (m:(Map A)) (m':(Map B)) (m'':(Map C)) 
+      (mapcanon A m) ->
+        (MapDomRestrTo A C (MapDomRestrBy A B m m') m'')=
+        (MapDomRestrTo A C m (MapDomRestrBy C B m'' m')).
   Proof.
     Intros. Apply mapcanon_unique. Apply MapDomRestrTo_canon.
     Apply MapDomRestrBy_canon; Assumption.
@@ -170,9 +177,10 @@ Section MapC.
     Apply MapDomRestrTo_By.
   Qed.
 
-  Lemma MapDomRestrTo_By_comm_c : (m:(Map A)) (m':(Map B)) (m'':(Map C)) (mapcanon A m) ->
-      (MapDomRestrTo A C (MapDomRestrBy A B m m') m'')=
-      (MapDomRestrBy A B (MapDomRestrTo A C m m'') m').
+  Lemma MapDomRestrTo_By_comm_c : (m:(Map A)) (m':(Map B)) (m'':(Map C)) 
+      (mapcanon A m) ->
+        (MapDomRestrTo A C (MapDomRestrBy A B m m') m'')=
+        (MapDomRestrBy A B (MapDomRestrTo A C m m'') m').
   Proof.
     Intros. Apply mapcanon_unique. Apply MapDomRestrTo_canon.
     (Apply MapDomRestrBy_canon; Assumption).
@@ -180,9 +188,10 @@ Section MapC.
     Apply MapDomRestrTo_By_comm.
   Qed.
 
-  Lemma MapDomRestrTo_To_comm_c : (m:(Map A)) (m':(Map B)) (m'':(Map C)) (mapcanon A m) ->
-      (MapDomRestrTo A C (MapDomRestrTo A B m m') m'')=
-      (MapDomRestrTo A B (MapDomRestrTo A C m m'') m').
+  Lemma MapDomRestrTo_To_comm_c : (m:(Map A)) (m':(Map B)) (m'':(Map C)) 
+      (mapcanon A m) ->
+        (MapDomRestrTo A C (MapDomRestrTo A B m m') m'')=
+        (MapDomRestrTo A B (MapDomRestrTo A C m m'') m').
   Proof.
     Intros. Apply mapcanon_unique. Apply MapDomRestrTo_canon.
     Apply MapDomRestrTo_canon; Assumption.
@@ -213,7 +222,8 @@ Section MapC.
     Apply MapMerge_DomRestrBy.
   Qed.
 
-  Lemma MapDelta_nilpotent_c : (m:(Map A)) (mapcanon A m) -> (MapDelta A m m)=(M0 A).
+  Lemma MapDelta_nilpotent_c : (m:(Map A)) (mapcanon A m) -> 
+      (MapDelta A m m)=(M0 A).
   Proof.
     Intros. Apply mapcanon_unique. (Apply MapDelta_canon; Assumption).
     Apply M0_canon.
@@ -222,7 +232,8 @@ Section MapC.
 
   Lemma MapDelta_as_Merge_c : (m,m':(Map A))
       (mapcanon A m) -> (mapcanon A m') ->
-        (MapDelta A m m')=(MapMerge A (MapDomRestrBy A A m m') (MapDomRestrBy A A m' m)).
+        (MapDelta A m m')=
+	(MapMerge A (MapDomRestrBy A A m m') (MapDomRestrBy A A m' m)).
   Proof.
     Intros. Apply mapcanon_unique. (Apply MapDelta_canon; Assumption).
     (Apply MapMerge_canon; Apply MapDomRestrBy_canon; Assumption).
@@ -231,7 +242,8 @@ Section MapC.
 
   Lemma MapDelta_as_DomRestrBy_c : (m,m':(Map A))
       (mapcanon A m) -> (mapcanon A m') ->
-        (MapDelta A m m')=(MapDomRestrBy A A (MapMerge A m m') (MapDomRestrTo A A m m')).
+        (MapDelta A m m')=
+	(MapDomRestrBy A A (MapMerge A m m') (MapDomRestrTo A A m m')).
   Proof.
     Intros. Apply mapcanon_unique. Apply MapDelta_canon; Assumption.
     Apply MapDomRestrBy_canon. (Apply MapMerge_canon; Assumption).
@@ -240,7 +252,8 @@ Section MapC.
 
   Lemma MapDelta_as_DomRestrBy_2_c : (m,m':(Map A))
       (mapcanon A m) -> (mapcanon A m') ->
-        (MapDelta A m m')=(MapDomRestrBy A A (MapMerge A m m') (MapDomRestrTo A A m' m)).
+        (MapDelta A m m')=
+	(MapDomRestrBy A A (MapMerge A m m') (MapDomRestrTo A A m' m)).
   Proof.
     Intros. Apply mapcanon_unique. (Apply MapDelta_canon; Assumption).
     Apply MapDomRestrBy_canon. Apply MapMerge_canon; Assumption.
@@ -273,7 +286,8 @@ Section MapC.
   Qed.
 
   Lemma MapDom_Split_3_c : (m:(Map A)) (m':(Map B)) (mapcanon A m) ->
-      (MapDomRestrTo A A (MapDomRestrTo A B m m') (MapDomRestrBy A B m m'))=(M0 A).
+      (MapDomRestrTo A A (MapDomRestrTo A B m m') (MapDomRestrBy A B m m'))=
+      (M0 A).
   Proof.
     Intros. Apply mapcanon_unique. Apply MapDomRestrTo_canon.
     Apply MapDomRestrTo_canon; Assumption.
diff --git a/theories/IntMap/Mapcanon.v b/theories/IntMap/Mapcanon.v
index b1616ebeb8..b98e9b233a 100644
--- a/theories/IntMap/Mapcanon.v
+++ b/theories/IntMap/Mapcanon.v
@@ -33,7 +33,8 @@ Section MapCanon.
     | M2_canon : (m1,m2:(Map A)) (mapcanon m1) -> (mapcanon m2) ->
         (le (2) (MapCard A (M2 A m1 m2))) -> (mapcanon (M2 A m1 m2)).
 
-  Lemma mapcanon_M2 : (m1,m2:(Map A)) (mapcanon (M2 A m1 m2)) -> (le (2) (MapCard A (M2 A m1 m2))).
+  Lemma mapcanon_M2 : 
+      (m1,m2:(Map A)) (mapcanon (M2 A m1 m2)) -> (le (2) (MapCard A (M2 A m1 m2))).
   Proof.
     Intros. Inversion H. Assumption.
   Qed.
@@ -48,7 +49,8 @@ Section MapCanon.
     Intros. Inversion H. Assumption.
   Qed.
 
-  Lemma M2_eqmap_1 : (m0,m1,m2,m3:(Map A)) (eqmap A (M2 A m0 m1) (M2 A m2 m3)) -> (eqmap A m0 m2).
+  Lemma M2_eqmap_1 : (m0,m1,m2,m3:(Map A)) 
+      (eqmap A (M2 A m0 m1) (M2 A m2 m3)) -> (eqmap A m0 m2).
   Proof.
     Unfold eqmap eqm. Intros. Rewrite <- (ad_double_div_2 a).
     Rewrite <- (MapGet_M2_bit_0_0 A ? (ad_double_bit_0 a) m0 m1).
@@ -56,7 +58,8 @@ Section MapCanon.
     Exact (H (ad_double a)).
   Qed.
 
-  Lemma M2_eqmap_2 : (m0,m1,m2,m3:(Map A)) (eqmap A (M2 A m0 m1) (M2 A m2 m3)) -> (eqmap A m1 m3).
+  Lemma M2_eqmap_2 : (m0,m1,m2,m3:(Map A)) 
+      (eqmap A (M2 A m0 m1) (M2 A m2 m3)) -> (eqmap A m1 m3).
   Proof.
     Unfold eqmap eqm. Intros. Rewrite <- (ad_double_plus_un_div_2 a).
     Rewrite <- (MapGet_M2_bit_0_1 A ? (ad_double_plus_un_bit_0 a) m0 m1).
@@ -97,7 +100,8 @@ Section MapCanon.
     Exact (M2_eqmap_1 ? ? ? ? H5).
   Qed.
 
-  Lemma MapPut1_canon : (p:positive) (a,a':ad) (y,y':A) (mapcanon (MapPut1 A a y a' y' p)).
+  Lemma MapPut1_canon : 
+      (p:positive) (a,a':ad) (y,y':A) (mapcanon (MapPut1 A a y a' y' p)).
   Proof.
     Induction p. Simpl. Intros. Case (ad_bit_0 a). Apply M2_canon. Apply M1_canon.
     Apply M1_canon.
@@ -119,7 +123,8 @@ Section MapCanon.
     Simpl. Apply le_n.
   Qed.
 
-  Lemma MapPut_canon : (m:(Map A)) (mapcanon m) -> (a:ad) (y:A) (mapcanon (MapPut A m a y)).
+  Lemma MapPut_canon : 
+      (m:(Map A)) (mapcanon m) -> (a:ad) (y:A) (mapcanon (MapPut A m a y)).
   Proof.
     Induction m. Intros. Simpl. Apply M1_canon.
     Intros a0 y0 H a y. Simpl. Case (ad_xor a0 a). Apply M1_canon.
@@ -174,7 +179,8 @@ Section MapCanon.
     Apply le_reg_l. Rewrite MapCard_Put_behind_Put. Exact (MapCard_Put_lb A m1 ad_z y).
   Qed.
 
-  Lemma makeM2_canon : (m,m':(Map A)) (mapcanon m) -> (mapcanon m') -> (mapcanon (makeM2 A m m')).
+  Lemma makeM2_canon : 
+      (m,m':(Map A)) (mapcanon m) -> (mapcanon m') -> (mapcanon (makeM2 A m m')).
   Proof.
     Intro. Case m. Intro. Case m'. Intros. Exact M0_canon.
     Intros a y H H0. Exact (M1_canon (ad_double_plus_un a) y).
@@ -212,13 +218,15 @@ Section MapCanon.
     Intros. Simpl. (Apply makeM2_canon; Assumption).
   Qed.
 
-  Lemma mapcanon_exists : (m:(Map A)) {m':(Map A) | (eqmap A m m') /\ (mapcanon m')}.
+  Lemma mapcanon_exists : 
+      (m:(Map A)) {m':(Map A) | (eqmap A m m') /\ (mapcanon m')}.
   Proof.
     Intro. Split with (MapCanonicalize m). Split. Apply mapcanon_exists_1.
     Apply mapcanon_exists_2.
   Qed.
 
-  Lemma MapRemove_canon : (m:(Map A)) (mapcanon m) -> (a:ad) (mapcanon (MapRemove A m a)).
+  Lemma MapRemove_canon : 
+      (m:(Map A)) (mapcanon m) -> (a:ad) (mapcanon (MapRemove A m a)).
   Proof.
     Induction m. Intros. Exact M0_canon.
     Intros a y H a0. Simpl. Case (ad_eq a a0). Exact M0_canon.
@@ -356,7 +364,8 @@ Section MapFoldCanon.
     Intros. Exact (MapFold_canon_1 m0 H op H0 f H1 m [a:ad]a).
   Qed.
 
-  Lemma MapCollect_canon : (f : ad->A->(Map B)) ((a:ad) (y:A) (mapcanon B (f a y))) ->
+  Lemma MapCollect_canon : 
+      (f : ad->A->(Map B)) ((a:ad) (y:A) (mapcanon B (f a y))) ->
 	(m:(Map A)) (mapcanon B (MapCollect A B f m)).
   Proof.
     Intros. Rewrite MapCollect_as_Fold. Apply MapFold_canon. Apply M0_canon.
diff --git a/theories/IntMap/Mapcard.v b/theories/IntMap/Mapcard.v
index 51c92c2bc5..cb7e7f933a 100644
--- a/theories/IntMap/Mapcard.v
+++ b/theories/IntMap/Mapcard.v
@@ -37,7 +37,8 @@ Section MapCard.
     Trivial.
   Qed.
 
-  Lemma MapCard_is_O : (m:(Map A)) (MapCard A m)=O -> (a:ad) (MapGet A m a)=(NONE A).
+  Lemma MapCard_is_O : (m:(Map A)) (MapCard A m)=O -> 
+      (a:ad) (MapGet A m a)=(NONE A).
   Proof.
     Induction m. Trivial.
     Intros a y H. Discriminate H.
@@ -75,9 +76,9 @@ Section MapCard.
     Rewrite ad_double_div_2. Exact H5.
   Qed.
 
-  Lemma MapCard_is_one_unique : (m:(Map A)) (MapCard A m)=(1) ->
-    (a,a':ad) (y,y':A) (MapGet A m a)=(SOME A y) -> (MapGet A m a')=(SOME A y') ->
-      a=a' /\ y=y'.
+  Lemma MapCard_is_one_unique : (m:(Map A)) (MapCard A m)=(1) -> (a,a':ad) (y,y':A) 
+      (MapGet A m a)=(SOME A y) -> (MapGet A m a')=(SOME A y') ->
+        a=a' /\ y=y'.
   Proof.
     Induction m. Intro. Discriminate H.
     Intros. Elim (sumbool_of_bool (ad_eq a a1)). Intro H2. Rewrite (ad_eq_complete ? ? H2) in H0.
@@ -110,14 +111,15 @@ Section MapCard.
     Assumption.
   Qed.
 
-  Lemma length_as_fold : (C:Set) (l:(list C)) (length l)=(fold_right [_:C][n:nat](S n) O l).
+  Lemma length_as_fold : (C:Set) (l:(list C)) 
+      (length l)=(fold_right [_:C][n:nat](S n) O l).
   Proof.
     Induction l. Reflexivity.
     Intros. Simpl. Rewrite H. Reflexivity.
   Qed.
 
-  Lemma length_as_fold_2 : (l:(alist A)) (length l)=
-      (fold_right [r:ad*A][n:nat]let (a,y)=r in (plus (1) n) O l).
+  Lemma length_as_fold_2 : (l:(alist A)) 
+      (length l)=(fold_right [r:ad*A][n:nat]let (a,y)=r in (plus (1) n) O l).
   Proof.
     Induction l. Reflexivity.
     Intros. Simpl. Rewrite H. (Elim a; Reflexivity).
@@ -132,7 +134,8 @@ Section MapCard.
     Rewrite <- (H0 [a0:ad](pf (ad_double_plus_un a0))). Reflexivity.
   Qed.
 
-  Lemma MapCard_as_Fold : (m:(Map A)) (MapCard A m)=(MapFold A nat O plus [_:ad][_:A](1) m).
+  Lemma MapCard_as_Fold : 
+      (m:(Map A)) (MapCard A m)=(MapFold A nat O plus [_:ad][_:A](1) m).
   Proof.
     Intro. Exact (MapCard_as_Fold_1 m [a0:ad]a0).
   Qed.
@@ -209,7 +212,8 @@ Section MapCard.
   Qed.
 
   Lemma MapCard_Put_1 : (m:(Map A)) (a:ad) (y:A)
-      (MapCard A (MapPut A m a y))=(MapCard A m) -> {y:A | (MapGet A m a)=(SOME A y)}.
+      (MapCard A (MapPut A m a y))=(MapCard A m) -> 
+        {y:A | (MapGet A m a)=(SOME A y)}.
   Proof.
     Induction m. Intros. Discriminate H.
     Intros a y a0 y0 H. Simpl in H. Elim (ad_sum (ad_xor a a0)). Intro H0. Elim H0.
@@ -394,7 +398,8 @@ Section MapCard.
   Qed.
 
   Lemma MapCard_Remove_2 : (m:(Map A)) (a:ad)
-      (S (MapCard A (MapRemove A m a)))=(MapCard A m) -> {y:A | (MapGet A m a)=(SOME A y)}.
+      (S (MapCard A (MapRemove A m a)))=(MapCard A m) -> 
+        {y:A | (MapGet A m a)=(SOME A y)}.
   Proof.
     Induction m. Intros. Discriminate H.
     Intros a y a0 H. Simpl in H. Elim (sumbool_of_bool (ad_eq a a0)). Intro H0.
@@ -428,7 +433,8 @@ Section MapCard.
   Qed.
 
   Lemma MapCard_Remove_2_conv : (m:(Map A)) (a:ad) (y:A)
-      (MapGet A m a)=(SOME A y) -> (S (MapCard A (MapRemove A m a)))=(MapCard A m).
+      (MapGet A m a)=(SOME A y) -> 
+        (S (MapCard A (MapRemove A m a)))=(MapCard A m).
   Proof.
     Intros.
     Elim (MapCard_Remove_sum m (MapRemove A m a) a (MapCard A m)
@@ -543,7 +549,8 @@ Section MapCard.
     Unfold in_dom. Rewrite H7. Reflexivity.
   Qed.
 
-  Lemma MapCard_is_Sn : (m:(Map A)) (n:nat) (MapCard ? m)=(S n) -> {a:ad | (in_dom ? a m)=true}.
+  Lemma MapCard_is_Sn : (m:(Map A)) (n:nat) (MapCard ? m)=(S n) -> 
+      {a:ad | (in_dom ? a m)=true}.
   Proof.
     Induction m. Intros. Discriminate H.
     Intros a y n H. Split with a. Unfold in_dom. Rewrite (M1_semantics_1 ? a y). Reflexivity.
diff --git a/theories/IntMap/Mapfold.v b/theories/IntMap/Mapfold.v
index 46b0fb2c72..1e59e42b22 100644
--- a/theories/IntMap/Mapfold.v
+++ b/theories/IntMap/Mapfold.v
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the      *)
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
-(*i 	$Id$	 i*)
+(*i   	  $Id$      i*)
 
 Require Bool.
 Require Sumbool.
@@ -97,7 +97,8 @@ Section MapFoldResults.
   Variable comm : (a,b:M) (op a b)=(op b a).
 
   Lemma MapFold_Put_disjoint_1 : (p:positive)
-        (f:ad->A->M) (pf:ad->ad) (a1,a2:ad) (y1,y2:A) (ad_xor a1 a2)=(ad_x p) ->
+        (f:ad->A->M) (pf:ad->ad) (a1,a2:ad) (y1,y2:A) 
+	  (ad_xor a1 a2)=(ad_x p) ->
       	    (MapFold1 A M neutral op f pf (MapPut1 A a1 y1 a2 y2 p))=
 	    (op (f (pf a1) y1) (f (pf a2) y2)).
   Proof.
@@ -175,7 +176,8 @@ Section MapFoldResults.
   Lemma MapFold_Put_disjoint : 
         (f:ad->A->M) (m:(Map A)) (a:ad) (y:A)
 	  (MapGet A m a)=(NONE A) ->
-      	    (MapFold A M neutral op f (MapPut A m a y))=(op (f a y) (MapFold A M neutral op f m)).
+      	    (MapFold A M neutral op f (MapPut A m a y))=
+	    (op (f a y) (MapFold A M neutral op f m)).
   Proof.
     Intros. Exact (MapFold_Put_disjoint_2 f m a y [a0:ad]a0 H).
   Qed.
@@ -368,7 +370,8 @@ Section DMergeDef.
   Qed.
 
   Lemma in_dom_DMerge_3 : (m:(Map (Map A))) (a,b:ad) (m0:(Map A))
-      (MapGet ? m a)=(SOME ? m0) -> (in_dom A b m0)=true -> (in_dom A b (DMerge m))=true.
+      (MapGet ? m a)=(SOME ? m0) -> (in_dom A b m0)=true -> 
+        (in_dom A b (DMerge m))=true.
   Proof.
     Intros m a b m0 H H0. Rewrite in_dom_DMerge_1.
     Elim (MapSweep_semantics_4 ? [_:ad][m'0:(Map A)](in_dom A b m'0) ? ? ? H H0).
diff --git a/theories/IntMap/Mapiter.v b/theories/IntMap/Mapiter.v
index 39ea1d9d8a..216a07c630 100644
--- a/theories/IntMap/Mapiter.v
+++ b/theories/IntMap/Mapiter.v
@@ -137,7 +137,8 @@ Section MapIter.
   Qed.
 
   Lemma MapSweep_semantics_3 : (m:(Map A))
-      (MapSweep m)=(NONE ?) -> (a:ad) (y:A) (MapGet A m a)=(SOME ? y) -> (f a y)=false.
+      (MapSweep m)=(NONE ?) -> (a:ad) (y:A) (MapGet A m a)=(SOME ? y) -> 
+        (f a y)=false.
   Proof.
     Intros.
     Exact (MapSweep_semantics_3_1 m [a0:ad]a0 H a y H0).
@@ -332,7 +333,8 @@ Section MapIter.
 
   Definition ad_inj := [pf:ad->ad] (a0,a1:ad) (pf a0)=(pf a1) -> a0=a1.
 
-  Lemma ad_comp_double_inj : (pf:ad->ad) (ad_inj pf) -> (ad_inj [a0:ad] (pf (ad_double a0))).
+  Lemma ad_comp_double_inj : 
+      (pf:ad->ad) (ad_inj pf) -> (ad_inj [a0:ad] (pf (ad_double a0))).
   Proof.
     Unfold ad_inj. Intros. Apply ad_double_inj. Exact (H ? ? H0).
   Qed.
diff --git a/theories/IntMap/Maplists.v b/theories/IntMap/Maplists.v
index c36c021511..6e5e40814b 100644
--- a/theories/IntMap/Maplists.v
+++ b/theories/IntMap/Maplists.v
@@ -38,7 +38,7 @@ Section MapLists.
     end.
 
   Lemma ad_in_list_forms_circuit : (x:ad) (l:(list ad)) (ad_in_list x l)=true ->
-      	 {l1 : (list ad) & {l2 : (list ad) | l=(app l1 (cons x l2))}}.
+      {l1 : (list ad) & {l2 : (list ad) | l=(app l1 (cons x l2))}}.
   Proof.
     Induction l. Intro. Discriminate H.
     Intros. Elim (sumbool_of_bool (ad_eq x a)). Intro H1. Simpl in H0. Split with (nil ad).
@@ -48,8 +48,8 @@ Section MapLists.
   Qed.
 
   Lemma ad_list_stutters_has_circuit : (l:(list ad)) (ad_list_stutters l)=true ->
-      	  {x:ad & {l0 : (list ad) & {l1 : (list ad) & {l2 : (list ad) |
-	    l=(app l0 (cons x (app l1 (cons x l2))))}}}}.
+      {x:ad & {l0 : (list ad) & {l1 : (list ad) & {l2 : (list ad) |
+        l=(app l0 (cons x (app l1 (cons x l2))))}}}}.
   Proof.
     Induction l. Intro. Discriminate H.
     Intros. Simpl in H0. Elim (orb_true_elim ? ? H0). Intro H1. Split with a.
@@ -162,8 +162,8 @@ Section MapLists.
     Intro H1. Rewrite (H l' a0 H1). Apply orb_b_true.
   Qed.
 
-  Lemma ad_list_stutters_app_l : (l,l':(list ad)) (ad_list_stutters l)=true
-      	  -> (ad_list_stutters (app l l'))=true.
+  Lemma ad_list_stutters_app_l : (l,l':(list ad)) (ad_list_stutters l)=true ->
+      (ad_list_stutters (app l l'))=true.
   Proof.
     Induction l. Intros. Discriminate H.
     Intros. Simpl. Simpl in H0. Elim (orb_true_elim ? ? H0). Intro H1.
@@ -178,23 +178,23 @@ Section MapLists.
     Intros. Simpl. Rewrite (H l' a0 H0). Apply orb_b_true. 
   Qed.
 
-  Lemma ad_list_stutters_app_r : (l,l':(list ad)) (ad_list_stutters l')=true
-      	  -> (ad_list_stutters (app l l'))=true.
+  Lemma ad_list_stutters_app_r : (l,l':(list ad)) (ad_list_stutters l')=true ->
+      (ad_list_stutters (app l l'))=true.
   Proof.
     Induction l. Trivial.
     Intros. Simpl. Rewrite (H l' H0). Apply orb_b_true.
   Qed.
 
-  Lemma ad_list_stutters_app_conv_l : (l,l':(list ad)) (ad_list_stutters (app l l'))=false
-      	  -> (ad_list_stutters l)=false.
+  Lemma ad_list_stutters_app_conv_l : (l,l':(list ad)) (ad_list_stutters (app l l'))=false ->
+      (ad_list_stutters l)=false.
   Proof.
     Intros. Elim (sumbool_of_bool (ad_list_stutters l)). Intro H0.
     Rewrite (ad_list_stutters_app_l l l' H0) in H. Discriminate H.
     Trivial.
   Qed.
 
-  Lemma ad_list_stutters_app_conv_r : (l,l':(list ad)) (ad_list_stutters (app l l'))=false
-      	  -> (ad_list_stutters l')=false.
+  Lemma ad_list_stutters_app_conv_r : (l,l':(list ad)) (ad_list_stutters (app l l'))=false ->
+      (ad_list_stutters l')=false.
   Proof.
     Intros. Elim (sumbool_of_bool (ad_list_stutters l')). Intro H0.
     Rewrite (ad_list_stutters_app_r l l' H0) in H. Discriminate H.
@@ -208,14 +208,14 @@ Section MapLists.
   Qed.
 
   Lemma ad_in_list_app : (l,l':(list ad)) (x:ad)
-          (ad_in_list x (app l l'))=(orb (ad_in_list x l) (ad_in_list x l')).
+      (ad_in_list x (app l l'))=(orb (ad_in_list x l) (ad_in_list x l')).
   Proof.
     Induction l. Trivial.
     Intros. Simpl. Rewrite <- orb_assoc. Rewrite (H l' x). Reflexivity.
   Qed.
 
   Lemma ad_in_list_rev : (l:(list ad)) (x:ad)
-      	(ad_in_list x (rev l))=(ad_in_list x l).
+      (ad_in_list x (rev l))=(ad_in_list x l).
   Proof.
     Induction l. Trivial.
     Intros. Simpl. Rewrite ad_in_list_app. Rewrite (H x). Simpl. Rewrite orb_b_false.
@@ -230,14 +230,14 @@ Section MapLists.
   Qed.
 
   Lemma ad_list_stutters_prev_l : (l,l':(list ad)) (x:ad) (ad_in_list x l)=true ->
-          (ad_list_stutters (app l (cons x l')))=true.
+      (ad_list_stutters (app l (cons x l')))=true.
   Proof.
     Intros. Elim (ad_in_list_forms_circuit ? ? H). Intros l0 H0. Elim H0. Intros l1 H1.
     Rewrite H1. Rewrite app_ass. Simpl. Apply ad_list_has_circuit_stutters.
   Qed.
 
   Lemma ad_list_stutters_prev_conv_l : (l,l':(list ad)) (x:ad)
-      	  (ad_list_stutters (app l (cons x l')))=false -> (ad_in_list x l)=false.
+      (ad_list_stutters (app l (cons x l')))=false -> (ad_in_list x l)=false.
   Proof.
     Intros. Elim (sumbool_of_bool (ad_in_list x l)). Intro H0.
     Rewrite (ad_list_stutters_prev_l l l' x H0) in H. Discriminate H.
@@ -245,14 +245,14 @@ Section MapLists.
   Qed.
 
   Lemma ad_list_stutters_prev_r : (l,l':(list ad)) (x:ad) (ad_in_list x l')=true ->
-          (ad_list_stutters (app l (cons x l')))=true.
+      (ad_list_stutters (app l (cons x l')))=true.
   Proof.
     Intros. Elim (ad_in_list_forms_circuit ? ? H). Intros l0 H0. Elim H0. Intros l1 H1.
     Rewrite H1. Apply ad_list_has_circuit_stutters.
   Qed.
 
   Lemma ad_list_stutters_prev_conv_r : (l,l':(list ad)) (x:ad)
-      	  (ad_list_stutters (app l (cons x l')))=false -> (ad_in_list x l')=false.
+      (ad_list_stutters (app l (cons x l')))=false -> (ad_in_list x l')=false.
   Proof.
     Intros. Elim (sumbool_of_bool (ad_in_list x l')). Intro H0.
     Rewrite (ad_list_stutters_prev_r l l' x H0) in H. Discriminate H.
@@ -298,7 +298,7 @@ Section MapLists.
   Qed.
 
   Lemma ad_list_app_rev : (l,l':(list ad)) (x:ad)
-      	 (app (rev l) (cons x l'))=(app (rev (cons x l)) l').
+      (app (rev l) (cons x l'))=(app (rev (cons x l)) l').
   Proof.
     Induction l. Trivial.
     Intros. Simpl. Rewrite (app_ass (rev l0) (cons a (nil ad)) (cons x l')). Simpl.
@@ -334,7 +334,8 @@ Section MapLists.
     Exact (sym_eq ? ? ?).
   Qed.
 
-  Lemma Elems_of_list_of_dom : (m:(Map A)) (eqmap unit (Elems (ad_list_of_dom m)) (MapDom A m)).
+  Lemma Elems_of_list_of_dom : 
+      (m:(Map A)) (eqmap unit (Elems (ad_list_of_dom m)) (MapDom A m)).
   Proof.
     Unfold eqmap eqm. Intros. Elim (sumbool_of_bool (in_FSet a (Elems (ad_list_of_dom m)))).
     Intro H. Elim (in_dom_some ? ? ? H). Intro t. Elim t. Intro H0.
@@ -356,8 +357,8 @@ Section MapLists.
   Qed.
 
   Lemma ad_list_of_dom_card_1 : (m:(Map A)) (pf:ad->ad)
-      (length (MapFold1 A (list ad) (nil ad) (app 1!ad) [a:ad][_:A](cons a (nil ad)) pf m))
-      =(MapCard A m).
+      (length (MapFold1 A (list ad) (nil ad) (app 1!ad) [a:ad][_:A](cons a (nil ad)) pf m))=
+      (MapCard A m).
   Proof.
     Induction m; Try Trivial. Simpl. Intros. Rewrite ad_list_app_length.
     Rewrite (H [a0:ad](pf (ad_double a0))). Rewrite (H0 [a0:ad](pf (ad_double_plus_un a0))).
@@ -369,7 +370,8 @@ Section MapLists.
     Exact [m:(Map A)](ad_list_of_dom_card_1 m [a:ad]a).
   Qed.
 
-  Lemma ad_list_of_dom_not_stutters : (m:(Map A)) (ad_list_stutters (ad_list_of_dom m))=false.
+  Lemma ad_list_of_dom_not_stutters : 
+      (m:(Map A)) (ad_list_stutters (ad_list_of_dom m))=false.
   Proof.
     Intro. Apply ad_list_not_stutters_card_conv. Rewrite ad_list_of_dom_card. Apply sym_eq.
     Rewrite (MapCard_Dom A m). Apply MapCard_ext. Exact (Elems_of_list_of_dom m).
@@ -379,10 +381,10 @@ Section MapLists.
 
   Lemma ad_list_of_dom_Dom_1 : (A:Set)
     (m:(Map A)) (pf:ad->ad)
-     (MapFold1 A (list ad) (nil ad) (app 1!ad)
-       [a:ad][_:A](cons a (nil ad)) pf m)
-      =(MapFold1 unit (list ad) (nil ad) (app 1!ad)
-         [a:ad][_:unit](cons a (nil ad)) pf (MapDom A m)).
+      (MapFold1 A (list ad) (nil ad) (app 1!ad) 
+        [a:ad][_:A](cons a (nil ad)) pf m)=
+      (MapFold1 unit (list ad) (nil ad) (app 1!ad)
+        [a:ad][_:unit](cons a (nil ad)) pf (MapDom A m)).
   Proof.
     Induction m; Try Trivial. Simpl. Intros. Rewrite (H [a0:ad](pf (ad_double a0))).
     Rewrite (H0 [a0:ad](pf (ad_double_plus_un a0))). Reflexivity.
diff --git a/theories/IntMap/Mapsubset.v b/theories/IntMap/Mapsubset.v
index 5cbfe7ef76..defe49712c 100644
--- a/theories/IntMap/Mapsubset.v
+++ b/theories/IntMap/Mapsubset.v
@@ -32,7 +32,8 @@ Section MapSubsetDef.
 	| _ => false
       end.
 
-  Definition MapSubset_2 := [m:(Map A)] [m':(Map B)] (eqmap A (MapDomRestrBy A B m m') (M0 A)).
+  Definition MapSubset_2 := [m:(Map A)] [m':(Map B)] 
+      (eqmap A (MapDomRestrBy A B m m') (M0 A)).
 
   Lemma MapSubset_imp_1 : (m:(Map A)) (m':(Map B))
       (MapSubset m m') -> (MapSubset_1 m m')=true.
@@ -61,12 +62,14 @@ Section MapSubsetDef.
     Intro H1. Rewrite H1 in H0. Discriminate H0.
   Qed.
 
-  Lemma map_dom_empty_1 : (m:(Map A)) (eqmap A m (M0 A)) -> (a:ad) (in_dom ? a m)=false.
+  Lemma map_dom_empty_1 : 
+      (m:(Map A)) (eqmap A m (M0 A)) -> (a:ad) (in_dom ? a m)=false.
   Proof.
     Unfold eqmap eqm in_dom. Intros. Rewrite (H a). Reflexivity.
   Qed.
 
-  Lemma map_dom_empty_2 : (m:(Map A)) ((a:ad) (in_dom ? a m)=false) -> (eqmap A m (M0 A)).
+  Lemma map_dom_empty_2 : 
+      (m:(Map A)) ((a:ad) (in_dom ? a m)=false) -> (eqmap A m (M0 A)).
   Proof.
     Unfold eqmap eqm in_dom. Intros.
     Cut (Cases (MapGet A m a) of NONE => false | (SOME _) => true end)=false.
@@ -75,14 +78,16 @@ Section MapSubsetDef.
     Exact (H a).
   Qed.
 
-  Lemma MapSubset_imp_2 : (m:(Map A)) (m':(Map B)) (MapSubset m m') -> (MapSubset_2 m m').
+  Lemma MapSubset_imp_2 : 
+      (m:(Map A)) (m':(Map B)) (MapSubset m m') -> (MapSubset_2 m m').
   Proof.
     Unfold MapSubset MapSubset_2. Intros. Apply map_dom_empty_2. Intro. Rewrite in_dom_restrby.
     Elim (sumbool_of_bool (in_dom A a m)). Intro H0. Rewrite H0. Rewrite (H a H0). Reflexivity.
     Intro H0. Rewrite H0. Reflexivity.
   Qed.
 
-  Lemma MapSubset_2_imp : (m:(Map A)) (m':(Map B)) (MapSubset_2 m m') -> (MapSubset m m').
+  Lemma MapSubset_2_imp : 
+      (m:(Map A)) (m':(Map B)) (MapSubset_2 m m') -> (MapSubset m m').
   Proof.
     Unfold MapSubset MapSubset_2. Intros. Cut (in_dom ? a (MapDomRestrBy A B m m'))=false.
     Rewrite in_dom_restrby. Intro. Elim (andb_false_elim ? ? H1). Rewrite H0.
@@ -103,7 +108,8 @@ Section MapSubsetOrder.
   Qed.
 
   Lemma MapSubset_antisym : (m:(Map A)) (m':(Map B))
-      (MapSubset A B m m') -> (MapSubset B A m' m) -> (eqmap unit (MapDom A m) (MapDom B m')).
+      (MapSubset A B m m') -> (MapSubset B A m' m) -> 
+        (eqmap unit (MapDom A m) (MapDom B m')).
   Proof.
     Unfold MapSubset eqmap eqm. Intros. Elim (option_sum ? (MapGet ? (MapDom A m) a)).
     Intro H1. Elim H1. Intro t. Elim t. Intro H2. Elim (option_sum ? (MapGet ? (MapDom B m') a)).
@@ -199,13 +205,15 @@ Section MapSubsetExtra.
     Intro H1. Rewrite (H ? H1). Apply orb_b_true.
   Qed.
 
-  Lemma MapSubset_Put_behind : (m:(Map A)) (a:ad) (y:A) (MapSubset A A m (MapPut_behind A m a y)).
+  Lemma MapSubset_Put_behind : 
+      (m:(Map A)) (a:ad) (y:A) (MapSubset A A m (MapPut_behind A m a y)).
   Proof.
     Unfold MapSubset. Intros. Rewrite in_dom_put_behind. Rewrite H. Apply orb_b_true.
   Qed.
 
   Lemma MapSubset_Put_behind_mono : (m:(Map A)) (m':(Map B)) (a:ad) (y:A) (y':B)
-      (MapSubset A B m m') -> (MapSubset A B (MapPut_behind A m a y) (MapPut_behind B m' a y')).
+      (MapSubset A B m m') -> 
+        (MapSubset A B (MapPut_behind A m a y) (MapPut_behind B m' a y')).
   Proof.
     Unfold MapSubset. Intros. Rewrite in_dom_put_behind.
     Rewrite (in_dom_put_behind A m a y a0) in H0.
@@ -272,9 +280,10 @@ Section MapSubsetExtra.
 
   Variable C, D : Set.
 
-  Lemma MapSubset_DomRestrTo_mono : (m:(Map A)) (m':(Map B)) (m'':(Map C)) (m''':(Map D))
-      (MapSubset ? ? m m'') -> (MapSubset ? ?  m' m''') ->
-      	(MapSubset ? ? (MapDomRestrTo ? ? m m') (MapDomRestrTo ? ? m'' m''')).
+  Lemma MapSubset_DomRestrTo_mono : 
+      (m:(Map A)) (m':(Map B)) (m'':(Map C)) (m''':(Map D))
+        (MapSubset ? ? m m'') -> (MapSubset ? ?  m' m''') ->
+      	  (MapSubset ? ? (MapDomRestrTo ? ? m m') (MapDomRestrTo ? ? m'' m''')).
   Proof.
     Unfold MapSubset. Intros. Rewrite in_dom_restrto. Rewrite (in_dom_restrto A B m m' a) in H1.
     Elim (andb_prop ? ? H1). Intros. Rewrite (H ? H2). Rewrite (H0 ? H3). Reflexivity.
@@ -287,9 +296,10 @@ Section MapSubsetExtra.
     Trivial.
   Qed.
 
-  Lemma MapSubset_DomRestrBy_mono : (m:(Map A)) (m':(Map B)) (m'':(Map C)) (m''':(Map D))
-      (MapSubset ? ? m m'') -> (MapSubset ? ?  m''' m') ->
-      	(MapSubset ? ? (MapDomRestrBy ? ? m m') (MapDomRestrBy ? ? m'' m''')).
+  Lemma MapSubset_DomRestrBy_mono : 
+      (m:(Map A)) (m':(Map B)) (m'':(Map C)) (m''':(Map D))
+        (MapSubset ? ? m m'') -> (MapSubset ? ?  m''' m') ->
+      	  (MapSubset ? ? (MapDomRestrBy ? ? m m') (MapDomRestrBy ? ? m'' m''')).
   Proof.
     Unfold MapSubset. Intros. Rewrite in_dom_restrby. Rewrite (in_dom_restrby A B m m' a) in H1.
     Elim (andb_prop ? ? H1). Intros. Rewrite (H ? H2). Elim (sumbool_of_bool (in_dom D a m''')).
@@ -312,7 +322,8 @@ Section MapDisjointDef.
 	| _ => false
       end.
 
-  Definition MapDisjoint_2 := [m:(Map A)] [m':(Map B)] (eqmap A (MapDomRestrTo A B m m') (M0 A)).
+  Definition MapDisjoint_2 := [m:(Map A)] [m':(Map B)] 
+      (eqmap A (MapDomRestrTo A B m m') (M0 A)).
 
   Lemma MapDisjoint_imp_1 : (m:(Map A)) (m':(Map B))
       (MapDisjoint m m') -> (MapDisjoint_1 m m')=true.
@@ -337,7 +348,8 @@ Section MapDisjointDef.
     Intro H3. Rewrite H3 in H0. Discriminate H0.
   Qed.
 
-  Lemma MapDisjoint_imp_2 : (m:(Map A)) (m':(Map B)) (MapDisjoint m m') -> (MapDisjoint_2 m m').
+  Lemma MapDisjoint_imp_2 : (m:(Map A)) (m':(Map B)) (MapDisjoint m m') -> 
+      (MapDisjoint_2 m m').
   Proof.
     Unfold MapDisjoint MapDisjoint_2. Unfold eqmap eqm. Intros.
     Rewrite (MapDomRestrTo_semantics A B m m' a).
@@ -350,7 +362,8 @@ Section MapDisjointDef.
     Exact (H a).
   Qed.
 
-  Lemma MapDisjoint_2_imp : (m:(Map A)) (m':(Map B)) (MapDisjoint_2 m m') -> (MapDisjoint m m').
+  Lemma MapDisjoint_2_imp : (m:(Map A)) (m':(Map B)) (MapDisjoint_2 m m') -> 
+      (MapDisjoint m m').
   Proof.
     Unfold MapDisjoint MapDisjoint_2. Unfold eqmap eqm. Intros. Elim (in_dom_some ? ? ? H0).
     Intros y H2. Elim (in_dom_some ? ? ? H1). Intros y' H3.
@@ -377,7 +390,8 @@ Section MapDisjointExtra.
   Variable A, B : Set.
 
   Lemma MapDisjoint_ext : (m0,m1:(Map A)) (m2,m3:(Map B))
-      (eqmap A m0 m1) -> (eqmap B m2 m3) -> (MapDisjoint A B m0 m2) -> (MapDisjoint A B m1 m3).
+      (eqmap A m0 m1) -> (eqmap B m2 m3) -> 
+        (MapDisjoint A B m0 m2) -> (MapDisjoint A B m1 m3).
   Proof.
     Intros. Apply MapDisjoint_2_imp. Unfold MapDisjoint_2.
     Apply eqmap_trans with m':=(MapDomRestrTo A B m0 m2). Apply eqmap_sym. Apply MapDomRestrTo_ext.
diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v
index a5155163b9..8fe4375611 100644
--- a/theories/Reals/DiscrR.v
+++ b/theories/Reals/DiscrR.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*i        $Id$       i*)
 
 Require Rbase.
 
diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
index f8b88f9c6e..b6024dcc7b 100644
--- a/theories/Reals/Rbase.v
+++ b/theories/Reals/Rbase.v
@@ -1314,7 +1314,8 @@ Save.
 
 (**********)
 Lemma single_z_r_R1
-  : (r:R)(z,x:Z)``r<(IZR z)``->``(IZR z)<=r+1``->``r<(IZR x)``->``(IZR x)<=r+1``->z=x.
+  : (r:R)(z,x:Z)``r<(IZR z)``->``(IZR z)<=r+1``->``r<(IZR x)``->``(IZR x)<=r+1``
+    ->z=x.
 Intros; Apply one_IZR_r_R1 with r; Auto.
 Save.
 
diff --git a/theories/Reals/SplitAbsolu.v b/theories/Reals/SplitAbsolu.v
index 3b423aefbf..ba2fbf5357 100644
--- a/theories/Reals/SplitAbsolu.v
+++ b/theories/Reals/SplitAbsolu.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(*      $Id$      *)
 
 Require Export Rbasic_fun.
 
diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v
index 1981080a2b..62fd1796eb 100644
--- a/theories/ZArith/Zsyntax.v
+++ b/theories/ZArith/Zsyntax.v
@@ -78,12 +78,12 @@ 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
+  enclosed into an ast (ZEXPR \$subexpr), which is printed like \$subexpr
   but without symbols "`" "`" around. 
 
-   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
+  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 *)