(One more) Minor layout adjustments for Library doc

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

2 files changed, 9 insertions, 9 deletions

diff --git a/theories/IntMap/Fset.v b/theories/IntMap/Fset.v
index 26bb5e8f35..3c00c21e09 100644
--- a/theories/IntMap/Fset.v
+++ b/theories/IntMap/Fset.v
@@ -246,8 +246,8 @@ Section FSetDefs.
       | (M2 m m') => (M2 unit (MapDom m) (MapDom m'))
     end.
 
-  Lemma MapDom_semantics_1 : (m:(Map A)) (a:ad) (y:A) (MapGet A m a)=(SOME A y) ->
-      (in_FSet a (MapDom m))=true.
+  Lemma MapDom_semantics_1 : (m:(Map A)) (a:ad) 
+      (y:A) (MapGet A m a)=(SOME A y) -> (in_FSet a (MapDom m))=true.
   Proof.
     Induction m. Intros. Discriminate H.
     Unfold MapDom. Unfold in_FSet. Unfold in_dom. Unfold MapGet. Intros a y a0 y0.
@@ -259,8 +259,8 @@ Section FSetDefs.
     Unfold in_FSet in_dom in H. Intro. Apply H with y:=y. Assumption.
   Qed.
 
-  Lemma MapDom_semantics_2 : (m:(Map A)) (a:ad) (in_FSet a (MapDom m))=true ->
-      {y:A | (MapGet A m a)=(SOME A y)}.
+  Lemma MapDom_semantics_2 : (m:(Map A)) (a:ad) 
+      (in_FSet a (MapDom m))=true -> {y:A | (MapGet A m a)=(SOME A y)}.
   Proof.
     Induction m. Intros. Discriminate H.
     Unfold MapDom. Unfold in_FSet. Unfold in_dom. Unfold MapGet. Intros a y a0. Case (ad_eq a a0).
@@ -272,16 +272,16 @@ Section FSetDefs.
     Unfold in_FSet in_dom in H. Intro. Apply H. Assumption.
   Qed.
 
-  Lemma MapDom_semantics_3 : (m:(Map A)) (a:ad) (MapGet A m a)=(NONE A) ->
-      (in_FSet a (MapDom m))=false.
+  Lemma MapDom_semantics_3 : (m:(Map A)) (a:ad) 
+      (MapGet A m a)=(NONE A) -> (in_FSet a (MapDom m))=false.
   Proof.
     Intros. Elim (sumbool_of_bool (in_FSet a (MapDom m))). Intro H0.
     Elim (MapDom_semantics_2 m a H0). Intros y H1. Rewrite H in H1. Discriminate H1.
     Trivial.
   Qed.
 
-  Lemma MapDom_semantics_4 : (m:(Map A)) (a:ad) (in_FSet a (MapDom m))=false ->
-      (MapGet A m a)=(NONE A).
+  Lemma MapDom_semantics_4 : (m:(Map A)) (a:ad) 
+      (in_FSet a (MapDom m))=false -> (MapGet A m a)=(NONE A).
   Proof.
     Intros. Elim (option_sum A (MapGet A m a)). Intro H0. Elim H0. Intros y H1.
     Rewrite (MapDom_semantics_1 m a y H1) in H. Discriminate H.
diff --git a/theories/IntMap/Mapcard.v b/theories/IntMap/Mapcard.v
index cb7e7f933a..e124a11f6b 100644
--- a/theories/IntMap/Mapcard.v
+++ b/theories/IntMap/Mapcard.v
@@ -297,7 +297,7 @@ Section MapCard.
   Qed.
 
   Lemma MapCard_Dom_Put_behind : (m:(Map A)) (a:ad) (y:A)
-    (MapDom A (MapPut_behind A m a y))=(MapDom A (MapPut A m a y)).
+      (MapDom A (MapPut_behind A m a y))=(MapDom A (MapPut A m a y)).
   Proof.
     Induction m. Trivial.
     Intros a y a0 y0. Simpl. Elim (ad_sum (ad_xor a a0)). Intro H. Elim H.