Updated PR by removing whitespaces. Bug 17450.

1 files changed, 73 insertions, 73 deletions

diff --git a/common/Values.v b/common/Values.v
index 8877f9a7..688e63ed 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -58,7 +58,7 @@ Module Val.
 
 Definition eq (x y: val): {x=y} + {x<>y}.
 Proof.
-  decide equality. 
+  decide equality.
   apply Int.eq_dec.
   apply Int64.eq_dec.
   apply Float.eq_dec.
@@ -809,14 +809,14 @@ Qed.
 Theorem cast8unsigned_and:
   forall x, zero_ext 8 x = and x (Vint(Int.repr 255)).
 Proof.
-  destruct x; simpl; auto. decEq. 
-  change 255 with (two_p 8 - 1). apply Int.zero_ext_and. omega. 
+  destruct x; simpl; auto. decEq.
+  change 255 with (two_p 8 - 1). apply Int.zero_ext_and. omega.
 Qed.
 
 Theorem cast16unsigned_and:
   forall x, zero_ext 16 x = and x (Vint(Int.repr 65535)).
 Proof.
-  destruct x; simpl; auto. decEq. 
+  destruct x; simpl; auto. decEq.
   change 65535 with (two_p 16 - 1). apply Int.zero_ext_and. omega.
 Qed.
 
@@ -829,7 +829,7 @@ Qed.
 Theorem bool_of_val_of_optbool:
   forall ob b, bool_of_val (of_optbool ob) b -> ob = Some b.
 Proof.
-  intros. destruct ob; simpl in H. 
+  intros. destruct ob; simpl in H.
   destruct b0; simpl in H; inv H; auto.
   inv H.
 Qed.
@@ -861,7 +861,7 @@ Qed.
 Theorem notbool_idem3:
   forall x, notbool(notbool(notbool x)) = notbool x.
 Proof.
-  destruct x; simpl; auto. 
+  destruct x; simpl; auto.
   case (Int.eq i Int.zero); reflexivity.
 Qed.
 
@@ -883,7 +883,7 @@ Proof.
   rewrite Int.add_assoc; auto.
   rewrite Int.add_assoc; auto.
   decEq. decEq. apply Int.add_commut.
-  decEq. rewrite Int.add_commut. rewrite <- Int.add_assoc. 
+  decEq. rewrite Int.add_commut. rewrite <- Int.add_assoc.
   decEq. apply Int.add_commut.
   decEq. rewrite Int.add_assoc. auto.
 Qed.
@@ -896,8 +896,8 @@ Qed.
 Theorem add_permut_4:
   forall x y z t, add (add x y) (add z t) = add (add x z) (add y t).
 Proof.
-  intros. rewrite add_permut. rewrite add_assoc. 
-  rewrite add_permut. symmetry. apply add_assoc. 
+  intros. rewrite add_permut. rewrite add_assoc.
+  rewrite add_permut. symmetry. apply add_assoc.
 Qed.
 
 Theorem neg_zero: neg Vzero = Vzero.
@@ -912,7 +912,7 @@ Qed.
 
 Theorem sub_zero_r: forall x, sub Vzero x = neg x.
 Proof.
-  destruct x; simpl; auto. 
+  destruct x; simpl; auto.
 Qed.
 
 Theorem sub_add_opp: forall x y, sub x (Vint y) = add x (Vint (Int.neg y)).
@@ -940,11 +940,11 @@ Theorem sub_add_r:
 Proof.
   destruct v1; destruct v2; intros; simpl; auto.
   rewrite Int.sub_add_r. auto.
-  repeat rewrite Int.sub_add_opp. decEq. 
+  repeat rewrite Int.sub_add_opp. decEq.
   repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  decEq. repeat rewrite Int.sub_add_opp. 
+  decEq. repeat rewrite Int.sub_add_opp.
   rewrite Int.add_assoc. decEq. apply Int.neg_add_distr.
-  case (eq_block b b0); intro. simpl. decEq. 
+  case (eq_block b b0); intro. simpl. decEq.
   repeat rewrite Int.sub_add_opp. rewrite Int.add_assoc. decEq.
   apply Int.neg_add_distr.
   reflexivity.
@@ -984,7 +984,7 @@ Proof.
   intros; destruct x; simpl; auto.
   change 32 with Int.zwordsize.
   rewrite (Int.is_power2_range _ _ H). decEq. apply Int.mul_pow2. auto.
-Qed.  
+Qed.
 
 Theorem mods_divs:
   forall x y z,
@@ -993,7 +993,7 @@ Proof.
   intros. destruct x; destruct y; simpl in *; try discriminate.
   destruct (Int.eq i0 Int.zero
         || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H.
-  exists (Vint (Int.divs i i0)); split; auto. 
+  exists (Vint (Int.divs i i0)); split; auto.
   simpl. rewrite Int.mods_divs. auto.
 Qed.
 
@@ -1002,10 +1002,10 @@ Theorem modu_divu:
   modu x y = Some z -> exists v, divu x y = Some v /\ z = sub x (mul v y).
 Proof.
   intros. destruct x; destruct y; simpl in *; try discriminate.
-  destruct (Int.eq i0 Int.zero) eqn:?; inv H. 
-  exists (Vint (Int.divu i i0)); split; auto. 
+  destruct (Int.eq i0 Int.zero) eqn:?; inv H.
+  exists (Vint (Int.divu i i0)); split; auto.
   simpl. rewrite Int.modu_divu. auto.
-  generalize (Int.eq_spec i0 Int.zero). rewrite Heqb; auto. 
+  generalize (Int.eq_spec i0 Int.zero). rewrite Heqb; auto.
 Qed.
 
 Theorem divs_pow2:
@@ -1027,8 +1027,8 @@ Theorem divu_pow2:
   shru x (Vint logn) = y.
 Proof.
   intros; destruct x; simpl in H0; inv H0.
-  destruct (Int.eq n Int.zero); inv H2. 
-  simpl. 
+  destruct (Int.eq n Int.zero); inv H2.
+  simpl.
   rewrite (Int.is_power2_range _ _ H).
   decEq. symmetry. apply Int.divu_pow2. auto.
 Qed.
@@ -1040,7 +1040,7 @@ Theorem modu_pow2:
   and x (Vint (Int.sub n Int.one)) = y.
 Proof.
   intros; destruct x; simpl in H0; inv H0.
-  destruct (Int.eq n Int.zero); inv H2. 
+  destruct (Int.eq n Int.zero); inv H2.
   simpl. decEq. symmetry. eapply Int.modu_and; eauto.
 Qed.
 
@@ -1079,12 +1079,12 @@ Qed.
 
 Theorem not_xor: forall x, notint x = xor x (Vint Int.mone).
 Proof.
-  destruct x; simpl; auto. 
+  destruct x; simpl; auto.
 Qed.
 
 Theorem shl_mul: forall x y, mul x (shl Vone y) = shl x y.
 Proof.
-  destruct x; destruct y; simpl; auto. 
+  destruct x; destruct y; simpl; auto.
   case (Int.ltu i0 Int.iwordsize); auto.
   decEq. symmetry. apply Int.shl_mul.
 Qed.
@@ -1112,11 +1112,11 @@ Theorem shrx_carry:
   shrx x y = Some z ->
   add (shr x y) (shr_carry x y) = z.
 Proof.
-  intros. destruct x; destruct y; simpl in H; inv H. 
+  intros. destruct x; destruct y; simpl in H; inv H.
   destruct (Int.ltu i0 (Int.repr 31)) eqn:?; inv H1.
   exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 31)) with 31. intros.
-  assert (Int.ltu i0 Int.iwordsize = true). 
-    unfold Int.ltu. apply zlt_true. change (Int.unsigned Int.iwordsize) with 32. omega. 
+  assert (Int.ltu i0 Int.iwordsize = true).
+    unfold Int.ltu. apply zlt_true. change (Int.unsigned Int.iwordsize) with 32. omega.
   simpl. rewrite H0. simpl. decEq. rewrite Int.shrx_carry; auto.
 Qed.
 
@@ -1127,12 +1127,12 @@ Theorem shrx_shr:
     x = Vint p /\ y = Vint q /\
     z = shr (if Int.lt p Int.zero then add x (Vint (Int.sub (Int.shl Int.one q) Int.one)) else x) (Vint q).
 Proof.
-  intros. destruct x; destruct y; simpl in H; inv H. 
+  intros. destruct x; destruct y; simpl in H; inv H.
   destruct (Int.ltu i0 (Int.repr 31)) eqn:?; inv H1.
   exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 31)) with 31. intros.
-  assert (Int.ltu i0 Int.iwordsize = true). 
-    unfold Int.ltu. apply zlt_true. change (Int.unsigned Int.iwordsize) with 32. omega. 
-  exists i; exists i0; intuition. 
+  assert (Int.ltu i0 Int.iwordsize = true).
+    unfold Int.ltu. apply zlt_true. change (Int.unsigned Int.iwordsize) with 32. omega.
+  exists i; exists i0; intuition.
   rewrite Int.shrx_shr; auto. destruct (Int.lt i Int.zero); simpl; rewrite H0; auto.
 Qed.
 
@@ -1151,7 +1151,7 @@ Theorem rolm_rolm:
            (Int.and (Int.rol m1 n2) m2).
 Proof.
   intros; destruct x; simpl; auto.
-  decEq. 
+  decEq.
   apply Int.rolm_rolm. apply int_wordsize_divides_modulus.
 Qed.
 
@@ -1174,10 +1174,10 @@ Theorem negate_cmpu_bool:
 Proof.
   assert (forall c,
     cmp_different_blocks (negate_comparison c) = option_map negb (cmp_different_blocks c)).
-  destruct c; auto. 
+  destruct c; auto.
   destruct x; destruct y; simpl; auto.
   rewrite Int.negate_cmpu. auto.
-  destruct (Int.eq i Int.zero && (valid_ptr b (Int.unsigned i0) || valid_ptr b (Int.unsigned i0 - 1))); auto. 
+  destruct (Int.eq i Int.zero && (valid_ptr b (Int.unsigned i0) || valid_ptr b (Int.unsigned i0 - 1))); auto.
   destruct (Int.eq i0 Int.zero && (valid_ptr b (Int.unsigned i) || valid_ptr b (Int.unsigned i - 1))); auto.
   destruct (eq_block b b0).
   destruct ((valid_ptr b (Int.unsigned i) || valid_ptr b (Int.unsigned i - 1)) &&
@@ -1190,7 +1190,7 @@ Qed.
 Lemma not_of_optbool:
   forall ob, of_optbool (option_map negb ob) = notbool (of_optbool ob).
 Proof.
-  destruct ob; auto. destruct b; auto. 
+  destruct ob; auto. destruct b; auto.
 Qed.
 
 Theorem negate_cmp:
@@ -1240,21 +1240,21 @@ Qed.
 Theorem negate_cmpf_eq:
   forall v1 v2, notbool (cmpf Cne v1 v2) = cmpf Ceq v1 v2.
 Proof.
-  destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool. 
+  destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool.
   rewrite Float.cmp_ne_eq. destruct (Float.cmp Ceq f f0); auto.
 Qed.
 
 Theorem negate_cmpf_ne:
   forall v1 v2, notbool (cmpf Ceq v1 v2) = cmpf Cne v1 v2.
 Proof.
-  destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool. 
+  destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool.
   rewrite Float.cmp_ne_eq. destruct (Float.cmp Ceq f f0); auto.
 Qed.
 
 Theorem cmpf_le:
   forall v1 v2, cmpf Cle v1 v2 = or (cmpf Clt v1 v2) (cmpf Ceq v1 v2).
 Proof.
-  destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool. 
+  destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool.
   rewrite Float.cmp_le_lt_eq.
   destruct (Float.cmp Clt f f0); destruct (Float.cmp Ceq f f0); auto.
 Qed.
@@ -1262,7 +1262,7 @@ Qed.
 Theorem cmpf_ge:
   forall v1 v2, cmpf Cge v1 v2 = or (cmpf Cgt v1 v2) (cmpf Ceq v1 v2).
 Proof.
-  destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool. 
+  destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool.
   rewrite Float.cmp_ge_gt_eq.
   destruct (Float.cmp Cgt f f0); destruct (Float.cmp Ceq f f0); auto.
 Qed.
@@ -1270,57 +1270,57 @@ Qed.
 Theorem cmp_ne_0_optbool:
   forall ob, cmp Cne (of_optbool ob) (Vint Int.zero) = of_optbool ob.
 Proof.
-  intros. destruct ob; simpl; auto. destruct b; auto. 
+  intros. destruct ob; simpl; auto. destruct b; auto.
 Qed.
 
 Theorem cmp_eq_1_optbool:
   forall ob, cmp Ceq (of_optbool ob) (Vint Int.one) = of_optbool ob.
 Proof.
-  intros. destruct ob; simpl; auto. destruct b; auto. 
+  intros. destruct ob; simpl; auto. destruct b; auto.
 Qed.
 
 Theorem cmp_eq_0_optbool:
   forall ob, cmp Ceq (of_optbool ob) (Vint Int.zero) = of_optbool (option_map negb ob).
 Proof.
-  intros. destruct ob; simpl; auto. destruct b; auto. 
+  intros. destruct ob; simpl; auto. destruct b; auto.
 Qed.
 
 Theorem cmp_ne_1_optbool:
   forall ob, cmp Cne (of_optbool ob) (Vint Int.one) = of_optbool (option_map negb ob).
 Proof.
-  intros. destruct ob; simpl; auto. destruct b; auto. 
+  intros. destruct ob; simpl; auto. destruct b; auto.
 Qed.
 
 Theorem cmpu_ne_0_optbool:
   forall valid_ptr ob,
   cmpu valid_ptr Cne (of_optbool ob) (Vint Int.zero) = of_optbool ob.
 Proof.
-  intros. destruct ob; simpl; auto. destruct b; auto. 
+  intros. destruct ob; simpl; auto. destruct b; auto.
 Qed.
 
 Theorem cmpu_eq_1_optbool:
   forall valid_ptr ob,
   cmpu valid_ptr Ceq (of_optbool ob) (Vint Int.one) = of_optbool ob.
 Proof.
-  intros. destruct ob; simpl; auto. destruct b; auto. 
+  intros. destruct ob; simpl; auto. destruct b; auto.
 Qed.
 
 Theorem cmpu_eq_0_optbool:
   forall valid_ptr ob,
   cmpu valid_ptr Ceq (of_optbool ob) (Vint Int.zero) = of_optbool (option_map negb ob).
 Proof.
-  intros. destruct ob; simpl; auto. destruct b; auto. 
+  intros. destruct ob; simpl; auto. destruct b; auto.
 Qed.
 
 Theorem cmpu_ne_1_optbool:
   forall valid_ptr ob,
   cmpu valid_ptr Cne (of_optbool ob) (Vint Int.one) = of_optbool (option_map negb ob).
 Proof.
-  intros. destruct ob; simpl; auto. destruct b; auto. 
+  intros. destruct ob; simpl; auto. destruct b; auto.
 Qed.
 
 Lemma zero_ext_and:
-  forall n v, 
+  forall n v,
   0 < n < Int.zwordsize ->
   Val.zero_ext n v = Val.and v (Vint (Int.repr (two_p n - 1))).
 Proof.
@@ -1332,8 +1332,8 @@ Lemma rolm_lt_zero:
 Proof.
   intros. unfold cmp, cmp_bool; destruct v; simpl; auto.
   transitivity (Vint (Int.shru i (Int.repr (Int.zwordsize - 1)))).
-  decEq. symmetry. rewrite Int.shru_rolm. auto. auto. 
-  rewrite Int.shru_lt_zero. destruct (Int.lt i Int.zero); auto. 
+  decEq. symmetry. rewrite Int.shru_rolm. auto. auto.
+  rewrite Int.shru_lt_zero. destruct (Int.lt i Int.zero); auto.
 Qed.
 
 Lemma rolm_ge_zero:
@@ -1344,7 +1344,7 @@ Proof.
   unfold cmp; simpl. destruct (Int.lt i Int.zero); auto.
 Qed.
 
-(** The ``is less defined'' relation between values. 
+(** The ``is less defined'' relation between values.
     A value is less defined than itself, and [Vundef] is
     less defined than any value. *)
 
@@ -1379,7 +1379,7 @@ Lemma lessdef_list_inv:
 Proof.
   induction 1; simpl.
   tauto.
-  inv H. destruct IHlessdef_list. 
+  inv H. destruct IHlessdef_list.
   left; congruence. tauto. tauto.
 Qed.
 
@@ -1430,7 +1430,7 @@ Lemma cmpu_bool_lessdef:
   cmpu_bool valid_ptr c v1 v2 = Some b ->
   cmpu_bool valid_ptr' c v1' v2' = Some b.
 Proof.
-  intros. 
+  intros.
   assert (A: forall b ofs, valid_ptr b ofs || valid_ptr b (ofs - 1) = true ->
                            valid_ptr' b ofs || valid_ptr' b (ofs - 1) = true).
   { intros until ofs. rewrite ! orb_true_iff. intuition. }
@@ -1438,9 +1438,9 @@ Proof.
   destruct v2; simpl in H2; try discriminate;
   inv H0; inv H1; simpl; auto.
   destruct (Int.eq i Int.zero && (valid_ptr b0 (Int.unsigned i0) || valid_ptr b0 (Int.unsigned i0 - 1))) eqn:E; try discriminate.
-  InvBooleans. rewrite H0, A by auto. auto. 
+  InvBooleans. rewrite H0, A by auto. auto.
   destruct (Int.eq i0 Int.zero && (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1))) eqn:E; try discriminate.
-  InvBooleans. rewrite H0, A by auto. auto. 
+  InvBooleans. rewrite H0, A by auto. auto.
   destruct (eq_block b0 b1).
   destruct (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1)) eqn:?; try discriminate.
   destruct (valid_ptr b1 (Int.unsigned i0) || valid_ptr b1 (Int.unsigned i0 - 1)) eqn:?; try discriminate.
@@ -1455,7 +1455,7 @@ Lemma of_optbool_lessdef:
   (forall b, ob = Some b -> ob' = Some b) ->
   lessdef (of_optbool ob) (of_optbool ob').
 Proof.
-  intros. destruct ob; simpl; auto. rewrite (H b); auto. 
+  intros. destruct ob; simpl; auto. rewrite (H b); auto.
 Qed.
 
 Lemma longofwords_lessdef:
@@ -1468,13 +1468,13 @@ Qed.
 Lemma loword_lessdef:
   forall v v', lessdef v v' -> lessdef (loword v) (loword v').
 Proof.
-  intros. inv H; auto. 
+  intros. inv H; auto.
 Qed.
 
 Lemma hiword_lessdef:
   forall v v', lessdef v v' -> lessdef (hiword v) (hiword v').
 Proof.
-  intros. inv H; auto. 
+  intros. inv H; auto.
 Qed.
 
 (** * Values and memory injections *)
@@ -1513,12 +1513,12 @@ Inductive inject (mi: meminj): val -> val -> Prop :=
 
 Hint Constructors inject.
 
-Inductive inject_list (mi: meminj): list val -> list val-> Prop:= 
+Inductive inject_list (mi: meminj): list val -> list val-> Prop:=
   | inject_list_nil :
       inject_list mi nil nil
-  | inject_list_cons : forall v v' vl vl' , 
+  | inject_list_cons : forall v v' vl vl' ,
       inject mi v v' -> inject_list mi vl vl'->
-      inject_list mi (v :: vl) (v' :: vl').  
+      inject_list mi (v :: vl) (v' :: vl').
 
 Hint Resolve inject_list_nil inject_list_cons.
 
@@ -1553,7 +1553,7 @@ Remark sub_inject:
 Proof.
   intros. inv H; inv H0; simpl; auto.
   econstructor; eauto. rewrite Int.sub_add_l. auto.
-  destruct (eq_block b1 b0); auto. subst. rewrite H1 in H. inv H. rewrite dec_eq_true. 
+  destruct (eq_block b1 b0); auto. subst. rewrite H1 in H. inv H. rewrite dec_eq_true.
   rewrite Int.sub_shifted. auto.
 Qed.
 
@@ -1613,16 +1613,16 @@ Proof.
   fold (weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))).
   destruct (Int.eq i Int.zero); auto.
   destruct (weak_valid_ptr1 b1 (Int.unsigned ofs1)) eqn:E; try discriminate.
-  erewrite weak_valid_ptr_inj by eauto. auto. 
+  erewrite weak_valid_ptr_inj by eauto. auto.
 - fold (weak_valid_ptr1 b1 (Int.unsigned ofs1)) in H1.
   fold (weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))).
   destruct (Int.eq i Int.zero); auto.
   destruct (weak_valid_ptr1 b1 (Int.unsigned ofs1)) eqn:E; try discriminate.
-  erewrite weak_valid_ptr_inj by eauto. auto. 
+  erewrite weak_valid_ptr_inj by eauto. auto.
 - fold (weak_valid_ptr1 b1 (Int.unsigned ofs1)) in H1.
   fold (weak_valid_ptr1 b0 (Int.unsigned ofs0)) in H1.
   fold (weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))).
-  fold (weak_valid_ptr2 b3 (Int.unsigned (Int.add ofs0 (Int.repr delta0)))). 
+  fold (weak_valid_ptr2 b3 (Int.unsigned (Int.add ofs0 (Int.repr delta0)))).
   destruct (eq_block b1 b0); subst.
   rewrite H in H2. inv H2. rewrite dec_eq_true.
   destruct (weak_valid_ptr1 b0 (Int.unsigned ofs1)) eqn:?; try discriminate.
@@ -1633,7 +1633,7 @@ Proof.
   destruct (valid_ptr1 b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
   destruct (eq_block b2 b3); subst.
   assert (valid_ptr_implies: forall b ofs, valid_ptr1 b ofs = true -> weak_valid_ptr1 b ofs = true).
-    intros. unfold weak_valid_ptr1. rewrite H0; auto. 
+    intros. unfold weak_valid_ptr1. rewrite H0; auto.
   erewrite !weak_valid_ptr_inj by eauto using valid_ptr_implies. simpl.
   exploit valid_different_ptrs_inj; eauto. intros [?|?]; [congruence |].
   destruct c; simpl in H1; inv H1.
@@ -1652,13 +1652,13 @@ Qed.
 Lemma loword_inject:
   forall v v', inject f v v' -> inject f (Val.loword v) (Val.loword v').
 Proof.
-  intros. unfold Val.loword; inv H; auto. 
+  intros. unfold Val.loword; inv H; auto.
 Qed.
 
 Lemma hiword_inject:
   forall v v', inject f v v' -> inject f (Val.hiword v) (Val.hiword v').
 Proof.
-  intros. unfold Val.hiword; inv H; auto. 
+  intros. unfold Val.hiword; inv H; auto.
 Qed.
 
 End VAL_INJ_OPS.
@@ -1677,10 +1677,10 @@ Lemma inject_incr_refl :
 Proof. unfold inject_incr. auto. Qed.
 
 Lemma inject_incr_trans :
-  forall f1 f2 f3, 
+  forall f1 f2 f3,
   inject_incr f1 f2 -> inject_incr f2 f3 -> inject_incr f1 f3 .
 Proof.
-  unfold inject_incr; intros. eauto. 
+  unfold inject_incr; intros. eauto.
 Qed.
 
 Lemma val_inject_incr:
@@ -1707,7 +1707,7 @@ Lemma val_inject_lessdef:
   forall v1 v2, Val.lessdef v1 v2 <-> Val.inject (fun b => Some(b, 0)) v1 v2.
 Proof.
   intros; split; intros.
-  inv H; auto. destruct v2; econstructor; eauto. rewrite Int.add_zero; auto. 
+  inv H; auto. destruct v2; econstructor; eauto. rewrite Int.add_zero; auto.
   inv H; auto. inv H0. rewrite Int.add_zero; auto.
 Qed.
 
@@ -1728,7 +1728,7 @@ Lemma val_inject_id:
   Val.inject inject_id v1 v2 <-> Val.lessdef v1 v2.
 Proof.
   intros; split; intros.
-  inv H; auto. 
+  inv H; auto.
   unfold inject_id in H0. inv H0. rewrite Int.add_zero. constructor.
   inv H. destruct v2; econstructor. unfold inject_id; reflexivity. rewrite Int.add_zero; auto.
   constructor.
@@ -1753,6 +1753,6 @@ Lemma val_inject_compose:
   Val.inject (compose_meminj f f') v1 v3.
 Proof.
   intros. inv H; auto; inv H0; auto. econstructor.
-  unfold compose_meminj; rewrite H1; rewrite H3; eauto. 
+  unfold compose_meminj; rewrite H1; rewrite H3; eauto.
   rewrite Int.add_assoc. decEq. unfold Int.add. apply Int.eqm_samerepr. auto with ints.
-Qed. 
+Qed.