bug 17392: remove trailing whitespace in source files

15 files changed, 620 insertions, 620 deletions

diff --git a/powerpc/Archi.v b/powerpc/Archi.v
index cf1a0fe3..8ff11f08 100644
--- a/powerpc/Archi.v
+++ b/powerpc/Archi.v
@@ -25,13 +25,13 @@ Definition big_endian := true.
 Notation align_int64 := 8%Z (only parsing).
 Notation align_float64 := 8%Z (only parsing).
 
-Program Definition default_pl_64 : bool * nan_pl 53 := 
+Program Definition default_pl_64 : bool * nan_pl 53 :=
   (false, nat_iter 51 xO xH).
 
 Definition choose_binop_pl_64 (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) :=
   false.                        (**r always choose first NaN *)
 
-Program Definition default_pl_32 : bool * nan_pl 24 := 
+Program Definition default_pl_32 : bool * nan_pl 24 :=
   (false, nat_iter 22 xO xH).
 
 Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_pl 24) :=
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index c1cc1052..228977c2 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -109,7 +109,7 @@ Inductive constant: Type :=
 (** A note on constants: while immediate operands to PowerPC
   instructions must be representable in 16 bits (with
   sign extension or left shift by 16 positions for some instructions),
-  we do not attempt to capture these restrictions in the 
+  we do not attempt to capture these restrictions in the
   abstract syntax nor in the semantics.  The assembler will
   emit an error if immediate operands exceed the representable
   range.  Of course, our PPC generator (file [Asmgen]) is
@@ -190,9 +190,9 @@ Inductive instruction : Type :=
   | Pfcfid: freg -> freg -> instruction                       (**r signed-long-to-float conversion (PPC64) *)
   | Pfcti: ireg -> freg -> instruction                        (**r float-to-signed-int conversion, round towards 0 (pseudo) *)
   | Pfctiu: ireg -> freg -> instruction                       (**r float-to-unsigned-int conversion, round towards 0 (pseudo, PPC64) *)
-  | Pfctidz: freg -> freg -> instruction                      (**r float-to-signed-long conversion, round towards 0 (PPC64) *) 
-  | Pfctiw: freg -> freg -> instruction                       (**r float-to-signed-int conversion, round by default *) 
-  | Pfctiwz: freg -> freg -> instruction                      (**r float-to-signed-int conversion, round towards 0 *) 
+  | Pfctidz: freg -> freg -> instruction                      (**r float-to-signed-long conversion, round towards 0 (PPC64) *)
+  | Pfctiw: freg -> freg -> instruction                       (**r float-to-signed-int conversion, round by default *)
+  | Pfctiwz: freg -> freg -> instruction                      (**r float-to-signed-int conversion, round towards 0 *)
   | Pfdiv: freg -> freg -> freg -> instruction                (**r float division *)
   | Pfdivs: freg -> freg -> freg -> instruction               (**r float division *)
   | Pfmake: freg -> ireg -> ireg -> instruction               (**r build a float from 2 ints (pseudo) *)
@@ -380,7 +380,7 @@ Definition program := AST.program fundef unit.
   type [Tint], float registers to values of type [Tfloat],
   and boolean registers ([CARRY], [CR0_0], etc) to either
   [Vzero] or [Vone]. *)
-  
+
 Definition regset := Pregmap.t val.
 Definition genv := Genv.t fundef unit.
 
@@ -674,7 +674,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       end
   | Pbtbl r tbl =>
       match rs r with
-      | Vint n => 
+      | Vint n =>
           match list_nth_z tbl (Int.unsigned n) with
           | None => Stuck
           | Some lbl => goto_label f lbl (rs #GPR12 <- Vundef #CTR <- Vundef) m
@@ -1038,7 +1038,7 @@ Inductive final_state: state -> int -> Prop :=
       rs#PC = Vzero ->
       rs#GPR3 = Vint r ->
       final_state (State rs m) r.
-      
+
 Definition semantics (p: program) :=
   Semantics step (initial_state p) final_state (Genv.globalenv p).
 
@@ -1053,9 +1053,9 @@ Proof.
           forall vl2, list_forall2 (extcall_arg rs m) ll vl2 -> vl1 = vl2).
     induction 1; intros vl2 EA; inv EA.
     auto.
-    f_equal; auto. 
+    f_equal; auto.
     inv H; inv H3; congruence.
-  intros. red in H0; red in H1. eauto. 
+  intros. red in H0; red in H1. eauto.
 Qed.
 
 Lemma semantics_determinate: forall p, determinate (semantics p).
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index fe3a6441..4ad5e2f9 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -126,7 +126,7 @@ Definition accessind {A: Type}
        (instr1: A -> constant -> ireg -> instruction)
        (instr2: A -> ireg -> ireg -> instruction)
        (base: ireg) (ofs: int) (r: A) (k: code) :=
-  if Int.eq (high_s ofs) Int.zero 
+  if Int.eq (high_s ofs) Int.zero
   then instr1 r (Cint ofs) base :: k
   else loadimm GPR0 ofs (instr2 r base GPR0 :: k).
 
@@ -522,7 +522,7 @@ Definition int_temp_for (r: mreg) :=
 Definition transl_memory_access
      (mk1: constant -> ireg -> instruction)
      (mk2: ireg -> ireg -> instruction)
-     (addr: addressing) (args: list mreg) 
+     (addr: addressing) (args: list mreg)
      (temp: ireg) (k: code) :=
   match addr, args with
   | Aindexed ofs, a1 :: nil =>
@@ -649,12 +649,12 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
       OK (Pmtctr r1 ::
           Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 ::
           Pmtlr GPR0 ::
-          Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: 
+          Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::
           Pbctr sig :: k)
   | Mtailcall sig (inr symb) =>
       OK (Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 ::
           Pmtlr GPR0 ::
-          Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: 
+          Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::
           Pbs symb sig :: k)
   | Mbuiltin ef args res =>
       OK (Pbuiltin ef (List.map (map_builtin_arg preg_of) args) (map_builtin_res preg_of res) :: k)
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index ece6af1a..4e59b297 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -44,25 +44,25 @@ Let tge := Genv.globalenv tprog.
 Lemma symbols_preserved:
   forall id, Genv.find_symbol tge id = Genv.find_symbol ge id.
 Proof.
-  intros. unfold ge, tge. 
+  intros. unfold ge, tge.
   apply Genv.find_symbol_transf_partial with transf_fundef.
-  exact TRANSF. 
+  exact TRANSF.
 Qed.
 
 Lemma public_preserved:
   forall id, Genv.public_symbol tge id = Genv.public_symbol ge id.
 Proof.
-  intros. unfold ge, tge. 
+  intros. unfold ge, tge.
   apply Genv.public_symbol_transf_partial with transf_fundef.
-  exact TRANSF. 
+  exact TRANSF.
 Qed.
 
 Lemma varinfo_preserved:
   forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
 Proof.
-  intros. unfold ge, tge. 
+  intros. unfold ge, tge.
   apply Genv.find_var_info_transf_partial with transf_fundef.
-  exact TRANSF. 
+  exact TRANSF.
 Qed.
 
 Lemma functions_translated:
@@ -78,7 +78,7 @@ Lemma functions_transl:
   transf_function f = OK tf ->
   Genv.find_funct_ptr tge b = Some (Internal tf).
 Proof.
-  intros. 
+  intros.
   destruct (functions_translated _ _ H) as [tf' [A B]].
   rewrite A. monadInv B. f_equal. congruence.
 Qed.
@@ -89,7 +89,7 @@ Lemma transf_function_no_overflow:
   forall f tf,
   transf_function f = OK tf -> list_length_z tf.(fn_code) <= Int.max_unsigned.
 Proof.
-  intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z x.(fn_code))); inv EQ0. 
+  intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z x.(fn_code))); inv EQ0.
   omega.
 Qed.
 
@@ -102,7 +102,7 @@ Proof.
   intros. inv H.
   eapply exec_straight_steps_1; eauto.
   eapply transf_function_no_overflow; eauto.
-  eapply functions_transl; eauto. 
+  eapply functions_transl; eauto.
 Qed.
 
 Lemma exec_straight_at:
@@ -112,8 +112,8 @@ Lemma exec_straight_at:
   exec_straight tge tf tc rs m tc' rs' m' ->
   transl_code_at_pc ge (rs' PC) fb f c' ep' tf tc'.
 Proof.
-  intros. inv H. 
-  exploit exec_straight_steps_2; eauto. 
+  intros. inv H.
+  exploit exec_straight_steps_2; eauto.
   eapply transf_function_no_overflow; eauto.
   eapply functions_transl; eauto.
   intros [ofs' [PC' CT']].
@@ -141,7 +141,7 @@ Section TRANSL_LABEL.
 Remark loadimm_label:
   forall r n k, tail_nolabel k (loadimm r n k).
 Proof.
-  intros. unfold loadimm. 
+  intros. unfold loadimm.
   case (Int.eq (high_s n) Int.zero). TailNoLabel.
   case (Int.eq (low_s n) Int.zero); TailNoLabel.
 Qed.
@@ -150,7 +150,7 @@ Hint Resolve loadimm_label: labels.
 Remark addimm_label:
   forall r1 r2 n k, tail_nolabel k (addimm r1 r2 n k).
 Proof.
-  intros; unfold addimm. 
+  intros; unfold addimm.
   case (Int.eq (high_s n) Int.zero). TailNoLabel.
   case (Int.eq (low_s n) Int.zero); TailNoLabel.
 Qed.
@@ -159,7 +159,7 @@ Hint Resolve addimm_label: labels.
 Remark andimm_base_label:
   forall r1 r2 n k, tail_nolabel k (andimm_base r1 r2 n k).
 Proof.
-  intros; unfold andimm_base. 
+  intros; unfold andimm_base.
   case (Int.eq (high_u n) Int.zero). TailNoLabel.
   case (Int.eq (low_u n) Int.zero). TailNoLabel.
   eapply tail_nolabel_trans; TailNoLabel.
@@ -169,7 +169,7 @@ Hint Resolve andimm_base_label: labels.
 Remark andimm_label:
   forall r1 r2 n k, tail_nolabel k (andimm r1 r2 n k).
 Proof.
-  intros; unfold andimm. 
+  intros; unfold andimm.
   case (is_rlw_mask n); TailNoLabel.
 Qed.
 Hint Resolve andimm_label: labels.
@@ -177,7 +177,7 @@ Hint Resolve andimm_label: labels.
 Remark orimm_label:
   forall r1 r2 n k, tail_nolabel k (orimm r1 r2 n k).
 Proof.
-  intros; unfold orimm. 
+  intros; unfold orimm.
   case (Int.eq (high_u n) Int.zero). TailNoLabel.
   case (Int.eq (low_u n) Int.zero); TailNoLabel.
 Qed.
@@ -186,7 +186,7 @@ Hint Resolve orimm_label: labels.
 Remark xorimm_label:
   forall r1 r2 n k, tail_nolabel k (xorimm r1 r2 n k).
 Proof.
-  intros; unfold xorimm. 
+  intros; unfold xorimm.
   case (Int.eq (high_u n) Int.zero). TailNoLabel.
   case (Int.eq (low_u n) Int.zero); TailNoLabel.
 Qed.
@@ -195,7 +195,7 @@ Hint Resolve xorimm_label: labels.
 Remark rolm_label:
   forall r1 r2 amount mask k, tail_nolabel k (rolm r1 r2 amount mask k).
 Proof.
-  intros; unfold rolm. 
+  intros; unfold rolm.
   case (is_rlw_mask mask); TailNoLabel.
 Qed.
 Hint Resolve rolm_label: labels.
@@ -291,7 +291,7 @@ Proof.
   destruct m; monadInv H; eapply transl_memory_access_label; TailNoLabel.
   destruct s0; monadInv H; TailNoLabel.
   destruct s0; monadInv H; TailNoLabel.
-  eapply tail_nolabel_trans. eapply transl_cond_label; eauto. 
+  eapply tail_nolabel_trans. eapply transl_cond_label; eauto.
   destruct (snd (crbit_for_cond c0)); TailNoLabel.
 Qed.
 
@@ -301,7 +301,7 @@ Lemma transl_instr_label':
   find_label lbl c = if Mach.is_label lbl i then Some k else find_label lbl k.
 Proof.
   intros. exploit transl_instr_label; eauto.
-  destruct i; try (intros [A B]; apply B). 
+  destruct i; try (intros [A B]; apply B).
   intros. subst c. simpl. auto.
 Qed.
 
@@ -316,7 +316,7 @@ Proof.
   induction c; simpl; intros.
   inv H. auto.
   monadInv H. rewrite (transl_instr_label' lbl _ _ _ _ _ EQ0).
-  generalize (Mach.is_label_correct lbl a). 
+  generalize (Mach.is_label_correct lbl a).
   destruct (Mach.is_label lbl a); intros.
   subst a. simpl in EQ. exists x; auto.
   eapply IHc; eauto.
@@ -332,7 +332,7 @@ Lemma transl_find_label:
 Proof.
   intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z x.(fn_code))); inv EQ0.
   monadInv EQ. rewrite transl_code'_transl_code in EQ0.
-  simpl. eapply transl_code_label; eauto. 
+  simpl. eapply transl_code_label; eauto.
 Qed.
 
 End TRANSL_LABEL.
@@ -347,17 +347,17 @@ Lemma find_label_goto_label:
   rs PC = Vptr b ofs ->
   Mach.find_label lbl f.(Mach.fn_code) = Some c' ->
   exists tc', exists rs',
-    goto_label tf lbl rs m = Next rs' m  
+    goto_label tf lbl rs m = Next rs' m
   /\ transl_code_at_pc ge (rs' PC) b f c' false tf tc'
   /\ forall r, r <> PC -> rs'#r = rs#r.
 Proof.
-  intros. exploit (transl_find_label lbl f tf); eauto. rewrite H2. 
+  intros. exploit (transl_find_label lbl f tf); eauto. rewrite H2.
   intros [tc [A B]].
   exploit label_pos_code_tail; eauto. instantiate (1 := 0).
   intros [pos' [P [Q R]]].
   exists tc; exists (rs#PC <- (Vptr b (Int.repr pos'))).
   split. unfold goto_label. rewrite P. rewrite H1. auto.
-  split. rewrite Pregmap.gss. constructor; auto. 
+  split. rewrite Pregmap.gss. constructor; auto.
   rewrite Int.unsigned_repr. replace (pos' - 0) with pos' in Q.
   auto. omega.
   generalize (transf_function_no_overflow _ _ H0). omega.
@@ -370,10 +370,10 @@ Lemma return_address_exists:
   forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) ->
   exists ra, return_address_offset f c ra.
 Proof.
-  intros. eapply Asmgenproof0.return_address_exists; eauto. 
-- intros. exploit transl_instr_label; eauto. 
+  intros. eapply Asmgenproof0.return_address_exists; eauto.
+- intros. exploit transl_instr_label; eauto.
   destruct i; try (intros [A B]; apply A). intros. subst c0. repeat constructor.
-- intros. monadInv H0. 
+- intros. monadInv H0.
   destruct (zlt Int.max_unsigned (list_length_z x.(fn_code))); inv EQ0. monadInv EQ.
   rewrite transl_code'_transl_code in EQ0.
   exists x; exists false; split; auto. unfold fn_code. repeat constructor.
@@ -442,10 +442,10 @@ Lemma exec_straight_steps:
   plus step tge (State rs1 m1') E0 st' /\
   match_states (Mach.State s fb sp c ms2 m2) st'.
 Proof.
-  intros. inversion H2. subst. monadInv H7. 
-  exploit H3; eauto. intros [rs2 [A [B C]]]. 
+  intros. inversion H2. subst. monadInv H7.
+  exploit H3; eauto. intros [rs2 [A [B C]]].
   exists (State rs2 m2'); split.
-  eapply exec_straight_exec; eauto. 
+  eapply exec_straight_exec; eauto.
   econstructor; eauto. eapply exec_straight_at; eauto.
 Qed.
 
@@ -470,15 +470,15 @@ Proof.
   exploit H5; eauto. intros [jmp [k' [rs2 [A [B C]]]]].
   generalize (functions_transl _ _ _ H7 H8); intro FN.
   generalize (transf_function_no_overflow _ _ H8); intro NOOV.
-  exploit exec_straight_steps_2; eauto. 
+  exploit exec_straight_steps_2; eauto.
   intros [ofs' [PC2 CT2]].
-  exploit find_label_goto_label; eauto. 
+  exploit find_label_goto_label; eauto.
   intros [tc' [rs3 [GOTO [AT' OTH]]]].
   exists (State rs3 m2'); split.
   eapply plus_right'.
-  eapply exec_straight_steps_1; eauto. 
+  eapply exec_straight_steps_1; eauto.
   econstructor; eauto.
-  eapply find_instr_tail. eauto. 
+  eapply find_instr_tail. eauto.
   rewrite C. eexact GOTO.
   traceEq.
   econstructor; eauto.
@@ -503,7 +503,7 @@ Definition measure (s: Mach.state) : nat :=
 
 Remark preg_of_not_GPR11: forall r, negb (mreg_eq r R11) = true -> IR GPR11 <> preg_of r.
 Proof.
-  intros. change (IR GPR11) with (preg_of R11). red; intros. 
+  intros. change (IR GPR11) with (preg_of R11). red; intros.
   exploit preg_of_injective; eauto. intros; subst r; discriminate.
 Qed.
 
@@ -518,8 +518,8 @@ Proof.
   induction 1; intros; inv MS.
 
 - (* Mlabel *)
-  left; eapply exec_straight_steps; eauto; intros. 
-  monadInv TR. econstructor; split. apply exec_straight_one. simpl; eauto. auto. 
+  left; eapply exec_straight_steps; eauto; intros.
+  monadInv TR. econstructor; split. apply exec_straight_one. simpl; eauto. auto.
   split. apply agree_nextinstr; auto. simpl; congruence.
 
 - (* Mgetstack *)
@@ -535,51 +535,51 @@ Proof.
 - (* Msetstack *)
   unfold store_stack in H.
   assert (Val.lessdef (rs src) (rs0 (preg_of src))). eapply preg_val; eauto.
-  exploit Mem.storev_extends; eauto. intros [m2' [A B]]. 
+  exploit Mem.storev_extends; eauto. intros [m2' [A B]].
   left; eapply exec_straight_steps; eauto.
   rewrite (sp_val _ _ _ AG) in A. intros. simpl in TR.
   exploit storeind_correct; eauto with asmgen. intros [rs' [P Q]].
   exists rs'; split. eauto.
   split. eapply agree_undef_regs; eauto with asmgen.
-  simpl; intros. rewrite Q; auto with asmgen. 
+  simpl; intros. rewrite Q; auto with asmgen.
 
 - (* Mgetparam *)
   assert (f0 = f) by congruence; subst f0.
-  unfold load_stack in *. 
-  exploit Mem.loadv_extends. eauto. eexact H0. auto. 
+  unfold load_stack in *.
+  exploit Mem.loadv_extends. eauto. eexact H0. auto.
   intros [parent' [A B]]. rewrite (sp_val _ _ _ AG) in A.
   exploit lessdef_parent_sp; eauto. clear B; intros B; subst parent'.
-  exploit Mem.loadv_extends. eauto. eexact H1. auto. 
+  exploit Mem.loadv_extends. eauto. eexact H1. auto.
   intros [v' [C D]].
 Opaque loadind.
   left; eapply exec_straight_steps; eauto; intros.
-  destruct ep; simpl in TR. 
+  destruct ep; simpl in TR.
 (* GPR11 contains parent *)
   exploit loadind_correct. eexact TR.
   instantiate (2 := rs0). rewrite DXP; eauto.  congruence.
   intros [rs1 [P [Q R]]].
-  exists rs1; split. eauto. 
+  exists rs1; split. eauto.
   split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen.
-  simpl; intros. rewrite R; auto with asmgen. 
+  simpl; intros. rewrite R; auto with asmgen.
   apply preg_of_not_GPR11; auto.
 (* GPR11 does not contain parent *)
-  monadInv TR.  
+  monadInv TR.
   exploit loadind_correct. eexact EQ0. eauto. congruence. intros [rs1 [P [Q R]]]. simpl in Q.
   exploit loadind_correct. eexact EQ. instantiate (2 := rs1). rewrite Q. eauto. congruence.
-  intros [rs2 [S [T U]]]. 
+  intros [rs2 [S [T U]]].
   exists rs2; split. eapply exec_straight_trans; eauto.
   split. eapply agree_set_mreg. eapply agree_set_mreg. eauto. eauto.
   instantiate (1 := rs1#GPR11 <- (rs2#GPR11)). intros.
   rewrite Pregmap.gso; auto with asmgen.
-  congruence. intros. unfold Pregmap.set. destruct (PregEq.eq r' GPR11). congruence. auto with asmgen. 
-  simpl; intros. rewrite U; auto with asmgen. 
+  congruence. intros. unfold Pregmap.set. destruct (PregEq.eq r' GPR11). congruence. auto with asmgen.
+  simpl; intros. rewrite U; auto with asmgen.
   apply preg_of_not_GPR11; auto.
 
 - (* Mop *)
-  assert (eval_operation tge sp op rs##args m = Some v). 
+  assert (eval_operation tge sp op rs##args m = Some v).
     rewrite <- H. apply eval_operation_preserved. exact symbols_preserved.
   exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eexact H0.
-  intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A. 
+  intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A.
   left; eapply exec_straight_steps; eauto; intros. simpl in TR.
   exploit transl_op_correct; eauto. intros [rs2 [P [Q R]]].
   exists rs2; split. eauto. split. auto.
@@ -589,34 +589,34 @@ Opaque loadind.
   change (destroyed_by_op Omove) with (@nil mreg). simpl; auto.
 
 - (* Mload *)
-  assert (eval_addressing tge sp addr rs##args = Some a). 
+  assert (eval_addressing tge sp addr rs##args = Some a).
     rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
   exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1.
   intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.
   exploit Mem.loadv_extends; eauto. intros [v' [C D]].
   left; eapply exec_straight_steps; eauto; intros. simpl in TR.
-  exploit transl_load_correct; eauto. intros [rs2 [P [Q R]]]. 
+  exploit transl_load_correct; eauto. intros [rs2 [P [Q R]]].
   exists rs2; split. eauto.
   split. eapply agree_set_undef_mreg; eauto. congruence.
-  intros; auto with asmgen. 
+  intros; auto with asmgen.
   simpl; congruence.
 
 - (* Mstore *)
-  assert (eval_addressing tge sp addr rs##args = Some a). 
+  assert (eval_addressing tge sp addr rs##args = Some a).
     rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
   exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1.
   intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.
   assert (Val.lessdef (rs src) (rs0 (preg_of src))). eapply preg_val; eauto.
   exploit Mem.storev_extends; eauto. intros [m2' [C D]].
   left; eapply exec_straight_steps; eauto.
-  intros. simpl in TR. exploit transl_store_correct; eauto. intros [rs2 [P Q]]. 
+  intros. simpl in TR. exploit transl_store_correct; eauto. intros [rs2 [P Q]].
   exists rs2; split. eauto.
   split. eapply agree_undef_regs; eauto with asmgen.
   simpl; congruence.
 
 - (* Mcall *)
   assert (f0 = f) by congruence.  subst f0.
-  inv AT. 
+  inv AT.
   assert (NOOV: list_length_z tf.(fn_code) <= Int.max_unsigned).
     eapply transf_function_no_overflow; eauto.
   destruct ros as [rf|fid]; simpl in H; monadInv H5.
@@ -633,27 +633,27 @@ Opaque loadind.
   exploit return_address_offset_correct; eauto. intros; subst ra.
   left; econstructor; split.
   eapply plus_left. eapply exec_step_internal. eauto.
-  eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
+  eapply functions_transl; eauto. eapply find_instr_tail; eauto.
   simpl. eauto.
   apply star_one. eapply exec_step_internal. Simpl. rewrite <- H2; simpl; eauto.
-  eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
+  eapply functions_transl; eauto. eapply find_instr_tail; eauto.
   simpl. eauto.
   traceEq.
-  econstructor; eauto. 
-  econstructor; eauto. 
+  econstructor; eauto.
+  econstructor; eauto.
   eapply agree_sp_def; eauto.
-  simpl. eapply agree_exten; eauto. intros. Simpl. 
+  simpl. eapply agree_exten; eauto. intros. Simpl.
   Simpl. rewrite <- H2. auto.
 + (* Direct call *)
   generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1.
   assert (TCA: transl_code_at_pc ge (Vptr fb (Int.add ofs Int.one)) fb f c false tf x).
-    econstructor; eauto. 
+    econstructor; eauto.
   exploit return_address_offset_correct; eauto. intros; subst ra.
   left; econstructor; split.
   apply plus_one. eapply exec_step_internal. eauto.
-  eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
+  eapply functions_transl; eauto. eapply find_instr_tail; eauto.
   simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. eauto.
-  econstructor; eauto. 
+  econstructor; eauto.
   econstructor; eauto.
   eapply agree_sp_def; eauto.
   simpl. eapply agree_exten; eauto. intros. Simpl.
@@ -667,7 +667,7 @@ Opaque loadind.
   exploit Mem.loadv_extends. eauto. eexact H2. auto. simpl. intros [ra' [C D]].
   exploit lessdef_parent_sp; eauto. intros. subst parent'. clear B.
   exploit lessdef_parent_ra; eauto. intros. subst ra'. clear D.
-  exploit Mem.free_parallel_extends; eauto. intros [m2' [E F]]. 
+  exploit Mem.free_parallel_extends; eauto. intros [m2' [E F]].
   destruct ros as [rf|fid]; simpl in H; monadInv H7.
 + (* Indirect call *)
   assert (rs rf = Vptr f' Int.zero).
@@ -685,16 +685,16 @@ Opaque loadind.
               :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pbctr sig :: x)
             rs0 m'0
             (Pbctr sig :: x) rs5 m2').
-  apply exec_straight_step with rs2 m'0. 
+  apply exec_straight_step with rs2 m'0.
   simpl. rewrite H9. auto. auto.
   apply exec_straight_step with rs3 m'0.
   simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low.
-  change (rs2 GPR1) with (rs0 GPR1). rewrite <- (sp_val _ _ _ AG). 
+  change (rs2 GPR1) with (rs0 GPR1). rewrite <- (sp_val _ _ _ AG).
   simpl. rewrite C. auto. congruence. auto.
   apply exec_straight_step with rs4 m'0.
   simpl. reflexivity. reflexivity.
-  apply exec_straight_one. 
-  simpl. change (rs4 GPR1) with (rs0 GPR1). rewrite <- (sp_val _ _ _ AG). 
+  apply exec_straight_one.
+  simpl. change (rs4 GPR1) with (rs0 GPR1). rewrite <- (sp_val _ _ _ AG).
   simpl. rewrite A.
   rewrite E. reflexivity. reflexivity.
   left; exists (State rs6 m2'); split.
@@ -703,9 +703,9 @@ Opaque loadind.
   econstructor.
   change (rs5 PC) with (Val.add (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone) Vone).
   rewrite <- H4; simpl. eauto.
-  eapply functions_transl; eauto. 
+  eapply functions_transl; eauto.
   eapply find_instr_tail.
-  repeat (eapply code_tail_next_int; auto). eauto. 
+  repeat (eapply code_tail_next_int; auto). eauto.
   simpl. reflexivity. traceEq.
   (* match states *)
   econstructor; eauto.
@@ -713,8 +713,8 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen.
   assert (AG4: agree rs (Vptr stk soff) rs4).
     unfold rs4, rs3, rs2; auto 10 with asmgen.
   assert (AG5: agree rs (parent_sp s) rs5).
-    unfold rs5. apply agree_nextinstr. eapply agree_change_sp. eauto. 
-    eapply parent_sp_def; eauto. 
+    unfold rs5. apply agree_nextinstr. eapply agree_change_sp. eauto.
+    eapply parent_sp_def; eauto.
   unfold rs6, rs5; auto 10 with asmgen.
 + (* Direct call *)
   set (rs2 := nextinstr (rs0#GPR0 <- (parent_ra s))).
@@ -726,13 +726,13 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen.
              :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pbs fid sig :: x)
             rs0 m'0
             (Pbs fid sig :: x) rs4 m2').
-  apply exec_straight_step with rs2 m'0. 
+  apply exec_straight_step with rs2 m'0.
   simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low.
   rewrite <- (sp_val _ _ _ AG). simpl. rewrite C. auto. congruence. auto.
   apply exec_straight_step with rs3 m'0.
   simpl. reflexivity. reflexivity.
-  apply exec_straight_one. 
-  simpl. change (rs3 GPR1) with (rs0 GPR1). rewrite <- (sp_val _ _ _ AG). simpl. rewrite A. 
+  apply exec_straight_one.
+  simpl. change (rs3 GPR1) with (rs0 GPR1). rewrite <- (sp_val _ _ _ AG). simpl. rewrite A.
   rewrite E. reflexivity. reflexivity.
   left; exists (State rs5 m2'); split.
   (* execution *)
@@ -740,30 +740,30 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen.
   econstructor.
   change (rs4 PC) with (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone).
   rewrite <- H4; simpl. eauto.
-  eapply functions_transl; eauto. 
+  eapply functions_transl; eauto.
   eapply find_instr_tail.
-  repeat (eapply code_tail_next_int; auto). eauto. 
+  repeat (eapply code_tail_next_int; auto). eauto.
   simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. auto. traceEq.
   (* match states *)
   econstructor; eauto.
   assert (AG3: agree rs (Vptr stk soff) rs3).
     unfold rs3, rs2; auto 10 with asmgen.
   assert (AG4: agree rs (parent_sp s) rs4).
-    unfold rs4. apply agree_nextinstr. eapply agree_change_sp. eauto. 
-    eapply parent_sp_def; eauto. 
+    unfold rs4. apply agree_nextinstr. eapply agree_change_sp. eauto.
+    eapply parent_sp_def; eauto.
   unfold rs5; auto 10 with asmgen.
 
 - (* Mbuiltin *)
-  inv AT. monadInv H4. 
+  inv AT. monadInv H4.
   exploit functions_transl; eauto. intro FN.
   generalize (transf_function_no_overflow _ _ H3); intro NOOV.
-  exploit builtin_args_match; eauto. intros [vargs' [P Q]]. 
+  exploit builtin_args_match; eauto. intros [vargs' [P Q]].
   exploit external_call_mem_extends; eauto.
   intros [vres' [m2' [A [B [C D]]]]].
-  left. econstructor; split. apply plus_one. 
+  left. econstructor; split. apply plus_one.
   eapply exec_step_builtin. eauto. eauto.
   eapply find_instr_tail; eauto.
-  erewrite <- sp_val by eauto. 
+  erewrite <- sp_val by eauto.
   eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
   eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
@@ -777,12 +777,12 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen.
   rewrite preg_notin_charact. intros. auto with asmgen.
   auto with asmgen.
   apply agree_nextinstr. eapply agree_set_res; auto.
-  eapply agree_undef_regs; eauto. intros; apply undef_regs_other_2; auto. 
+  eapply agree_undef_regs; eauto. intros; apply undef_regs_other_2; auto.
   congruence.
 
 - (* Mgoto *)
   assert (f0 = f) by congruence. subst f0.
-  inv AT. monadInv H4. 
+  inv AT. monadInv H4.
   exploit find_label_goto_label; eauto. intros [tc' [rs' [GOTO [AT2 INV]]]].
   left; exists (State rs' m'); split.
   apply plus_one. econstructor; eauto.
@@ -802,13 +802,13 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen.
   rewrite EC in B.
   destruct (snd (crbit_for_cond cond)).
   (* Pbt, taken *)
-  econstructor; econstructor; econstructor; split. eexact A. 
+  econstructor; econstructor; econstructor; split. eexact A.
   split. eapply agree_exten; eauto with asmgen.
-  simpl. rewrite B. reflexivity. 
+  simpl. rewrite B. reflexivity.
   (* Pbf, taken *)
-  econstructor; econstructor; econstructor; split. eexact A. 
+  econstructor; econstructor; econstructor; split. eexact A.
   split. eapply agree_exten; eauto with asmgen.
-  simpl. rewrite B. reflexivity. 
+  simpl. rewrite B. reflexivity.
 
 - (* Mcond false *)
   exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
@@ -816,7 +816,7 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen.
   destruct (transl_cond_correct_1 tge tf cond args _ rs0 m' _ TR) as [rs' [A [B C]]].
   rewrite EC in B.
   econstructor; split.
-  eapply exec_straight_trans. eexact A. 
+  eapply exec_straight_trans. eexact A.
   destruct (snd (crbit_for_cond cond)).
   apply exec_straight_one. simpl. rewrite B. reflexivity. auto.
   apply exec_straight_one. simpl. rewrite B. reflexivity. auto.
@@ -826,23 +826,23 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen.
 
 - (* Mjumptable *)
   assert (f0 = f) by congruence. subst f0.
-  inv AT. monadInv H6. 
+  inv AT. monadInv H6.
   exploit functions_transl; eauto. intro FN.
   generalize (transf_function_no_overflow _ _ H5); intro NOOV.
   exploit find_label_goto_label. eauto. eauto.
-  instantiate (2 := rs0#GPR12 <- Vundef #CTR <- Vundef). 
+  instantiate (2 := rs0#GPR12 <- Vundef #CTR <- Vundef).
   Simpl. eauto.
-  eauto. 
+  eauto.
   intros [tc' [rs' [A [B C]]]].
   exploit ireg_val; eauto. rewrite H. intros LD; inv LD.
   left; econstructor; split.
-  apply plus_one. econstructor; eauto. 
-  eapply find_instr_tail; eauto. 
+  apply plus_one. econstructor; eauto.
+  eapply find_instr_tail; eauto.
   simpl. rewrite <- H9. unfold Mach.label in H0; unfold label; rewrite H0. eexact A.
-  econstructor; eauto. 
+  econstructor; eauto.
   eapply agree_undef_regs; eauto.
-Local Transparent destroyed_by_jumptable. 
-  simpl. intros. rewrite C; auto with asmgen. Simpl. 
+Local Transparent destroyed_by_jumptable.
+  simpl. intros. rewrite C; auto with asmgen. Simpl.
   congruence.
 
 - (* Mreturn *)
@@ -851,9 +851,9 @@ Local Transparent destroyed_by_jumptable.
   assert (NOOV: list_length_z tf.(fn_code) <= Int.max_unsigned).
     eapply transf_function_no_overflow; eauto.
   rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *.
-  exploit Mem.loadv_extends. eauto. eexact H0. auto. simpl. intros [parent' [A B]]. 
+  exploit Mem.loadv_extends. eauto. eexact H0. auto. simpl. intros [parent' [A B]].
   exploit lessdef_parent_sp; eauto. intros. subst parent'. clear B.
-  exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [ra' [C D]]. 
+  exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [ra' [C D]].
   exploit lessdef_parent_ra; eauto. intros. subst ra'. clear D.
   exploit Mem.free_parallel_extends; eauto. intros [m2' [E F]].
   monadInv H6.
@@ -868,43 +868,43 @@ Local Transparent destroyed_by_jumptable.
            (Pblr :: x) rs4 m2').
   simpl. apply exec_straight_three with rs2 m'0 rs3 m'0.
   simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low. rewrite C. auto. congruence.
-  simpl. auto. 
-  simpl. change (rs3 GPR1) with (rs0 GPR1). rewrite A. 
-  rewrite <- (sp_val _ _ _ AG). rewrite E. auto. 
-  auto. auto. auto. 
+  simpl. auto.
+  simpl. change (rs3 GPR1) with (rs0 GPR1). rewrite A.
+  rewrite <- (sp_val _ _ _ AG). rewrite E. auto.
+  auto. auto. auto.
   left; exists (State rs5 m2'); split.
   (* execution *)
   apply plus_right' with E0 (State rs4 m2') E0.
   eapply exec_straight_exec; eauto.
   econstructor.
-  change (rs4 PC) with (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone). 
+  change (rs4 PC) with (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone).
   rewrite <- H3. simpl. eauto.
   eapply functions_transl; eauto.
-  eapply find_instr_tail. 
+  eapply find_instr_tail.
   eapply code_tail_next_int; auto.
   eapply code_tail_next_int; auto.
   eapply code_tail_next_int; eauto.
   reflexivity. traceEq.
   (* match states *)
-  econstructor; eauto. 
-  assert (AG3: agree rs (Vptr stk soff) rs3). 
+  econstructor; eauto.
+  assert (AG3: agree rs (Vptr stk soff) rs3).
     unfold rs3, rs2; auto 10 with asmgen.
   assert (AG4: agree rs (parent_sp s) rs4).
-    unfold rs4. apply agree_nextinstr. eapply agree_change_sp; eauto. 
+    unfold rs4. apply agree_nextinstr. eapply agree_change_sp; eauto.
     eapply parent_sp_def; eauto.
   unfold rs5; auto with asmgen.
 
 - (* internal function *)
   exploit functions_translated; eauto. intros [tf [A B]]. monadInv B.
-  generalize EQ; intros EQ'. monadInv EQ'. 
+  generalize EQ; intros EQ'. monadInv EQ'.
   destruct (zlt Int.max_unsigned (list_length_z x0.(fn_code))); inversion EQ1. clear EQ1.
-  unfold store_stack in *. 
-  exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. 
+  unfold store_stack in *.
+  exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl.
   intros [m1' [C D]].
-  exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto. 
+  exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto.
   intros [m2' [F G]].
-  simpl chunk_of_type in F. 
-  exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto. 
+  simpl chunk_of_type in F.
+  exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto.
   intros [m3' [P Q]].
   (* Execution of function prologue *)
   monadInv EQ0. rewrite transl_code'_transl_code in EQ1.
@@ -916,31 +916,31 @@ Local Transparent destroyed_by_jumptable.
             exec_straight tge x
               x.(fn_code) rs0 m'
               x1 rs5 m3').
-  rewrite <- H5 at 2. simpl. 
+  rewrite <- H5 at 2. simpl.
   apply exec_straight_step with rs2 m2'.
   unfold exec_instr. rewrite C. fold sp.
   rewrite <- (sp_val _ _ _ AG). rewrite F. auto. auto.
   apply exec_straight_step with rs3 m2'.
   simpl. auto. auto.
   apply exec_straight_two with rs4 m3'.
-  simpl. unfold store1. rewrite gpr_or_zero_not_zero. 
-  change (rs3 GPR1) with sp. change (rs3 GPR0) with (rs0 LR). simpl. 
+  simpl. unfold store1. rewrite gpr_or_zero_not_zero.
+  change (rs3 GPR1) with sp. change (rs3 GPR0) with (rs0 LR). simpl.
   rewrite Int.add_zero_l. simpl in P. rewrite Int.add_zero_l in P. rewrite ATLR. rewrite P. auto. congruence.
   auto. auto. auto.
   left; exists (State rs5 m3'); split.
-  eapply exec_straight_steps_1; eauto. omega. constructor. 
-  econstructor; eauto. 
+  eapply exec_straight_steps_1; eauto. omega. constructor.
+  econstructor; eauto.
   change (rs5 PC) with (Val.add (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone) Vone).
   rewrite ATPC. simpl. constructor; eauto.
   subst x; simpl in g. unfold fn_code.
-  eapply code_tail_next_int. omega. 
-  eapply code_tail_next_int. omega. 
+  eapply code_tail_next_int. omega.
+  eapply code_tail_next_int. omega.
   eapply code_tail_next_int. omega.
   eapply code_tail_next_int. omega.
   constructor.
   unfold rs5, rs4, rs3, rs2.
-  apply agree_nextinstr. apply agree_nextinstr. 
-  apply agree_set_other; auto. apply agree_set_other; auto. 
+  apply agree_nextinstr. apply agree_nextinstr.
+  apply agree_set_other; auto. apply agree_set_other; auto.
   apply agree_nextinstr. apply agree_set_other; auto.
   eapply agree_change_sp; eauto. unfold sp; congruence.
   congruence.
@@ -948,13 +948,13 @@ Local Transparent destroyed_by_jumptable.
 - (* external function *)
   exploit functions_translated; eauto.
   intros [tf [A B]]. simpl in B. inv B.
-  exploit extcall_arguments_match; eauto. 
+  exploit extcall_arguments_match; eauto.
   intros [args' [C D]].
   exploit external_call_mem_extends'; eauto.
   intros [res' [m2' [P [Q [R S]]]]].
   left; econstructor; split.
-  apply plus_one. eapply exec_step_external; eauto. 
-  eapply external_call_symbols_preserved'; eauto. 
+  apply plus_one. eapply exec_step_external; eauto.
+  eapply external_call_symbols_preserved'; eauto.
   exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
   econstructor; eauto.
   unfold loc_external_result.
@@ -963,7 +963,7 @@ Local Transparent destroyed_by_jumptable.
 - (* return *)
   inv STACKS. simpl in *.
   right. split. omega. split. auto.
-  rewrite <- ATPC in H5. 
+  rewrite <- ATPC in H5.
   econstructor; eauto. congruence.
 Qed.
 
@@ -980,19 +980,19 @@ Proof.
   econstructor; eauto.
   constructor.
   apply Mem.extends_refl.
-  split. auto. simpl. unfold Vzero; congruence. intros. rewrite Regmap.gi. auto. 
-  unfold Genv.symbol_address. 
+  split. auto. simpl. unfold Vzero; congruence. intros. rewrite Regmap.gi. auto.
+  unfold Genv.symbol_address.
   rewrite (transform_partial_program_main _ _ TRANSF).
-  rewrite symbols_preserved. 
+  rewrite symbols_preserved.
   unfold ge; rewrite H1. auto.
 Qed.
 
 Lemma transf_final_states:
-  forall st1 st2 r, 
+  forall st1 st2 r,
   match_states st1 st2 -> Mach.final_state st1 r -> Asm.final_state st2 r.
 Proof.
-  intros. inv H0. inv H. constructor. auto. 
-  compute in H1. inv H1.  
+  intros. inv H0. inv H. constructor. auto.
+  compute in H1. inv H1.
   generalize (preg_val _ _ _ R3 AG). rewrite H2. intros LD; inv LD. auto.
 Qed.
 
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 25e8bf07..aa2645f3 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -35,8 +35,8 @@ Lemma low_high_u:
   forall n, Int.or (Int.shl (high_u n) (Int.repr 16)) (low_u n) = n.
 Proof.
   intros. unfold high_u, low_u.
-  rewrite Int.shl_rolm. rewrite Int.shru_rolm. 
-  rewrite Int.rolm_rolm. 
+  rewrite Int.shl_rolm. rewrite Int.shru_rolm.
+  rewrite Int.rolm_rolm.
   change (Int.modu (Int.add (Int.sub (Int.repr (Z_of_nat Int.wordsize)) (Int.repr 16))
                             (Int.repr 16))
                    (Int.repr (Z_of_nat Int.wordsize)))
@@ -50,8 +50,8 @@ Lemma low_high_u_xor:
   forall n, Int.xor (Int.shl (high_u n) (Int.repr 16)) (low_u n) = n.
 Proof.
   intros. unfold high_u, low_u.
-  rewrite Int.shl_rolm. rewrite Int.shru_rolm. 
-  rewrite Int.rolm_rolm. 
+  rewrite Int.shl_rolm. rewrite Int.shru_rolm.
+  rewrite Int.rolm_rolm.
   change (Int.modu (Int.add (Int.sub (Int.repr (Z_of_nat Int.wordsize)) (Int.repr 16))
                             (Int.repr 16))
                    (Int.repr (Z_of_nat Int.wordsize)))
@@ -65,8 +65,8 @@ Lemma low_high_s:
   forall n, Int.add (Int.shl (high_s n) (Int.repr 16)) (low_s n) = n.
 Proof.
   intros.
-  rewrite Int.shl_mul_two_p. 
-  unfold high_s. 
+  rewrite Int.shl_mul_two_p.
+  unfold high_s.
   rewrite <- (Int.divu_pow2 (Int.sub n (low_s n)) (Int.repr 65536) (Int.repr 16)).
   2: reflexivity.
   change (two_p (Int.unsigned (Int.repr 16))) with 65536.
@@ -78,17 +78,17 @@ Proof.
     unfold Int.modu, Int.zero. decEq.
     change 0 with (0 mod 65536).
     change (Int.unsigned (Int.repr 65536)) with 65536.
-    apply Int.eqmod_mod_eq. omega. 
+    apply Int.eqmod_mod_eq. omega.
     unfold x, low_s. eapply Int.eqmod_trans.
     apply Int.eqmod_divides with Int.modulus.
     unfold Int.sub. apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl.
     exists 65536. compute; auto.
     replace 0 with (Int.unsigned n - Int.unsigned n) by omega.
-    apply Int.eqmod_sub. apply Int.eqmod_refl. apply Int.eqmod_sign_ext'. 
+    apply Int.eqmod_sub. apply Int.eqmod_refl. apply Int.eqmod_sign_ext'.
     compute; auto.
   rewrite H0 in H. rewrite Int.add_zero in H.
   rewrite <- H. unfold x. rewrite Int.sub_add_opp. rewrite Int.add_assoc.
-  rewrite (Int.add_commut (Int.neg (low_s n))). rewrite <- Int.sub_add_opp. 
+  rewrite (Int.add_commut (Int.neg (low_s n))). rewrite <- Int.sub_add_opp.
   rewrite Int.sub_idem. apply Int.add_zero.
 Qed.
 
@@ -96,7 +96,7 @@ Lemma add_zero_symbol_address:
   forall (ge: genv) id ofs,
   Val.add Vzero (Genv.symbol_address ge id ofs) = Genv.symbol_address ge id ofs.
 Proof.
-  unfold Genv.symbol_address; intros. destruct (Genv.find_symbol ge id); auto. 
+  unfold Genv.symbol_address; intros. destruct (Genv.find_symbol ge id); auto.
   simpl. rewrite Int.add_zero; auto.
 Qed.
 
@@ -213,15 +213,15 @@ Proof.
   intros. unfold loadimm.
   case (Int.eq (high_s n) Int.zero).
   (* addi *)
-  econstructor; split. apply exec_straight_one. simpl; eauto. auto. 
+  econstructor; split. apply exec_straight_one. simpl; eauto. auto.
   rewrite Int.add_zero_l. intuition Simpl.
   (* addis *)
   generalize (Int.eq_spec (low_s n) Int.zero); case (Int.eq (low_s n) Int.zero); intro.
-  econstructor; split. apply exec_straight_one. simpl; eauto. auto. 
-  rewrite <- H. rewrite Int.add_commut. rewrite low_high_s. 
+  econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+  rewrite <- H. rewrite Int.add_commut. rewrite low_high_s.
   intuition Simpl.
   (* addis + ori *)
-  econstructor; split. eapply exec_straight_two. 
+  econstructor; split. eapply exec_straight_two.
   simpl; eauto. simpl; eauto. auto. auto.
   split. Simpl. rewrite Int.add_zero_l. unfold Val.or. rewrite low_high_u. auto.
   intros; Simpl.
@@ -241,25 +241,25 @@ Proof.
   intros. unfold addimm.
   (* addi *)
   case (Int.eq (high_s n) Int.zero).
-  econstructor; split. apply exec_straight_one. 
+  econstructor; split. apply exec_straight_one.
   simpl. rewrite gpr_or_zero_not_zero; eauto.
   reflexivity.
   intuition Simpl.
   (* addis *)
   generalize (Int.eq_spec (low_s n) Int.zero); case (Int.eq (low_s n) Int.zero); intro.
   econstructor; split. apply exec_straight_one.
-  simpl. rewrite gpr_or_zero_not_zero; auto. auto. 
-  split. Simpl. 
-  generalize (low_high_s n). rewrite H1. rewrite Int.add_zero. congruence. 
+  simpl. rewrite gpr_or_zero_not_zero; auto. auto.
+  split. Simpl.
+  generalize (low_high_s n). rewrite H1. rewrite Int.add_zero. congruence.
   intros; Simpl.
   (* addis + addi *)
   econstructor; split. eapply exec_straight_two.
-  simpl. rewrite gpr_or_zero_not_zero; eauto. 
   simpl. rewrite gpr_or_zero_not_zero; eauto.
-  auto. auto. 
+  simpl. rewrite gpr_or_zero_not_zero; eauto.
+  auto. auto.
   split. Simpl. rewrite Val.add_assoc. simpl. rewrite low_high_s. auto.
   intros; Simpl.
-Qed. 
+Qed.
 
 (** And integer immediate. *)
 
@@ -290,7 +290,7 @@ Proof.
   generalize (compare_sint_spec (rs#r1 <- v) v Vzero).
   intros [A [B [C D]]].
   split. apply exec_straight_one. simpl.
-  generalize (low_high_u n). rewrite H0. rewrite Int.or_zero. 
+  generalize (low_high_u n). rewrite H0. rewrite Int.or_zero.
   intro. rewrite H1. reflexivity. reflexivity.
   split. rewrite D; auto with asmgen. Simpl.
   split. auto.
@@ -301,10 +301,10 @@ Proof.
   exists (nextinstr (compare_sint (rs1#r1 <- v) v Vzero)).
   generalize (compare_sint_spec (rs1#r1 <- v) v Vzero).
   intros [A [B [C D]]].
-  split. eapply exec_straight_trans. eexact EX1. 
-  apply exec_straight_one. simpl. rewrite RES1. 
+  split. eapply exec_straight_trans. eexact EX1.
+  apply exec_straight_one. simpl. rewrite RES1.
   rewrite (OTHER1 r2). reflexivity. congruence. congruence.
-  reflexivity. 
+  reflexivity.
   split. rewrite D; auto with asmgen. Simpl.
   split. auto.
   intros. rewrite D; auto with asmgen. Simpl.
@@ -321,7 +321,7 @@ Proof.
   intros. unfold andimm. destruct (is_rlw_mask n).
   (* turned into rlw *)
   econstructor; split. eapply exec_straight_one.
-  simpl. rewrite Val.rolm_zero. eauto. auto. 
+  simpl. rewrite Val.rolm_zero. eauto. auto.
   intuition Simpl.
   (* andimm_base *)
   destruct (andimm_base_correct r1 r2 n k rs m) as [rs' [A [B [C D]]]]; auto.
@@ -349,13 +349,13 @@ Proof.
   case (Int.eq (low_u n) Int.zero); intro.
   exists (nextinstr (rs#r1 <- v)).
   split. apply exec_straight_one. simpl.
-  generalize (low_high_u n). rewrite H. rewrite Int.or_zero. 
+  generalize (low_high_u n). rewrite H. rewrite Int.or_zero.
   intro. rewrite H0. reflexivity. reflexivity.
   intuition Simpl.
   (* oris + ori *)
   econstructor; split. eapply exec_straight_two; simpl; reflexivity.
-  intuition Simpl. 
-  rewrite Val.or_assoc. simpl. rewrite low_high_u. reflexivity. 
+  intuition Simpl.
+  rewrite Val.or_assoc. simpl. rewrite low_high_u. reflexivity.
 Qed.
 
 (** Xor integer immediate. *)
@@ -379,13 +379,13 @@ Proof.
   case (Int.eq (low_u n) Int.zero); intro.
   exists (nextinstr (rs#r1 <- v)).
   split. apply exec_straight_one. simpl.
-  generalize (low_high_u n). rewrite H. rewrite Int.or_zero. 
+  generalize (low_high_u n). rewrite H. rewrite Int.or_zero.
   intro. rewrite H0. reflexivity. reflexivity.
   intuition Simpl.
   (* xoris + xori *)
   econstructor; split. eapply exec_straight_two; simpl; reflexivity.
-  intuition Simpl. 
-  rewrite Val.xor_assoc. simpl. rewrite low_high_u_xor. reflexivity. 
+  intuition Simpl.
+  rewrite Val.xor_assoc. simpl. rewrite low_high_u_xor. reflexivity.
 Qed.
 
 (** Rotate and mask. *)
@@ -406,12 +406,12 @@ Proof.
   set (rs1 := nextinstr (rs#r1 <- (Val.rolm rs#r2 amount Int.mone))).
   destruct (andimm_base_correct r1 r1 mask k rs1 m) as [rs' [A [B [C D]]]]; auto.
   exists rs'.
-  split. eapply exec_straight_step; eauto. auto. auto. 
-  split. rewrite B. unfold rs1. rewrite nextinstr_inv; auto with asmgen. 
-  rewrite Pregmap.gss. destruct (rs r2); simpl; auto. 
-  unfold Int.rolm. rewrite Int.and_assoc. 
+  split. eapply exec_straight_step; eauto. auto. auto.
+  split. rewrite B. unfold rs1. rewrite nextinstr_inv; auto with asmgen.
+  rewrite Pregmap.gss. destruct (rs r2); simpl; auto.
+  unfold Int.rolm. rewrite Int.and_assoc.
   decEq; decEq; decEq. rewrite Int.and_commut. apply Int.and_mone.
-  intros. rewrite D; auto. unfold rs1; Simpl. 
+  intros. rewrite D; auto. unfold rs1; Simpl.
 Qed.
 
 (** Indexed memory loads. *)
@@ -433,14 +433,14 @@ Lemma accessind_load_correct:
   /\ forall r, r <> PC -> r <> inj rx -> r <> GPR0 -> rs'#r = rs#r.
 Proof.
   intros. unfold accessind. destruct (Int.eq (high_s ofs) Int.zero).
-- econstructor; split. apply exec_straight_one. 
+- econstructor; split. apply exec_straight_one.
   rewrite H. unfold load1. rewrite gpr_or_zero_not_zero by auto. simpl.
   rewrite H1. eauto. unfold nextinstr. repeat Simplif.
-  split. unfold nextinstr. repeat Simplif. 
-  intros. repeat Simplif. 
+  split. unfold nextinstr. repeat Simplif.
+  intros. repeat Simplif.
 - exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [P [Q R]]].
   econstructor; split. eapply exec_straight_trans. eexact P.
-  apply exec_straight_one. rewrite H0. unfold load2. rewrite Q, R by auto with asmgen. 
+  apply exec_straight_one. rewrite H0. unfold load2. rewrite Q, R by auto with asmgen.
   rewrite H1. reflexivity. unfold nextinstr. repeat Simplif.
   split. repeat Simplif.
   intros. repeat Simplif.
@@ -482,14 +482,14 @@ Lemma accessind_store_correct:
   /\ forall r, r <> PC -> r <> GPR0 -> rs'#r = rs#r.
 Proof.
   intros. unfold accessind. destruct (Int.eq (high_s ofs) Int.zero).
-- econstructor; split. apply exec_straight_one. 
+- econstructor; split. apply exec_straight_one.
   rewrite H. unfold store1. rewrite gpr_or_zero_not_zero by auto. simpl.
   rewrite H1. eauto. unfold nextinstr. repeat Simplif.
-  intros. repeat Simplif. 
+  intros. repeat Simplif.
 - exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [P [Q R]]].
   econstructor; split. eapply exec_straight_trans. eexact P.
   apply exec_straight_one. rewrite H0. unfold store2.
-  rewrite Q. rewrite R by auto with asmgen. rewrite R by auto. 
+  rewrite Q. rewrite R by auto with asmgen. rewrite R by auto.
   rewrite H1. reflexivity. unfold nextinstr. repeat Simplif.
   intros. repeat Simplif.
 Qed.
@@ -519,15 +519,15 @@ Lemma floatcomp_correct:
   forall cmp (r1 r2: freg) k rs m,
   exists rs',
      exec_straight ge fn (floatcomp cmp r1 r2 k) rs m k rs' m
-  /\ rs'#(reg_of_crbit (fst (crbit_for_fcmp cmp))) = 
+  /\ rs'#(reg_of_crbit (fst (crbit_for_fcmp cmp))) =
        (if snd (crbit_for_fcmp cmp)
         then Val.cmpf cmp rs#r1 rs#r2
         else Val.notbool (Val.cmpf cmp rs#r1 rs#r2))
-  /\ forall r', 
+  /\ forall r',
        r' <> PC -> r' <> CR0_0 -> r' <> CR0_1 ->
        r' <> CR0_2 -> r' <> CR0_3 -> rs'#r' = rs#r'.
 Proof.
-  intros. 
+  intros.
   generalize (compare_float_spec rs rs#r1 rs#r2).
   intros [A [B [C D]]].
   set (rs1 := nextinstr (compare_float rs rs#r1 rs#r2)) in *.
@@ -538,25 +538,25 @@ Proof.
   exists rs1.
   split. destruct H0 as [EQ|[EQ|[EQ|EQ]]]; subst cmp;
   apply exec_straight_one; reflexivity.
-  split. 
-  destruct H0 as [EQ|[EQ|[EQ|EQ]]]; subst cmp; simpl; auto. 
+  split.
+  destruct H0 as [EQ|[EQ|[EQ|EQ]]]; subst cmp; simpl; auto.
   rewrite Val.negate_cmpf_eq. auto.
   auto.
   (* two instrs *)
   exists (nextinstr (rs1#CR0_3 <- (Val.cmpf cmp rs#r1 rs#r2))).
   split. elim H0; intro; subst cmp.
   apply exec_straight_two with rs1 m.
-  reflexivity. simpl. 
+  reflexivity. simpl.
   rewrite C; rewrite A. rewrite Val.or_commut. rewrite <- Val.cmpf_le.
   reflexivity. reflexivity. reflexivity.
   apply exec_straight_two with rs1 m.
-  reflexivity. simpl. 
+  reflexivity. simpl.
   rewrite C; rewrite B. rewrite Val.or_commut. rewrite <- Val.cmpf_ge.
   reflexivity. reflexivity. reflexivity.
   split. elim H0; intro; subst cmp; simpl.
   reflexivity.
   reflexivity.
-  intros. Simpl. 
+  intros. Simpl.
 Qed.
 
 (** Translation of conditions. *)
@@ -580,7 +580,7 @@ Lemma transl_cond_correct_1:
   transl_cond cond args k = OK c ->
   exists rs',
      exec_straight ge fn c rs m k rs' m
-  /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = 
+  /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) =
        (if snd (crbit_for_cond cond)
         then Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m)
         else Val.notbool (Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m)))
@@ -594,7 +594,7 @@ Opaque Int.eq.
   destruct (compare_sint_spec rs (rs x) (rs x0)) as [A [B [C D]]].
   econstructor; split.
   apply exec_straight_one. simpl; reflexivity. reflexivity.
-  split. 
+  split.
   case c0; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto.
   auto with asmgen.
   (* Ccompu *)
@@ -602,7 +602,7 @@ Opaque Int.eq.
   destruct (compare_uint_spec rs m (rs x) (rs x0)) as [A [B [C D]]].
   econstructor; split.
   apply exec_straight_one. simpl; reflexivity. reflexivity.
-  split. 
+  split.
   case c0; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto.
   auto with asmgen.
   (* Ccompimm *)
@@ -611,7 +611,7 @@ Opaque Int.eq.
   destruct (compare_sint_spec rs (rs x) (Vint i)) as [A [B [C D]]].
   econstructor; split.
   apply exec_straight_one. simpl; reflexivity. reflexivity.
-  split. 
+  split.
   case c0; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto.
   auto with asmgen.
   destruct (loadimm_correct GPR0 i (Pcmpw x GPR0 :: k) rs m) as [rs1 [EX1 [RES1 OTH1]]].
@@ -620,8 +620,8 @@ Opaque Int.eq.
   exists (nextinstr (compare_sint rs1 (rs1 x) (Vint i))).
   split. eapply exec_straight_trans. eexact EX1.
   apply exec_straight_one. simpl. rewrite RES1; rewrite SAME; auto.
-  reflexivity. 
-  split. rewrite SAME. 
+  reflexivity.
+  split. rewrite SAME.
   case c0; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto.
   intros. rewrite SAME; rewrite D; auto with asmgen.
   (* Ccompuimm *)
@@ -630,7 +630,7 @@ Opaque Int.eq.
   destruct (compare_uint_spec rs m (rs x) (Vint i)) as [A [B [C D]]].
   econstructor; split.
   apply exec_straight_one. simpl; reflexivity. reflexivity.
-  split. 
+  split.
   case c0; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto.
   auto with asmgen.
   destruct (loadimm_correct GPR0 i (Pcmplw x GPR0 :: k) rs m) as [rs1 [EX1 [RES1 OTH1]]].
@@ -639,36 +639,36 @@ Opaque Int.eq.
   exists (nextinstr (compare_uint rs1 m (rs1 x) (Vint i))).
   split. eapply exec_straight_trans. eexact EX1.
   apply exec_straight_one. simpl. rewrite RES1; rewrite SAME; auto.
-  reflexivity. 
-  split. rewrite SAME. 
+  reflexivity.
+  split. rewrite SAME.
   case c0; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto.
   intros. rewrite SAME; rewrite D; auto with asmgen.
   (* Ccompf *)
   fold (Val.cmpf c0 (rs x) (rs x0)).
   destruct (floatcomp_correct c0 x x0 k rs m) as [rs' [EX [RES OTH]]].
-  exists rs'. split. auto. 
-  split. apply RES. 
+  exists rs'. split. auto.
+  split. apply RES.
   auto with asmgen.
   (* Cnotcompf *)
   rewrite Val.notbool_negb_3. rewrite Val.notbool_idem4.
   fold (Val.cmpf c0 (rs x) (rs x0)).
   destruct (floatcomp_correct c0 x x0 k rs m) as [rs' [EX [RES OTH]]].
-  exists rs'. split. auto. 
-  split. rewrite RES. destruct (snd (crbit_for_fcmp c0)); auto. 
+  exists rs'. split. auto.
+  split. rewrite RES. destruct (snd (crbit_for_fcmp c0)); auto.
   auto with asmgen.
   (* Cmaskzero *)
   destruct (andimm_base_correct GPR0 x i k rs m) as [rs' [A [B [C D]]]].
   eauto with asmgen.
-  exists rs'. split. assumption. 
-  split. rewrite C. destruct (rs x); auto. 
+  exists rs'. split. assumption.
+  split. rewrite C. destruct (rs x); auto.
   auto with asmgen.
   (* Cmasknotzero *)
   destruct (andimm_base_correct GPR0 x i k rs m) as [rs' [A [B [C D]]]].
   eauto with asmgen.
-  exists rs'. split. assumption. 
+  exists rs'. split. assumption.
   split. rewrite C. destruct (rs x); auto.
   fold (option_map negb (Some (Int.eq (Int.and i0 i) Int.zero))).
-  rewrite Val.notbool_negb_3. rewrite Val.notbool_idem4. auto. 
+  rewrite Val.notbool_negb_3. rewrite Val.notbool_idem4. auto.
   auto with asmgen.
 Qed.
 
@@ -678,7 +678,7 @@ Lemma transl_cond_correct_2:
   eval_condition cond (map rs (map preg_of args)) m = Some b ->
   exists rs',
      exec_straight ge fn c rs m k rs' m
-  /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = 
+  /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) =
        (if snd (crbit_for_cond cond)
         then Val.of_bool b
         else Val.notbool (Val.of_bool b))
@@ -687,7 +687,7 @@ Proof.
   intros.
   replace (Val.of_bool b)
   with (Val.of_optbool (eval_condition cond rs ## (preg_of ## args) m)).
-  eapply transl_cond_correct_1; eauto. 
+  eapply transl_cond_correct_1; eauto.
   rewrite H0; auto.
 Qed.
 
@@ -699,14 +699,14 @@ Lemma transl_cond_correct_3:
   Mem.extends m m' ->
   exists rs',
      exec_straight ge fn c rs m' k rs' m'
-  /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = 
+  /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) =
        (if snd (crbit_for_cond cond)
         then Val.of_bool b
         else Val.notbool (Val.of_bool b))
   /\ agree ms sp rs'.
 Proof.
   intros.
-  exploit transl_cond_correct_2. eauto. 
+  exploit transl_cond_correct_2. eauto.
     eapply eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto.
   intros [rs' [A [B C]]].
   exists rs'; split. eauto. split. auto. apply agree_exten with rs; auto.
@@ -722,21 +722,21 @@ Remark add_carry_eq0:
 Proof.
   intros. rewrite <- Int.sub_add_l. rewrite Int.add_zero_l.
   rewrite Int.sub_idem. rewrite Int.add_zero_l. fold (Int.not i).
-  predSpec Int.eq Int.eq_spec i Int.zero. 
+  predSpec Int.eq Int.eq_spec i Int.zero.
   subst i. reflexivity.
-  unfold Val.of_bool, Vfalse. decEq. 
+  unfold Val.of_bool, Vfalse. decEq.
   unfold Int.add_carry. rewrite Int.unsigned_zero. rewrite Int.unsigned_one.
   apply zlt_true.
-  generalize (Int.unsigned_range (Int.not i)); intro. 
+  generalize (Int.unsigned_range (Int.not i)); intro.
   assert (Int.unsigned (Int.not i) <> Int.modulus - 1).
     red; intros.
     assert (Int.repr (Int.unsigned (Int.not i)) = Int.mone).
 Local Transparent Int.repr.
-      rewrite H1. apply Int.mkint_eq. reflexivity. 
-   rewrite Int.repr_unsigned in H2. 
+      rewrite H1. apply Int.mkint_eq. reflexivity.
+   rewrite Int.repr_unsigned in H2.
    assert (Int.not (Int.not i) = Int.zero).
    rewrite H2. apply Int.mkint_eq; reflexivity.
-  rewrite Int.not_involutive in H3. 
+  rewrite Int.not_involutive in H3.
   congruence.
   omega.
 Qed.
@@ -749,10 +749,10 @@ Remark add_carry_ne0:
 Proof.
   intros. fold (Int.not (Int.add i Int.mone)). rewrite Int.not_neg.
   rewrite (Int.add_commut  (Int.neg (Int.add i Int.mone))).
-  rewrite <- Int.sub_add_opp. rewrite Int.sub_add_r. rewrite Int.sub_idem. 
+  rewrite <- Int.sub_add_opp. rewrite Int.sub_add_r. rewrite Int.sub_idem.
   rewrite Int.add_zero_l. rewrite Int.add_neg_zero. rewrite Int.add_zero_l.
 Transparent Int.eq.
-  unfold Int.add_carry, Int.eq. 
+  unfold Int.add_carry, Int.eq.
   rewrite Int.unsigned_zero.  rewrite Int.unsigned_mone.
   unfold negb, Val.of_bool, Vtrue, Vfalse.
   destruct (zeq (Int.unsigned i) 0); decEq.
@@ -774,25 +774,25 @@ Proof.
 (* eq 0 *)
   econstructor; split.
   eapply exec_straight_two; simpl; reflexivity.
-  split. Simpl. destruct (rs x0); simpl; auto.  
+  split. Simpl. destruct (rs x0); simpl; auto.
   apply add_carry_eq0.
   intros; Simpl.
 (* ne 0 *)
   econstructor; split.
   eapply exec_straight_two; simpl; reflexivity.
   rewrite gpr_or_zero_not_zero; eauto with asmgen.
-  split. Simpl. destruct (rs x0); simpl; auto.  
+  split. Simpl. destruct (rs x0); simpl; auto.
   apply add_carry_ne0.
   intros; Simpl.
 (* ge 0 *)
   econstructor; split.
   eapply exec_straight_two; simpl; reflexivity.
-  split. Simpl. rewrite Val.rolm_ge_zero. auto.  
+  split. Simpl. rewrite Val.rolm_ge_zero. auto.
   intros; Simpl.
 (* lt 0 *)
   econstructor; split.
   apply exec_straight_one; simpl; reflexivity.
-  split. Simpl. rewrite Val.rolm_lt_zero. auto. 
+  split. Simpl. rewrite Val.rolm_lt_zero. auto.
   intros; Simpl.
 (* default *)
   set (bit := fst (crbit_for_cond c)) in *.
@@ -803,15 +803,15 @@ Proof.
          then k
          else Pxori x x (Cint Int.one) :: k)).
   generalize (transl_cond_correct_1 c rl k1 rs m c0 EQ0).
-  fold bit; fold isset. 
+  fold bit; fold isset.
   intros [rs1 [EX1 [RES1 AG1]]].
   destruct isset.
   (* bit set *)
-  econstructor; split.  eapply exec_straight_trans. eexact EX1. 
+  econstructor; split.  eapply exec_straight_trans. eexact EX1.
   unfold k1. apply exec_straight_one; simpl; reflexivity.
   intuition Simpl.
   (* bit clear *)
-  econstructor; split.  eapply exec_straight_trans. eexact EX1. 
+  econstructor; split.  eapply exec_straight_trans. eexact EX1.
   unfold k1. eapply exec_straight_two; simpl; reflexivity.
   intuition Simpl.
   rewrite RES1. destruct (eval_condition c rs ## (preg_of ## rl) m). destruct b; auto. auto.
@@ -840,8 +840,8 @@ Opaque Int.eq.
   TranslOpSimpl.
   TranslOpSimpl.
   (* Ointconst *)
-  destruct (loadimm_correct x i k rs m) as [rs' [A [B C]]]. 
-  exists rs'. auto with asmgen. 
+  destruct (loadimm_correct x i k rs m) as [rs' [A [B C]]].
+  exists rs'. auto with asmgen.
   (* Oaddrsymbol *)
   set (v' := Genv.symbol_address ge i i0).
   destruct (symbol_is_small_data i i0) eqn:SD; [ | destruct (symbol_is_rel_data i i0) ].
@@ -853,13 +853,13 @@ Opaque Val.add.
   (* relative data *)
   econstructor; split. eapply exec_straight_two; simpl; reflexivity.
   split. Simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen. Simpl.
-  apply low_high_half_zero. 
+  apply low_high_half_zero.
   intros; Simpl.
   (* absolute data *)
   econstructor; split. eapply exec_straight_two; simpl; reflexivity.
   split. Simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. Simpl.
   apply low_high_half_zero.
-  intros; Simpl. 
+  intros; Simpl.
   (* Oaddrstack *)
   destruct (addimm_correct x GPR1 i k rs m) as [rs' [EX [RES OTH]]]; eauto with asmgen.
   exists rs'; auto with asmgen.
@@ -869,21 +869,21 @@ Opaque Val.add.
   (* Oaddsymbol *)
   destruct (symbol_is_small_data i i0) eqn:SD; [ | destruct (symbol_is_rel_data i i0) ].
   (* small data *)
-  econstructor; split. eapply exec_straight_two; simpl; reflexivity. 
+  econstructor; split. eapply exec_straight_two; simpl; reflexivity.
   split. Simpl. rewrite (Val.add_commut (rs x)). f_equal.
   rewrite small_data_area_addressing by auto. apply add_zero_symbol_address.
   intros; Simpl.
   (* relative data *)
-  econstructor; split. eapply exec_straight_trans. 
+  econstructor; split. eapply exec_straight_trans.
   eapply exec_straight_two; simpl; reflexivity.
   eapply exec_straight_two; simpl; reflexivity.
   split. assert (GPR0 <> x0) by (apply sym_not_equal; eauto with asmgen).
   Simpl. rewrite ! gpr_or_zero_zero. rewrite ! gpr_or_zero_not_zero by eauto with asmgen. Simpl.
   rewrite low_high_half_zero. auto.
-  intros; Simpl. 
+  intros; Simpl.
   (* absolute data *)
   econstructor; split. eapply exec_straight_two; simpl; reflexivity.
-  split. Simpl. rewrite ! gpr_or_zero_not_zero by (eauto with asmgen). Simpl. 
+  split. Simpl. rewrite ! gpr_or_zero_not_zero by (eauto with asmgen). Simpl.
   rewrite Val.add_assoc. rewrite (Val.add_commut (rs x)). rewrite low_high_half. auto.
   intros; Simpl.
   (* Osubimm *)
@@ -892,7 +892,7 @@ Opaque Val.add.
   destruct (loadimm_correct GPR0 i (Psubfc x0 x GPR0 :: k) rs m) as [rs1 [EX [RES OTH]]].
   econstructor; split.
   eapply exec_straight_trans. eexact EX. apply exec_straight_one; simpl; reflexivity.
-  split. Simpl. rewrite RES. rewrite OTH; eauto with asmgen. 
+  split. Simpl. rewrite RES. rewrite OTH; eauto with asmgen.
   intros; Simpl.
   (* Omulimm *)
   case (Int.eq (high_s i) Int.zero).
@@ -900,15 +900,15 @@ Opaque Val.add.
   destruct (loadimm_correct GPR0 i (Pmullw x0 x GPR0 :: k) rs m) as [rs1 [EX [RES OTH]]].
   econstructor; split.
   eapply exec_straight_trans. eexact EX. apply exec_straight_one; simpl; reflexivity.
-  split. Simpl. rewrite RES. rewrite OTH; eauto with asmgen. 
+  split. Simpl. rewrite RES. rewrite OTH; eauto with asmgen.
   intros; Simpl.
   (* Odivs *)
   replace v with (Val.maketotal (Val.divs (rs x) (rs x0))).
-  TranslOpSimpl. 
+  TranslOpSimpl.
   rewrite H1; auto.
   (* Odivu *)
   replace v with (Val.maketotal (Val.divu (rs x) (rs x0))).
-  TranslOpSimpl. 
+  TranslOpSimpl.
   rewrite H1; auto.
   (* Oand *)
   set (v' := Val.and (rs x) (rs x0)) in *.
@@ -932,8 +932,8 @@ Opaque Val.add.
   destruct (rs x); simpl; auto. rewrite Int.or_idem. auto.
   (* Oshrximm *)
   econstructor; split.
-  eapply exec_straight_two; simpl; reflexivity. 
-  split. Simpl. apply Val.shrx_carry. auto. 
+  eapply exec_straight_two; simpl; reflexivity.
+  split. Simpl. apply Val.shrx_carry. auto.
   intros; Simpl.
   (* Orolm *)
   destruct (rolm_correct x0 x i i0 k rs m) as [rs' [A [B C]]]; eauto with asmgen.
@@ -969,9 +969,9 @@ Lemma transl_op_correct:
   /\ agree (Regmap.set res v (Mach.undef_regs (destroyed_by_op op) ms)) sp rs'
   /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r.
 Proof.
-  intros. 
-  exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eauto. 
-  intros [v' [A B]].  rewrite (sp_val _ _ _ H0) in A. 
+  intros.
+  exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eauto.
+  intros [v' [A B]].  rewrite (sp_val _ _ _ H0) in A.
   exploit transl_op_correct_aux; eauto. intros [rs' [P [Q R]]].
   rewrite <- Q in B.
   exists rs'; split. eexact P.
@@ -999,7 +999,7 @@ Lemma transl_memory_access_correct:
   exists rs',
       exec_straight ge fn c rs m k rs' m' /\ P rs'.
 Proof.
-  intros until m'; intros TR ADDR TEMP MK1 MK2. 
+  intros until m'; intros TR ADDR TEMP MK1 MK2.
   unfold transl_memory_access in TR; destruct addr; ArgsInv; simpl in ADDR; inv ADDR.
   (* Aindexed *)
   case (Int.eq (high_s i) Int.zero).
@@ -1015,37 +1015,37 @@ Transparent Val.add.
     intros; unfold rs1; Simpl.
   intros [rs' [EX' AG']].
   exists rs'. split. apply exec_straight_step with rs1 m.
-  simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. 
+  simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
   auto. auto.
   (* Aindexed2 *)
   apply MK2; auto.
   (* Aglobal *)
   destruct (symbol_is_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ]; inv TR.
   (* Aglobal from small data *)
-  apply MK1. unfold const_low. rewrite small_data_area_addressing by auto. 
+  apply MK1. unfold const_low. rewrite small_data_area_addressing by auto.
   apply add_zero_symbol_address.
   auto.
   (* Aglobal from relative data *)
   set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))).
   set (rs2 := nextinstr (rs1#temp <- (Genv.symbol_address ge i i0))).
   exploit (MK1 (Cint Int.zero) temp rs2).
-    simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen. 
+    simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen.
     unfold rs2. Simpl. rewrite Val.add_commut. apply add_zero_symbol_address.
-    intros; unfold rs2, rs1; Simpl. 
+    intros; unfold rs2, rs1; Simpl.
   intros [rs' [EX' AG']].
-  exists rs'; split. apply exec_straight_step with rs1 m; auto. 
-  apply exec_straight_step with rs2 m; auto. simpl. unfold rs2. 
+  exists rs'; split. apply exec_straight_step with rs1 m; auto.
+  apply exec_straight_step with rs2 m; auto. simpl. unfold rs2.
   rewrite gpr_or_zero_not_zero by eauto with asmgen. f_equal. f_equal. f_equal.
   unfold rs1; Simpl. apply low_high_half_zero.
   eexact EX'. auto.
   (* Aglobal from absolute data *)
   set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))).
   exploit (MK1 (Csymbol_low i i0) temp rs1).
-    simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen. 
-    unfold rs1. Simpl. apply low_high_half_zero. 
-    intros; unfold rs1; Simpl. 
+    simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen.
+    unfold rs1. Simpl. apply low_high_half_zero.
+    intros; unfold rs1; Simpl.
   intros [rs' [EX' AG']].
-  exists rs'; split. apply exec_straight_step with rs1 m; auto. 
+  exists rs'; split. apply exec_straight_step with rs1 m; auto.
   eexact EX'. auto.
   (* Abased *)
   destruct (symbol_is_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ].
@@ -1055,8 +1055,8 @@ Transparent Val.add.
     unfold rs1; Simpl. apply Val.add_commut.
     intros. unfold rs1; Simpl.
   intros [rs' [EX' AG']].
-  exists rs'; split. apply exec_straight_step with rs1 m. 
-  unfold exec_instr. rewrite gpr_or_zero_zero. f_equal. unfold rs1. f_equal. f_equal. 
+  exists rs'; split. apply exec_straight_step with rs1 m.
+  unfold exec_instr. rewrite gpr_or_zero_zero. f_equal. unfold rs1. f_equal. f_equal.
   unfold const_low. rewrite small_data_area_addressing; auto.
   apply add_zero_symbol_address.
   reflexivity.
@@ -1066,20 +1066,20 @@ Transparent Val.add.
   set (rs2 := nextinstr (rs1#temp <- (Val.add Vzero (high_half ge i i0)))).
   set (rs3 := nextinstr (rs2#temp <- (Genv.symbol_address ge i i0))).
   exploit (MK2 temp GPR0 rs3).
-    f_equal. unfold rs3; Simpl. unfold rs3, rs2, rs1; Simpl. 
+    f_equal. unfold rs3; Simpl. unfold rs3, rs2, rs1; Simpl.
     intros. unfold rs3, rs2, rs1; Simpl.
   intros [rs' [EX' AG']].
-  exists rs'. split. eapply exec_straight_trans with (rs2 := rs3) (m2 := m). 
-  apply exec_straight_three with rs1 m rs2 m; auto. 
-  simpl. unfold rs3. f_equal. f_equal. f_equal. rewrite gpr_or_zero_not_zero by auto. 
-  unfold rs2; Simpl. apply low_high_half_zero. 
-  eexact EX'. auto. 
+  exists rs'. split. eapply exec_straight_trans with (rs2 := rs3) (m2 := m).
+  apply exec_straight_three with rs1 m rs2 m; auto.
+  simpl. unfold rs3. f_equal. f_equal. f_equal. rewrite gpr_or_zero_not_zero by auto.
+  unfold rs2; Simpl. apply low_high_half_zero.
+  eexact EX'. auto.
   (* Abased absolute *)
   set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (high_half ge i i0)))).
   exploit (MK1 (Csymbol_low i i0) temp rs1 k).
     simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen.
-    unfold rs1. Simpl. 
-    rewrite Val.add_assoc. rewrite low_high_half. apply Val.add_commut. 
+    unfold rs1. Simpl.
+    rewrite Val.add_assoc. rewrite low_high_half. apply Val.add_commut.
     intros; unfold rs1; Simpl.
   intros [rs' [EX' AG']].
   exists rs'. split. apply exec_straight_step with rs1 m.
@@ -1087,10 +1087,10 @@ Transparent Val.add.
   assumption. assumption.
   (* Ainstack *)
   destruct (Int.eq (high_s i) Int.zero); inv TR.
-  apply MK1. simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. 
+  apply MK1. simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
   set (rs1 := nextinstr (rs#temp <- (Val.add rs#GPR1 (Vint (Int.shl (high_s i) (Int.repr 16)))))).
   exploit (MK1 (Cint (low_s i)) temp rs1 k).
-    simpl. rewrite gpr_or_zero_not_zero; auto. 
+    simpl. rewrite gpr_or_zero_not_zero; auto.
     unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss.
     rewrite Val.add_assoc. simpl. rewrite low_high_s. auto.
     congruence.
@@ -1129,12 +1129,12 @@ Proof.
   /\ forall r, r <> PC -> r <> GPR12 -> r <> GPR0 -> r <> preg_of dst -> rs' r = rs r).
   {
   intros. eapply transl_memory_access_correct; eauto. congruence.
-  intros. econstructor; split. apply exec_straight_one. 
-  rewrite H4. unfold load1. rewrite H6. rewrite H3. eauto. 
+  intros. econstructor; split. apply exec_straight_one.
+  rewrite H4. unfold load1. rewrite H6. rewrite H3. eauto.
   unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso; auto with asmgen.
   intuition Simpl.
-  intros. econstructor; split. apply exec_straight_one. 
-  rewrite H5. unfold load2. rewrite H6. rewrite H3. eauto. 
+  intros. econstructor; split. apply exec_straight_one.
+  rewrite H5. unfold load2. rewrite H6. rewrite H3. eauto.
   unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso; auto with asmgen.
   intuition Simpl.
   }
@@ -1142,17 +1142,17 @@ Proof.
 - (* Mint8signed *)
   assert (exists v1, Mem.loadv Mint8unsigned m a = Some v1 /\ v = Val.sign_ext 8 v1).
   {
-    destruct a; simpl in *; try discriminate. 
-    rewrite Mem.load_int8_signed_unsigned in H1. 
+    destruct a; simpl in *; try discriminate.
+    rewrite Mem.load_int8_signed_unsigned in H1.
     destruct (Mem.load Mint8unsigned m b (Int.unsigned i)); simpl in H1; inv H1.
     exists v0; auto.
   }
-  destruct H as [v1 [LD SG]]. clear H1. 
+  destruct H as [v1 [LD SG]]. clear H1.
   exploit BASE; eauto; erewrite ireg_of_eq by eauto; auto.
   intros [rs1 [A [B C]]].
-  econstructor; split. 
-  eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto. 
-  split. Simpl. congruence. intros. Simpl. 
+  econstructor; split.
+  eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto.
+  split. Simpl. congruence. intros. Simpl.
 - (* Mint8unsigned *)
   eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto.
 - (* Mint816signed *)
@@ -1185,9 +1185,9 @@ Local Transparent destroyed_by_store.
   assert (TEMP1: int_temp_for src <> GPR0).
     destruct TEMP0; congruence.
   assert (TEMP2: IR (int_temp_for src) <> preg_of src).
-    unfold int_temp_for. destruct (mreg_eq src R12). 
+    unfold int_temp_for. destruct (mreg_eq src R12).
     subst src; simpl; congruence.
-    change (IR GPR12) with (preg_of R12). red; intros; elim n. 
+    change (IR GPR12) with (preg_of R12). red; intros; elim n.
     eapply preg_of_injective; eauto.
   assert (BASE: forall mk1 mk2 chunk',
   transl_memory_access mk1 mk2 addr args (int_temp_for src) k = OK c ->
@@ -1203,12 +1203,12 @@ Local Transparent destroyed_by_store.
   /\ forall r, r <> PC -> r <> GPR0 -> r <> GPR11 /\ r <> GPR12 -> rs' r = rs r).
   {
   intros. eapply transl_memory_access_correct; eauto.
-  intros. econstructor; split. apply exec_straight_one. 
-  rewrite H4. unfold store1. rewrite H6. rewrite H7; auto with asmgen. rewrite H3. eauto. auto. 
-  intros; Simpl. apply H7; auto. destruct TEMP0; destruct H10; congruence. 
-  intros. econstructor; split. apply exec_straight_one. 
-  rewrite H5. unfold store2. rewrite H6. rewrite H7; auto with asmgen. rewrite H3. eauto. auto. 
-  intros; Simpl. apply H7; auto. destruct TEMP0; destruct H10; congruence. 
+  intros. econstructor; split. apply exec_straight_one.
+  rewrite H4. unfold store1. rewrite H6. rewrite H7; auto with asmgen. rewrite H3. eauto. auto.
+  intros; Simpl. apply H7; auto. destruct TEMP0; destruct H10; congruence.
+  intros. econstructor; split. apply exec_straight_one.
+  rewrite H5. unfold store2. rewrite H6. rewrite H7; auto with asmgen. rewrite H3. eauto. auto.
+  intros; Simpl. apply H7; auto. destruct TEMP0; destruct H10; congruence.
   }
   destruct chunk; monadInv H.
 - (* Mint8signed *)
diff --git a/powerpc/CombineOp.v b/powerpc/CombineOp.v
index 6ad6987d..15ddb76f 100644
--- a/powerpc/CombineOp.v
+++ b/powerpc/CombineOp.v
@@ -10,7 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Recognition of combined operations, addressing modes and conditions 
+(** Recognition of combined operations, addressing modes and conditions
   during the [CSE] phase. *)
 
 Require Import Coqlib.
@@ -95,7 +95,7 @@ Function combine_op (op: operation) (args: list valnum) : option(operation * lis
       end
   | Oandimm n, x :: nil =>
       match get x with
-      | Some(Op (Oandimm m) ys) => 
+      | Some(Op (Oandimm m) ys) =>
           Some(let p := Int.and m n in
                if Int.eq p m then (Omove, x :: nil) else (Oandimm p, ys))
       | Some(Op (Orolm amount m) ys) =>
diff --git a/powerpc/CombineOpproof.v b/powerpc/CombineOpproof.v
index 4d8fed78..4883876d 100644
--- a/powerpc/CombineOpproof.v
+++ b/powerpc/CombineOpproof.v
@@ -10,7 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Recognition of combined operations, addressing modes and conditions 
+(** Recognition of combined operations, addressing modes and conditions
   during the [CSE] phase. *)
 
 Require Import Coqlib.
@@ -36,7 +36,7 @@ Hypothesis get_sound: forall v rhs, get v = Some rhs -> rhs_eval_to valu ge sp m
 Lemma get_op_sound:
   forall v op vl, get v = Some (Op op vl) -> eval_operation ge sp op (map valu vl) m = Some (valu v).
 Proof.
-  intros. exploit get_sound; eauto. intros REV; inv REV; auto. 
+  intros. exploit get_sound; eauto. intros REV; inv REV; auto.
 Qed.
 
 Ltac UseGetSound :=
@@ -44,7 +44,7 @@ Ltac UseGetSound :=
   | [ H: get _ = Some _ |- _ ] =>
       let x := fresh "EQ" in (generalize (get_op_sound _ _ _ H); intros x; simpl in x; FuncInv)
   end.
-  
+
 Lemma combine_compimm_ne_0_sound:
   forall x cond args,
   combine_compimm_ne_0 get x = Some(cond, args) ->
@@ -53,11 +53,11 @@ Lemma combine_compimm_ne_0_sound:
 Proof.
   intros until args. functional induction (combine_compimm_ne_0 get x); intros EQ; inv EQ.
   (* of cmp *)
-  UseGetSound. rewrite <- H. 
+  UseGetSound. rewrite <- H.
   destruct (eval_condition cond (map valu args) m); simpl; auto. destruct b; auto.
   (* of and *)
-  UseGetSound. rewrite <- H. 
-  destruct v; simpl; auto. 
+  UseGetSound. rewrite <- H.
+  destruct v; simpl; auto.
 Qed.
 
 Lemma combine_compimm_eq_0_sound:
@@ -69,10 +69,10 @@ Proof.
   intros until args. functional induction (combine_compimm_eq_0 get x); intros EQ; inv EQ.
   (* of cmp *)
   UseGetSound. rewrite <- H.
-  rewrite eval_negate_condition. 
+  rewrite eval_negate_condition.
   destruct (eval_condition c (map valu args) m); simpl; auto. destruct b; auto.
   (* of and *)
-  UseGetSound. rewrite <- H. destruct v; auto. 
+  UseGetSound. rewrite <- H. destruct v; auto.
 Qed.
 
 Lemma combine_compimm_eq_1_sound:
@@ -83,7 +83,7 @@ Lemma combine_compimm_eq_1_sound:
 Proof.
   intros until args. functional induction (combine_compimm_eq_1 get x); intros EQ; inv EQ.
   (* of cmp *)
-  UseGetSound. rewrite <- H. 
+  UseGetSound. rewrite <- H.
   destruct (eval_condition cond (map valu args) m); simpl; auto. destruct b; auto.
 Qed.
 
@@ -95,7 +95,7 @@ Lemma combine_compimm_ne_1_sound:
 Proof.
   intros until args. functional induction (combine_compimm_ne_1 get x); intros EQ; inv EQ.
   (* of cmp *)
-  UseGetSound. rewrite <- H. 
+  UseGetSound. rewrite <- H.
   rewrite eval_negate_condition.
   destruct (eval_condition c (map valu args) m); simpl; auto. destruct b; auto.
 Qed.
@@ -131,7 +131,7 @@ Theorem combine_addr_sound:
 Proof.
   intros. functional inversion H; subst.
   (* indexed - addimm *)
-  UseGetSound. simpl; rewrite <- H0. rewrite Val.add_assoc. auto. 
+  UseGetSound. simpl; rewrite <- H0. rewrite Val.add_assoc. auto.
 Qed.
 
 Theorem combine_op_sound:
@@ -144,27 +144,27 @@ Proof.
   UseGetSound; simpl. rewrite <- H0. rewrite Val.add_assoc. auto.
 (* addimm - subimm *)
 Opaque Val.sub.
-  UseGetSound; simpl. rewrite <- H0. 
+  UseGetSound; simpl. rewrite <- H0.
   change (Vint (Int.add m0 n)) with (Val.add (Vint m0) (Vint n)).
   rewrite Val.sub_add_l. auto.
 (* subimm - addimm *)
-  UseGetSound; simpl. rewrite <- H0. 
+  UseGetSound; simpl. rewrite <- H0.
 Transparent Val.sub.
   destruct v; simpl; auto. repeat rewrite Int.sub_add_opp. rewrite Int.add_assoc.
   rewrite Int.neg_add_distr. decEq. decEq. decEq. apply Int.add_commut.
 (* andimm - andimm *)
-  UseGetSound; simpl. 
-  generalize (Int.eq_spec p m0); rewrite H7; intros. 
+  UseGetSound; simpl.
+  generalize (Int.eq_spec p m0); rewrite H7; intros.
   rewrite <- H0. rewrite Val.and_assoc. simpl. fold p. rewrite H1. auto.
-  UseGetSound; simpl. 
+  UseGetSound; simpl.
   rewrite <- H0. rewrite Val.and_assoc. auto.
 (* andimm - rolm *)
-  UseGetSound; simpl. 
-  generalize (Int.eq_spec p m0); rewrite H7; intros. 
-  rewrite <- H0. destruct v; simpl; auto. unfold Int.rolm. 
+  UseGetSound; simpl.
+  generalize (Int.eq_spec p m0); rewrite H7; intros.
+  rewrite <- H0. destruct v; simpl; auto. unfold Int.rolm.
   rewrite Int.and_assoc. fold p. rewrite H1. auto.
-  UseGetSound; simpl. 
-  rewrite <- H0. destruct v; simpl; auto. unfold Int.rolm. 
+  UseGetSound; simpl.
+  rewrite <- H0. destruct v; simpl; auto. unfold Int.rolm.
   rewrite Int.and_assoc. auto.
 (* orimm *)
   UseGetSound; simpl. rewrite <- H0. rewrite Val.or_assoc. auto.
@@ -172,10 +172,10 @@ Transparent Val.sub.
   UseGetSound; simpl. rewrite <- H0. rewrite Val.xor_assoc. auto.
 (* rolm - andimm *)
   UseGetSound; simpl. rewrite <- H0.
-  rewrite <- Val.rolm_zero. rewrite Val.rolm_rolm. 
+  rewrite <- Val.rolm_zero. rewrite Val.rolm_rolm.
   rewrite (Int.add_commut Int.zero). rewrite Int.add_zero. auto.
 (* rolm - rolm *)
-  UseGetSound; simpl. rewrite <- H0. rewrite Val.rolm_rolm. auto. 
+  UseGetSound; simpl. rewrite <- H0. rewrite Val.rolm_rolm. auto.
 (* cmp *)
   simpl. decEq; decEq. eapply combine_cond_sound; eauto.
 Qed.
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index aac37dc6..eb68f586 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -51,7 +51,7 @@ Lemma match_G:
   forall r id ofs,
   AE.get r ae = Ptr(Gl id ofs) -> Val.lessdef rs#r (Genv.symbol_address ge id ofs).
 Proof.
-  intros. apply vmatch_ptr_gl with bc; auto. rewrite <- H. apply MATCH. 
+  intros. apply vmatch_ptr_gl with bc; auto. rewrite <- H. apply MATCH.
 Qed.
 
 Lemma match_S:
@@ -63,9 +63,9 @@ Qed.
 
 Ltac InvApproxRegs :=
   match goal with
-  | [ H: _ :: _ = _ :: _ |- _ ] => 
+  | [ H: _ :: _ = _ :: _ |- _ ] =>
         injection H; clear H; intros; InvApproxRegs
-  | [ H: ?v = AE.get ?r ae |- _ ] => 
+  | [ H: ?v = AE.get ?r ae |- _ ] =>
         generalize (MATCH r); rewrite <- H; clear H; intro; InvApproxRegs
   | _ => idtac
   end.
@@ -86,11 +86,11 @@ Ltac SimplVM :=
       rewrite E in *; clear H; SimplVM
   | [ H: vmatch _ ?v (Ptr(Gl ?id ?ofs)) |- _ ] =>
       let E := fresh in
-      assert (E: Val.lessdef v (Genv.symbol_address ge id ofs)) by (eapply vmatch_ptr_gl; eauto); 
+      assert (E: Val.lessdef v (Genv.symbol_address ge id ofs)) by (eapply vmatch_ptr_gl; eauto);
       clear H; SimplVM
   | [ H: vmatch _ ?v (Ptr(Stk ?ofs)) |- _ ] =>
       let E := fresh in
-      assert (E: Val.lessdef v (Vptr sp ofs)) by (eapply vmatch_ptr_stk; eauto); 
+      assert (E: Val.lessdef v (Vptr sp ofs)) by (eapply vmatch_ptr_stk; eauto);
       clear H; SimplVM
   | _ => idtac
   end.
@@ -114,20 +114,20 @@ Lemma make_cmp_base_correct:
   forall c args vl,
   vl = map (fun r => AE.get r ae) args ->
   let (op', args') := make_cmp_base c args vl in
-  exists v, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some v 
+  exists v, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some v
          /\ Val.lessdef (Val.of_optbool (eval_condition c rs##args m)) v.
 Proof.
-  intros. unfold make_cmp_base. 
-  generalize (cond_strength_reduction_correct c args vl H). 
+  intros. unfold make_cmp_base.
+  generalize (cond_strength_reduction_correct c args vl H).
   destruct (cond_strength_reduction c args vl) as [c' args']. intros EQ.
-  econstructor; split. simpl; eauto. rewrite EQ. auto. 
+  econstructor; split. simpl; eauto. rewrite EQ. auto.
 Qed.
 
 Lemma make_cmp_correct:
   forall c args vl,
   vl = map (fun r => AE.get r ae) args ->
   let (op', args') := make_cmp c args vl in
-  exists v, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some v 
+  exists v, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some v
          /\ Val.lessdef (Val.of_optbool (eval_condition c rs##args m)) v.
 Proof.
   intros c args vl.
@@ -136,20 +136,20 @@ Proof.
   { intros. apply vmatch_Uns_1 with bc Ptop. eapply vmatch_ge. eapply vincl_ge; eauto. apply MATCH. }
   unfold make_cmp. case (make_cmp_match c args vl); intros.
 - destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
-  simpl in H; inv H. InvBooleans. subst n. 
+  simpl in H; inv H. InvBooleans. subst n.
   exists (rs#r1); split; auto. simpl.
   exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
   destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
-  simpl in H; inv H. InvBooleans. subst n. 
+  simpl in H; inv H. InvBooleans. subst n.
   exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl.
   exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
   apply make_cmp_base_correct; auto.
 - destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
-  simpl in H; inv H. InvBooleans. subst n. 
+  simpl in H; inv H. InvBooleans. subst n.
   exists (rs#r1); split; auto. simpl.
   exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
   destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
-  simpl in H; inv H. InvBooleans. subst n. 
+  simpl in H; inv H. InvBooleans. subst n.
   exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl.
   exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
   apply make_cmp_base_correct; auto.
@@ -162,7 +162,7 @@ Lemma make_addimm_correct:
   exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.add rs#r (Vint n)) v.
 Proof.
   intros. unfold make_addimm.
-  predSpec Int.eq Int.eq_spec n Int.zero; intros. 
+  predSpec Int.eq Int.eq_spec n Int.zero; intros.
   subst. exists (rs#r); split; auto. destruct (rs#r); simpl; auto; rewrite Int.add_zero; auto.
   exists (Val.add rs#r (Vint n)); auto.
 Qed.
@@ -177,7 +177,7 @@ Proof.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
   exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.shl_zero. auto.
   destruct (Int.ltu n Int.iwordsize) eqn:?; intros.
-  rewrite Val.shl_rolm; auto. econstructor; split; eauto. auto. 
+  rewrite Val.shl_rolm; auto. econstructor; split; eauto. auto.
   econstructor; split; eauto. simpl. congruence.
 Qed.
 
@@ -205,7 +205,7 @@ Proof.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
   exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.shru_zero. auto.
   destruct (Int.ltu n Int.iwordsize) eqn:?; intros.
-  rewrite Val.shru_rolm; auto. econstructor; split; eauto. auto. 
+  rewrite Val.shru_rolm; auto. econstructor; split; eauto. auto.
   econstructor; split; eauto. simpl. congruence.
 Qed.
 
@@ -221,10 +221,10 @@ Proof.
   predSpec Int.eq Int.eq_spec n Int.one; intros. subst.
   exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.mul_one; auto.
   destruct (Int.is_power2 n) eqn:?; intros.
-  rewrite (Val.mul_pow2 rs#r1 _ _ Heqo). rewrite Val.shl_rolm. 
-  econstructor; split; eauto. auto. 
+  rewrite (Val.mul_pow2 rs#r1 _ _ Heqo). rewrite Val.shl_rolm.
+  econstructor; split; eauto. auto.
   eapply Int.is_power2_range; eauto.
-  econstructor; split; eauto. auto. 
+  econstructor; split; eauto. auto.
 Qed.
 
 Lemma make_divimm_correct:
@@ -235,9 +235,9 @@ Lemma make_divimm_correct:
   exists w, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_divimm.
-  destruct (Int.is_power2 n) eqn:?. 
+  destruct (Int.is_power2 n) eqn:?.
   destruct (Int.ltu i (Int.repr 31)) eqn:?.
-  exists v; split; auto. simpl. eapply Val.divs_pow2; eauto. congruence. 
+  exists v; split; auto. simpl. eapply Val.divs_pow2; eauto. congruence.
   exists v; auto.
   exists v; auto.
 Qed.
@@ -250,11 +250,11 @@ Lemma make_divuimm_correct:
   exists w, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_divuimm.
-  destruct (Int.is_power2 n) eqn:?. 
+  destruct (Int.is_power2 n) eqn:?.
   econstructor; split. simpl; eauto.
   exploit Int.is_power2_range; eauto. intros RANGE.
-  rewrite <- Val.shru_rolm; auto. rewrite H0 in H. 
-  destruct (rs#r1); simpl in *; inv H. 
+  rewrite <- Val.shru_rolm; auto. rewrite H0 in H.
+  destruct (rs#r1); simpl in *; inv H.
   destruct (Int.eq n Int.zero); inv H2.
   rewrite RANGE. rewrite (Int.divu_pow2 i0 _ _ Heqo). auto.
   exists v; auto.
@@ -273,17 +273,17 @@ Proof.
   subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.and_mone; auto.
   destruct (match x with Uns _ k => Int.eq (Int.zero_ext k (Int.not n)) Int.zero
                        | _ => false end) eqn:UNS.
-  destruct x; try congruence. 
+  destruct x; try congruence.
   exists (rs#r); split; auto.
   inv H; auto. simpl. replace (Int.and i n) with i; auto.
   generalize (Int.eq_spec (Int.zero_ext n0 (Int.not n)) Int.zero); rewrite UNS; intro EQ.
   Int.bit_solve. destruct (zlt i0 n0).
   replace (Int.testbit n i0) with (negb (Int.testbit Int.zero i0)).
-  rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto. 
-  rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto. 
-  rewrite Int.bits_not by auto. apply negb_involutive. 
-  rewrite H6 by auto. auto. 
-  econstructor; split; eauto. auto. 
+  rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto.
+  rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto.
+  rewrite Int.bits_not by auto. apply negb_involutive.
+  rewrite H6 by auto. auto.
+  econstructor; split; eauto. auto.
 Qed.
 
 Lemma make_orimm_correct:
@@ -296,7 +296,7 @@ Proof.
   subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.or_zero; auto.
   predSpec Int.eq Int.eq_spec n Int.mone; intros.
   subst n. exists (Vint Int.mone); split; auto. destruct (rs#r); simpl; auto. rewrite Int.or_mone; auto.
-  econstructor; split; eauto. auto. 
+  econstructor; split; eauto. auto.
 Qed.
 
 Lemma make_xorimm_correct:
@@ -306,10 +306,10 @@ Lemma make_xorimm_correct:
 Proof.
   intros; unfold make_xorimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
-  subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.xor_zero; auto. 
+  subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.xor_zero; auto.
   predSpec Int.eq Int.eq_spec n Int.mone; intros.
-  subst n. exists (Val.notint rs#r); split; auto. 
-  econstructor; split; eauto. auto. 
+  subst n. exists (Val.notint rs#r); split; auto.
+  econstructor; split; eauto. auto.
 Qed.
 
 Lemma make_mulfimm_correct:
@@ -318,11 +318,11 @@ Lemma make_mulfimm_correct:
   let (op, args) := make_mulfimm n r1 r1 r2 in
   exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v.
 Proof.
-  intros; unfold make_mulfimm. 
-  destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros. 
+  intros; unfold make_mulfimm.
+  destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros.
   simpl. econstructor; split. eauto. rewrite H; subst n.
-  destruct (rs#r1); simpl; auto. rewrite Float.mul2_add; auto. 
-  simpl. econstructor; split; eauto. 
+  destruct (rs#r1); simpl; auto. rewrite Float.mul2_add; auto.
+  simpl. econstructor; split; eauto.
 Qed.
 
 Lemma make_mulfimm_correct_2:
@@ -331,12 +331,12 @@ Lemma make_mulfimm_correct_2:
   let (op, args) := make_mulfimm n r2 r1 r2 in
   exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v.
 Proof.
-  intros; unfold make_mulfimm. 
-  destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros. 
+  intros; unfold make_mulfimm.
+  destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros.
   simpl. econstructor; split. eauto. rewrite H; subst n.
-  destruct (rs#r2); simpl; auto. rewrite Float.mul2_add; auto. 
-  rewrite Float.mul_commut; auto. 
-  simpl. econstructor; split; eauto. 
+  destruct (rs#r2); simpl; auto. rewrite Float.mul2_add; auto.
+  rewrite Float.mul_commut; auto.
+  simpl. econstructor; split; eauto.
 Qed.
 
 Lemma make_mulfsimm_correct:
@@ -345,11 +345,11 @@ Lemma make_mulfsimm_correct:
   let (op, args) := make_mulfsimm n r1 r1 r2 in
   exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulfs rs#r1 rs#r2) v.
 Proof.
-  intros; unfold make_mulfsimm. 
-  destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros. 
+  intros; unfold make_mulfsimm.
+  destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros.
   simpl. econstructor; split. eauto. rewrite H; subst n.
-  destruct (rs#r1); simpl; auto. rewrite Float32.mul2_add; auto. 
-  simpl. econstructor; split; eauto. 
+  destruct (rs#r1); simpl; auto. rewrite Float32.mul2_add; auto.
+  simpl. econstructor; split; eauto.
 Qed.
 
 Lemma make_mulfsimm_correct_2:
@@ -358,12 +358,12 @@ Lemma make_mulfsimm_correct_2:
   let (op, args) := make_mulfsimm n r2 r1 r2 in
   exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulfs rs#r1 rs#r2) v.
 Proof.
-  intros; unfold make_mulfsimm. 
-  destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros. 
+  intros; unfold make_mulfsimm.
+  destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros.
   simpl. econstructor; split. eauto. rewrite H; subst n.
-  destruct (rs#r2); simpl; auto. rewrite Float32.mul2_add; auto. 
-  rewrite Float32.mul_commut; auto. 
-  simpl. econstructor; split; eauto. 
+  destruct (rs#r2); simpl; auto. rewrite Float32.mul2_add; auto.
+  rewrite Float32.mul_commut; auto.
+  simpl. econstructor; split; eauto.
 Qed.
 
 Lemma make_cast8signed_correct:
@@ -372,8 +372,8 @@ Lemma make_cast8signed_correct:
   let (op, args) := make_cast8signed r x in
   exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 8 rs#r) v.
 Proof.
-  intros; unfold make_cast8signed. destruct (vincl x (Sgn Ptop 8)) eqn:INCL. 
-  exists rs#r; split; auto. 
+  intros; unfold make_cast8signed. destruct (vincl x (Sgn Ptop 8)) eqn:INCL.
+  exists rs#r; split; auto.
   assert (V: vmatch bc rs#r (Sgn Ptop 8)).
   { eapply vmatch_ge; eauto. apply vincl_ge; auto. }
   inv V; simpl; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto.
@@ -386,8 +386,8 @@ Lemma make_cast16signed_correct:
   let (op, args) := make_cast16signed r x in
   exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 16 rs#r) v.
 Proof.
-  intros; unfold make_cast16signed. destruct (vincl x (Sgn Ptop 16)) eqn:INCL. 
-  exists rs#r; split; auto. 
+  intros; unfold make_cast16signed. destruct (vincl x (Sgn Ptop 16)) eqn:INCL.
+  exists rs#r; split; auto.
   assert (V: vmatch bc rs#r (Sgn Ptop 16)).
   { eapply vmatch_ge; eauto. apply vincl_ge; auto. }
   inv V; simpl; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto.
@@ -413,7 +413,7 @@ Proof.
   InvApproxRegs; SimplVM; inv H0. econstructor; split; eauto. apply Val.add_lessdef; auto.
   InvApproxRegs; SimplVM; inv H0. econstructor; split; eauto. rewrite Val.add_commut. apply Val.add_lessdef; auto.
 (* sub *)
-  InvApproxRegs; SimplVM; inv H0. fold (Val.sub (Vint n1) rs#r2). econstructor; split; eauto. 
+  InvApproxRegs; SimplVM; inv H0. fold (Val.sub (Vint n1) rs#r2). econstructor; split; eauto.
   InvApproxRegs; SimplVM; inv H0. rewrite Val.sub_add_opp. apply make_addimm_correct.
 (* mul *)
   InvApproxRegs; SimplVM; inv H0. fold (Val.mul (Vint n1) rs#r2). rewrite Val.mul_commut. apply make_mulimm_correct; auto.
@@ -464,23 +464,23 @@ Proof.
   intros until res. unfold addr_strength_reduction.
   destruct (addr_strength_reduction_match addr args vl); simpl;
   intros VL EA; InvApproxRegs; SimplVM; try (inv EA).
-- rewrite Genv.shift_symbol_address. econstructor; split; eauto. apply Val.add_lessdef; auto. 
+- rewrite Genv.shift_symbol_address. econstructor; split; eauto. apply Val.add_lessdef; auto.
 - fold (Val.add (Vint n1) rs#r2). rewrite Int.add_commut. rewrite Genv.shift_symbol_address. rewrite Val.add_commut.
   econstructor; split; eauto. apply Val.add_lessdef; auto.
-- rewrite Int.add_zero_l. 
+- rewrite Int.add_zero_l.
   change (Vptr sp (Int.add n1 n2)) with (Val.add (Vptr sp n1) (Vint n2)).
   econstructor; split; eauto. apply Val.add_lessdef; auto.
 - fold (Val.add (Vint n1) rs#r2).  rewrite Int.add_zero_l. rewrite Int.add_commut.
   change (Vptr sp (Int.add n2 n1)) with (Val.add (Vptr sp n2) (Vint n1)).
   rewrite Val.add_commut. econstructor; split; eauto. apply Val.add_lessdef; auto.
-- econstructor; split; eauto. apply Val.add_lessdef; auto. 
-- rewrite Val.add_commut. econstructor; split; eauto. apply Val.add_lessdef; auto. 
+- econstructor; split; eauto. apply Val.add_lessdef; auto.
+- rewrite Val.add_commut. econstructor; split; eauto. apply Val.add_lessdef; auto.
 - fold (Val.add (Vint n1) rs#r2).
   rewrite Val.add_commut. econstructor; split; eauto.
 - econstructor; split; eauto.
-- rewrite Genv.shift_symbol_address. econstructor; split; eauto. 
-- rewrite Genv.shift_symbol_address. econstructor; split; eauto. apply Val.add_lessdef; auto. 
-- rewrite Int.add_zero_l.  
+- rewrite Genv.shift_symbol_address. econstructor; split; eauto.
+- rewrite Genv.shift_symbol_address. econstructor; split; eauto. apply Val.add_lessdef; auto.
+- rewrite Int.add_zero_l.
   change (Vptr sp (Int.add n1 n)) with (Val.add (Vptr sp n1) (Vint n)).
   econstructor; split; eauto. apply Val.add_lessdef; auto.
 - exists res; auto.
diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v
index 7c7177e4..4ee25a32 100644
--- a/powerpc/Conventions1.v
+++ b/powerpc/Conventions1.v
@@ -10,7 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Function calling conventions and other conventions regarding the use of 
+(** Function calling conventions and other conventions regarding the use of
     machine registers and stack slots. *)
 
 Require Import Coqlib.
@@ -58,8 +58,8 @@ Definition index_int_callee_save (r: mreg) :=
   match r with
   | R14 => 17 | R15 => 16 | R16 => 15 | R17 => 14
   | R18 => 13 | R19 => 12 | R20 => 11 | R21 => 10
-  | R22 => 9  | R23 => 8  | R24 => 7  | R25 => 6 
-  | R26 => 5  | R27 => 4  | R28 => 3  | R29 => 2 
+  | R22 => 9  | R23 => 8  | R24 => 7  | R25 => 6
+  | R26 => 5  | R27 => 4  | R28 => 3  | R29 => 2
   | R30 => 1  | R31 => 0  | _ => -1
   end.
 
@@ -67,8 +67,8 @@ Definition index_float_callee_save (r: mreg) :=
   match r with
   | F14 => 17 | F15 => 16 | F16 => 15 | F17 => 14
   | F18 => 13 | F19 => 12 | F20 => 11 | F21 => 10
-  | F22 => 9  | F23 => 8  | F24 => 7  | F25 => 6 
-  | F26 => 5  | F27 => 4  | F28 => 3  | F29 => 2 
+  | F22 => 9  | F23 => 8  | F24 => 7  | F25 => 6
+  | F26 => 5  | F27 => 4  | F28 => 3  | F29 => 2
   | F30 => 1  | F31 => 0  | _ => -1
   end.
 
@@ -123,25 +123,25 @@ Proof.
 Qed.
 
 Lemma index_int_callee_save_inj:
-  forall r1 r2, 
+  forall r1 r2,
   In r1 int_callee_save_regs ->
   In r2 int_callee_save_regs ->
   r1 <> r2 ->
   index_int_callee_save r1 <> index_int_callee_save r2.
 Proof.
-  intros r1 r2. 
+  intros r1 r2.
   simpl; ElimOrEq; ElimOrEq; unfold index_int_callee_save;
   intros; congruence.
 Qed.
 
 Lemma index_float_callee_save_inj:
-  forall r1 r2, 
+  forall r1 r2,
   In r1 float_callee_save_regs ->
   In r2 float_callee_save_regs ->
   r1 <> r2 ->
   index_float_callee_save r1 <> index_float_callee_save r2.
 Proof.
-  intros r1 r2. 
+  intros r1 r2.
   simpl; ElimOrEq; ElimOrEq; unfold index_float_callee_save;
   intros; congruence.
 Qed.
@@ -157,24 +157,24 @@ Proof.
 Qed.
 
 Lemma register_classification:
-  forall r, 
+  forall r,
   In r destroyed_at_call \/ In r int_callee_save_regs \/ In r float_callee_save_regs.
 Proof.
-  destruct r; 
+  destruct r;
   try (left; simpl; OrEq);
   try (right; left; simpl; OrEq);
   try (right; right; simpl; OrEq).
 Qed.
 
 Lemma int_callee_save_not_destroyed:
-  forall r, 
+  forall r,
     In r destroyed_at_call -> In r int_callee_save_regs -> False.
 Proof.
   intros. revert H0 H. simpl. ElimOrEq; NotOrEq.
 Qed.
 
 Lemma float_callee_save_not_destroyed:
-  forall r, 
+  forall r,
     In r destroyed_at_call -> In r float_callee_save_regs -> False.
 Proof.
   intros. revert H0 H. simpl. ElimOrEq; NotOrEq.
@@ -217,9 +217,9 @@ Qed.
 (** The functions in this section determine the locations (machine registers
   and stack slots) used to communicate arguments and results between the
   caller and the callee during function calls.  These locations are functions
-  of the signature of the function and of the call instruction.  
+  of the signature of the function and of the call instruction.
   Agreement between the caller and the callee on the locations to use
-  is guaranteed by our dynamic semantics for Cminor and RTL, which demand 
+  is guaranteed by our dynamic semantics for Cminor and RTL, which demand
   that the signature of the call instruction is identical to that of the
   called function.
 
@@ -257,7 +257,7 @@ Qed.
 (** The result locations are caller-save registers *)
 
 Lemma loc_result_caller_save:
-  forall (s: signature) (r: mreg), 
+  forall (s: signature) (r: mreg),
   In r (loc_result s) -> In r destroyed_at_call.
 Proof.
   intros.
@@ -354,7 +354,7 @@ Definition tailcall_possible (s: signature) : Prop :=
   forall l, In l (loc_arguments s) ->
   match l with R _ => True | S _ _ _ => False end.
 
-(** Argument locations are either caller-save registers or [Outgoing] 
+(** Argument locations are either caller-save registers or [Outgoing]
   stack slots at nonnegative offsets. *)
 
 Definition loc_argument_acceptable (l: loc) : Prop :=
@@ -384,12 +384,12 @@ Opaque list_nth_z.
   subst. split. omega. congruence.
   exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega.
 - (* float *)
-  destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H. 
+  destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H.
   subst. right. eapply list_nth_z_in; eauto.
   eapply IHtyl; eauto.
   subst. split. apply Zle_ge. apply align_le. omega. congruence.
   exploit IHtyl; eauto. destruct l; auto. destruct sl; auto.
-  assert (ofs <= align ofs 2) by (apply align_le; omega). 
+  assert (ofs <= align ofs 2) by (apply align_le; omega).
   intuition omega.
 - (* long *)
   set (ir' := align ir 2) in *.
@@ -398,21 +398,21 @@ Opaque list_nth_z.
   destruct H. subst; left; eapply list_nth_z_in; eauto.
   destruct H. subst; left; eapply list_nth_z_in; eauto.
   eapply IHtyl; eauto.
-  assert (ofs <= align ofs 2) by (apply align_le; omega). 
+  assert (ofs <= align ofs 2) by (apply align_le; omega).
   destruct H. subst. split. omega. congruence.
   destruct H. subst. split. omega. congruence.
   exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega.
-  assert (ofs <= align ofs 2) by (apply align_le; omega). 
+  assert (ofs <= align ofs 2) by (apply align_le; omega).
   destruct H. subst. split. omega. congruence.
   destruct H. subst. split. omega. congruence.
-  exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega. 
+  exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega.
 - (* single *)
-  destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H. 
+  destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H.
   subst. right. eapply list_nth_z_in; eauto.
   eapply IHtyl; eauto.
   subst. split. apply Zle_ge. apply align_le. omega. congruence.
   exploit IHtyl; eauto. destruct l; auto. destruct sl; auto.
-  assert (ofs <= align ofs 2) by (apply align_le; omega). 
+  assert (ofs <= align ofs 2) by (apply align_le; omega).
   intuition omega.
 - (* any32 *)
   destruct (list_nth_z int_param_regs ir) as [r|] eqn:E; destruct H.
@@ -421,12 +421,12 @@ Opaque list_nth_z.
   subst. split. omega. congruence.
   exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega.
 - (* any64 *)
-  destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H. 
+  destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H.
   subst. right. eapply list_nth_z_in; eauto.
   eapply IHtyl; eauto.
   subst. split. apply Zle_ge. apply align_le. omega. congruence.
   exploit IHtyl; eauto. destruct l; auto. destruct sl; auto.
-  assert (ofs <= align ofs 2) by (apply align_le; omega). 
+  assert (ofs <= align ofs 2) by (apply align_le; omega).
   intuition omega.
 Qed.
 
@@ -439,7 +439,7 @@ Proof.
   destruct l.
   intro H0; elim H0; simpl; ElimOrEq; OrEq.
   destruct sl; try contradiction. simpl. intuition omega.
-Qed. 
+Qed.
 Hint Resolve loc_arguments_acceptable: locs.
 
 (** The offsets of [Outgoing] arguments are below [size_arguments s]. *)
@@ -474,7 +474,7 @@ Qed.
 Lemma size_arguments_above:
   forall s, size_arguments s >= 0.
 Proof.
-  intros; unfold size_arguments. apply Zle_ge.  
+  intros; unfold size_arguments. apply Zle_ge.
   apply size_arguments_rec_above.
 Qed.
 
@@ -492,48 +492,48 @@ Proof.
   elim H0.
   destruct a.
 - (* int *)
-  destruct (list_nth_z int_param_regs ir); destruct H0. 
+  destruct (list_nth_z int_param_regs ir); destruct H0.
   congruence.
   eauto.
   inv H0. apply size_arguments_rec_above.
   eauto.
 - (* float *)
-  destruct (list_nth_z float_param_regs fr); destruct H0. 
+  destruct (list_nth_z float_param_regs fr); destruct H0.
   congruence.
   eauto.
-  inv H0. apply size_arguments_rec_above. eauto. 
+  inv H0. apply size_arguments_rec_above. eauto.
 - (* long *)
   set (ir' := align ir 2) in *.
   destruct (list_nth_z int_param_regs ir').
   destruct (list_nth_z int_param_regs (ir' + 1)).
   destruct H0. congruence. destruct H0. congruence. eauto.
-  destruct H0. inv H0. 
+  destruct H0. inv H0.
   transitivity (align ofs0 2 + 2). simpl; omega. eauto.  apply size_arguments_rec_above.
   destruct H0. inv H0.
   transitivity (align ofs0 2 + 2). simpl; omega. eauto.  apply size_arguments_rec_above.
-  eauto. 
-  destruct H0. inv H0. 
+  eauto.
+  destruct H0. inv H0.
   transitivity (align ofs0 2 + 2). simpl; omega. eauto.  apply size_arguments_rec_above.
   destruct H0. inv H0.
   transitivity (align ofs0 2 + 2). simpl; omega. eauto.  apply size_arguments_rec_above.
   eauto.
 - (* single *)
-  destruct (list_nth_z float_param_regs fr); destruct H0. 
+  destruct (list_nth_z float_param_regs fr); destruct H0.
   congruence.
   eauto.
   inv H0. transitivity (align ofs0 2 + 2). simpl; omega. apply size_arguments_rec_above.
   eauto.
 - (* any32 *)
-  destruct (list_nth_z int_param_regs ir); destruct H0. 
+  destruct (list_nth_z int_param_regs ir); destruct H0.
   congruence.
   eauto.
   inv H0. apply size_arguments_rec_above.
   eauto.
 - (* any64 *)
-  destruct (list_nth_z float_param_regs fr); destruct H0. 
+  destruct (list_nth_z float_param_regs fr); destruct H0.
   congruence.
   eauto.
-  inv H0. apply size_arguments_rec_above. eauto. 
+  inv H0. apply size_arguments_rec_above. eauto.
   }
   eauto.
 Qed.
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index 20bec532..8d3976f4 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -21,7 +21,7 @@ Require Import Op.
 (** The following type defines the machine registers that can be referenced
   as locations.  These include:
 - Integer registers that can be allocated to RTL pseudo-registers ([Rxx]).
-- Floating-point registers that can be allocated to RTL pseudo-registers 
+- Floating-point registers that can be allocated to RTL pseudo-registers
   ([Fxx]).
 
   The type [mreg] does not include special-purpose or reserved
diff --git a/powerpc/NeedOp.v b/powerpc/NeedOp.v
index 71c16ab9..4d8c32bd 100644
--- a/powerpc/NeedOp.v
+++ b/powerpc/NeedOp.v
@@ -101,7 +101,7 @@ Proof.
   intros. destruct cond; simpl in H;
   try (eapply default_needs_of_condition_sound; eauto; fail);
   simpl in *; FuncInv; InvAgree.
-- eapply maskzero_sound; eauto. 
+- eapply maskzero_sound; eauto.
 - destruct (Val.maskzero_bool v i) as [b'|] eqn:MZ; try discriminate.
   erewrite maskzero_sound; eauto.
 Qed.
@@ -117,7 +117,7 @@ Lemma needs_of_operation_sound:
 Proof.
   unfold needs_of_operation; intros; destruct op; try (eapply default_needs_of_operation_sound; eauto; fail);
   simpl in *; FuncInv; InvAgree; TrivialExists.
-- apply sign_ext_sound; auto. compute; auto. 
+- apply sign_ext_sound; auto. compute; auto.
 - apply sign_ext_sound; auto. compute; auto.
 - apply add_sound; auto.
 - apply add_sound; auto with na.
@@ -137,8 +137,8 @@ Proof.
 - apply and_sound; auto. apply notint_sound; rewrite bitwise_idem; auto.
 - apply or_sound; auto. apply notint_sound; rewrite bitwise_idem; auto.
 - apply shrimm_sound; auto.
-- apply rolm_sound; auto. 
-- destruct (eval_condition c args m) as [b|] eqn:EC; simpl in H2. 
+- apply rolm_sound; auto.
+- destruct (eval_condition c args m) as [b|] eqn:EC; simpl in H2.
   erewrite needs_of_condition_sound by eauto.
   subst v; simpl. auto with na.
   subst v; auto with na.
@@ -154,7 +154,7 @@ Proof.
   intros. destruct op; simpl in *; try discriminate; inv H1; FuncInv; subst.
 - apply sign_ext_redundant_sound; auto. omega.
 - apply sign_ext_redundant_sound; auto. omega.
-- apply andimm_redundant_sound; auto. 
+- apply andimm_redundant_sound; auto.
 - apply orimm_redundant_sound; auto.
 - apply rolm_redundant_sound; auto.
 Qed.
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 6866b086..c8028557 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -17,7 +17,7 @@
 - [operation]: arithmetic and logical operations;
 - [addressing]: addressing modes for load and store operations.
 
-  These types are PowerPC-specific and correspond roughly to what the 
+  These types are PowerPC-specific and correspond roughly to what the
   processor can compute in one instruction.  In other terms, these
   types reflect the state of the program after instruction selection.
   For a processor-independent set of operations, see the abstract
@@ -118,7 +118,7 @@ Inductive operation : Type :=
 (*c Boolean tests: *)
   | Ocmp: condition -> operation.       (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
 
-(** Addressing modes.  [r1], [r2], etc, are the arguments to the 
+(** Addressing modes.  [r1], [r2], etc, are the arguments to the
   addressing. *)
 
 Inductive addressing: Type :=
@@ -184,7 +184,7 @@ Definition eval_operation
   | Ointconst n, nil => Some (Vint n)
   | Ofloatconst n, nil => Some (Vfloat n)
   | Osingleconst n, nil => Some (Vsingle n)
-  | Oaddrsymbol s ofs, nil => Some (Genv.symbol_address genv s ofs) 
+  | Oaddrsymbol s ofs, nil => Some (Genv.symbol_address genv s ofs)
   | Oaddrstack ofs, nil => Some (Val.add sp (Vint ofs))
   | Ocast8signed, v1::nil => Some (Val.sign_ext 8 v1)
   | Ocast16signed, v1::nil => Some (Val.sign_ext 16 v1)
@@ -436,7 +436,7 @@ Proof with (try exact I).
   destruct v0; destruct v1...
   destruct v0...
   destruct v0...
-  destruct (eval_condition c vl m); simpl... destruct b... 
+  destruct (eval_condition c vl m); simpl... destruct b...
 Qed.
 
 End SOUNDNESS.
@@ -460,7 +460,7 @@ Proof.
   intros until a. unfold is_move_operation; destruct op;
   try (intros; discriminate).
   destruct args. intros; discriminate.
-  destruct args. intros. intuition congruence. 
+  destruct args. intros. intuition congruence.
   intros; discriminate.
 Qed.
 
@@ -488,9 +488,9 @@ Proof.
   repeat (destruct vl; auto). apply Val.negate_cmpu_bool.
   repeat (destruct vl; auto). apply Val.negate_cmp_bool.
   repeat (destruct vl; auto). apply Val.negate_cmpu_bool.
-  repeat (destruct vl; auto). 
+  repeat (destruct vl; auto).
   repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0); auto. destruct b; auto.
-  repeat (destruct vl; auto). 
+  repeat (destruct vl; auto).
   repeat (destruct vl; auto). destruct (Val.maskzero_bool v i) as [[]|]; auto.
 Qed.
 
@@ -511,7 +511,7 @@ Definition shift_stack_operation (delta: int) (op: operation) :=
 Lemma type_shift_stack_addressing:
   forall delta addr, type_of_addressing (shift_stack_addressing delta addr) = type_of_addressing addr.
 Proof.
-  intros. destruct addr; auto. 
+  intros. destruct addr; auto.
 Qed.
 
 Lemma type_shift_stack_operation:
@@ -559,10 +559,10 @@ Lemma eval_offset_addressing:
 Proof.
   intros. destruct addr; simpl in H; inv H; simpl in *; FuncInv; subst.
   rewrite Val.add_assoc; auto.
-  unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto. 
   unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto.
-  rewrite Val.add_assoc. rewrite Val.add_permut. rewrite Val.add_commut. auto. 
-  rewrite Val.add_assoc. auto. 
+  unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto.
+  rewrite Val.add_assoc. rewrite Val.add_permut. rewrite Val.add_commut. auto.
+  rewrite Val.add_assoc. auto.
 Qed.
 
 (** Operations that are so cheap to recompute that CSE should not factor them out. *)
@@ -591,7 +591,7 @@ Lemma op_depends_on_memory_correct:
   eval_operation ge sp op args m1 = eval_operation ge sp op args m2.
 Proof.
   intros until m2. destruct op; simpl; try congruence. unfold eval_condition.
-  destruct c; simpl; auto; try discriminate. 
+  destruct c; simpl; auto; try discriminate.
 Qed.
 
 (** Global variables mentioned in an operation or addressing mode *)
@@ -630,7 +630,7 @@ Remark symbol_address_preserved:
 Proof.
   unfold Genv.symbol_address; intros. rewrite agree_on_symbols; auto.
 Qed.
- 
+
 Lemma eval_operation_preserved:
   forall sp op vl m,
   eval_operation ge2 sp op vl m = eval_operation ge1 sp op vl m.
@@ -740,25 +740,25 @@ Lemma eval_operation_inj:
 Proof.
   intros until v1; intros GL; intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
   apply GL; simpl; auto.
-  apply Values.Val.add_inject; auto. 
+  apply Values.Val.add_inject; auto.
   inv H4; simpl; auto.
   inv H4; simpl; auto.
   apply Values.Val.add_inject; auto.
   apply Values.Val.add_inject; auto.
   apply Values.Val.add_inject; auto. apply GL; simpl; auto.
-  inv H4; inv H2; simpl; auto. econstructor; eauto. 
+  inv H4; inv H2; simpl; auto. econstructor; eauto.
     rewrite Int.sub_add_l. auto.
-    destruct (eq_block b1 b0); auto. subst. rewrite H1 in H0. inv H0. rewrite dec_eq_true. 
+    destruct (eq_block b1 b0); auto. subst. rewrite H1 in H0. inv H0. rewrite dec_eq_true.
     rewrite Int.sub_shifted. auto.
-  inv H4; auto. 
+  inv H4; auto.
   inv H4; inv H2; simpl; auto.
   inv H4; simpl; auto.
   inv H4; inv H2; simpl; auto.
   inv H4; inv H2; simpl; auto.
-  inv H4; inv H3; simpl in H1; inv H1. simpl. 
+  inv H4; inv H3; simpl in H1; inv H1. simpl.
     destruct (Int.eq i0 Int.zero
          || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2. TrivialExists.
-  inv H4; inv H3; simpl in H1; inv H1. simpl. 
+  inv H4; inv H3; simpl in H1; inv H1. simpl.
     destruct (Int.eq i0 Int.zero); inv H2. TrivialExists.
   inv H4; inv H2; simpl; auto.
   inv H4; simpl; auto.
@@ -841,7 +841,7 @@ Remark valid_pointer_extends:
   Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
   Mem.valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
 Proof.
-  intros. inv H0. rewrite Int.add_zero. eapply Mem.valid_pointer_extends; eauto. 
+  intros. inv H0. rewrite Int.add_zero. eapply Mem.valid_pointer_extends; eauto.
 Qed.
 
 Remark weak_valid_pointer_extends:
@@ -909,8 +909,8 @@ Proof.
   apply valid_different_pointers_extends; auto.
   intros. rewrite <- val_inject_lessdef; auto.
   rewrite <- val_inject_lessdef; auto.
-  eauto. auto. 
-  destruct H2 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. 
+  eauto. auto.
+  destruct H2 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto.
 Qed.
 
 Lemma eval_addressing_lessdef:
@@ -926,8 +926,8 @@ Proof.
   eapply eval_addressing_inj with (sp1 := sp).
   intros. rewrite <- val_inject_lessdef; auto.
   rewrite <- val_inject_lessdef; auto.
-  eauto. auto. 
-  destruct H1 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. 
+  eauto. auto.
+  destruct H1 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto.
 Qed.
 
 End EVAL_LESSDEF.
@@ -949,7 +949,7 @@ Remark symbol_address_inject:
   forall id ofs, Val.inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs).
 Proof.
   intros. unfold Genv.symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto.
-  exploit (proj1 globals); eauto. intros. 
+  exploit (proj1 globals); eauto. intros.
   econstructor; eauto. rewrite Int.add_zero; auto.
 Qed.
 
@@ -971,11 +971,11 @@ Lemma eval_addressing_inject:
   forall addr vl1 vl2 v1,
   Val.inject_list f vl1 vl2 ->
   eval_addressing genv (Vptr sp1 Int.zero) addr vl1 = Some v1 ->
-  exists v2, 
+  exists v2,
      eval_addressing genv (Vptr sp2 Int.zero) (shift_stack_addressing (Int.repr delta) addr) vl2 = Some v2
   /\ Val.inject f v1 v2.
 Proof.
-  intros. 
+  intros.
   rewrite eval_shift_stack_addressing. simpl.
   eapply eval_addressing_inj with (sp1 := Vptr sp1 Int.zero); eauto.
   intros. apply symbol_address_inject.
@@ -990,7 +990,7 @@ Lemma eval_operation_inject:
      eval_operation genv (Vptr sp2 Int.zero) (shift_stack_operation (Int.repr delta) op) vl2 m2 = Some v2
   /\ Val.inject f v1 v2.
 Proof.
-  intros. 
+  intros.
   rewrite eval_shift_stack_operation. simpl.
   eapply eval_operation_inj with (sp1 := Vptr sp1 Int.zero) (m1 := m1); eauto.
   intros; eapply Mem.valid_pointer_inject_val; eauto.
@@ -1015,7 +1015,7 @@ End EVAL_INJECT.
               / \        / \        / \
               \ /        \ /        \ /
         -0--> [1] --1--> [2] --0--> [3]
-       /     
+       /
      [0]
        \
         -1--> [4] --0--> [5] --1--> [6]
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index ad1adc47..f93b93e5 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -32,7 +32,7 @@ Open Local Scope cminorsel_scope.
 
 (** The following are trivial lemmas and custom tactics that help
   perform backward (inversion) and forward reasoning over the evaluation
-  of operator applications. *)  
+  of operator applications. *)
 
 Ltac EvalOp := eapply eval_Eop; eauto with evalexpr.
 
@@ -117,8 +117,8 @@ Theorem eval_addrsymbol:
   forall le id ofs,
   exists v, eval_expr ge sp e m le (addrsymbol id ofs) v /\ Val.lessdef (Genv.symbol_address ge id ofs) v.
 Proof.
-  intros. unfold addrsymbol. econstructor; split. 
-  EvalOp. simpl; eauto. 
+  intros. unfold addrsymbol. econstructor; split.
+  EvalOp. simpl; eauto.
   auto.
 Qed.
 
@@ -127,7 +127,7 @@ Theorem eval_addrstack:
   exists v, eval_expr ge sp e m le (addrstack ofs) v /\ Val.lessdef (Val.add sp (Vint ofs)) v.
 Proof.
   intros. unfold addrstack. econstructor; split.
-  EvalOp. simpl; eauto. 
+  EvalOp. simpl; eauto.
   auto.
 Qed.
 
@@ -138,20 +138,20 @@ Proof.
   unfold notint; red; intros until x; case (notint_match a); intros; InvEval.
   TrivialExists.
   subst. exists v1; split; auto.
-  subst. TrivialExists. 
+  subst. TrivialExists.
   subst. TrivialExists.
   subst. TrivialExists.
   subst. exists (Val.and v1 v0); split; auto. EvalOp.
   subst. exists (Val.or v1 v0); split; auto. EvalOp.
   subst. exists (Val.xor v1 v0); split; auto. EvalOp.
-  subst. exists (Val.or v0 (Val.notint v1)); split. EvalOp. 
+  subst. exists (Val.or v0 (Val.notint v1)); split. EvalOp.
     destruct v0; destruct v1; simpl; auto. rewrite Int.not_and_or_not. rewrite Int.not_involutive.
     rewrite Int.or_commut. auto.
-  subst. exists (Val.and v0 (Val.notint v1)); split. EvalOp. 
+  subst. exists (Val.and v0 (Val.notint v1)); split. EvalOp.
     destruct v0; destruct v1; simpl; auto. rewrite Int.not_or_and_not. rewrite Int.not_involutive.
     rewrite Int.and_commut. auto.
   subst x. TrivialExists. simpl. rewrite Val.not_xor. rewrite Val.xor_assoc. auto.
-  TrivialExists. 
+  TrivialExists.
 Qed.
 
 Theorem eval_addimm:
@@ -159,7 +159,7 @@ Theorem eval_addimm:
 Proof.
   red; unfold addimm; intros until x.
   predSpec Int.eq Int.eq_spec n Int.zero.
-  subst n. intros. exists x; split; auto. 
+  subst n. intros. exists x; split; auto.
   destruct x; simpl; auto. rewrite Int.add_zero. auto. rewrite Int.add_zero. auto.
   case (addimm_match a); intros; InvEval; simpl; TrivialExists; simpl.
   rewrite Int.add_commut. auto.
@@ -167,15 +167,15 @@ Proof.
   rewrite Val.add_assoc. rewrite Int.add_commut. auto.
   subst. rewrite Val.add_assoc. rewrite Int.add_commut. auto.
   subst. rewrite Int.add_commut. rewrite Genv.shift_symbol_address. rewrite ! Val.add_assoc. f_equal. f_equal. apply Val.add_commut.
-Qed. 
+Qed.
 
 Theorem eval_addsymbol:
   forall s ofs, unary_constructor_sound (addsymbol s ofs) (Val.add (Genv.symbol_address ge s ofs)).
 Proof.
   red; unfold addsymbol; intros until x.
   case (addsymbol_match a); intros; InvEval; simpl; TrivialExists; simpl.
-  rewrite Genv.shift_symbol_address. auto. 
-  rewrite Genv.shift_symbol_address. subst x. rewrite Val.add_assoc. f_equal. f_equal. 
+  rewrite Genv.shift_symbol_address. auto.
+  rewrite Genv.shift_symbol_address. subst x. rewrite Val.add_assoc. f_equal. f_equal.
   apply Val.add_commut.
 Qed.
 
@@ -187,36 +187,36 @@ Proof.
 - apply eval_addimm; auto.
 - apply eval_addsymbol; auto.
 - rewrite Val.add_commut. apply eval_addsymbol; auto.
-- subst. 
+- subst.
   replace (Val.add (Val.add v1 (Vint n1)) (Val.add v0 (Vint n2)))
      with (Val.add (Val.add v1 v0) (Val.add (Vint n1) (Vint n2))).
   apply eval_addimm. EvalOp.
   repeat rewrite Val.add_assoc. decEq. apply Val.add_permut.
-- subst. 
+- subst.
   replace (Val.add (Val.add v1 (Vint n1)) y)
      with (Val.add (Val.add v1 y) (Vint n1)).
   apply eval_addimm. EvalOp.
   repeat rewrite Val.add_assoc. decEq. apply Val.add_commut.
-- subst. TrivialExists. 
+- subst. TrivialExists.
     econstructor. EvalOp. simpl. reflexivity. econstructor. eauto. constructor.
     simpl. repeat rewrite Val.add_assoc. decEq; decEq.
     rewrite Val.add_commut. rewrite Val.add_permut. auto.
 - replace (Val.add x y) with
     (Val.add (Genv.symbol_address ge s (Int.add ofs n)) (Val.add v1 v0)).
-  apply eval_addsymbol; auto. EvalOp. 
-  subst. rewrite Genv.shift_symbol_address. rewrite ! Val.add_assoc. f_equal. 
+  apply eval_addsymbol; auto. EvalOp.
+  subst. rewrite Genv.shift_symbol_address. rewrite ! Val.add_assoc. f_equal.
   rewrite Val.add_permut. f_equal. apply Val.add_commut.
-- subst. rewrite Val.add_assoc. apply eval_addsymbol. EvalOp. 
+- subst. rewrite Val.add_assoc. apply eval_addsymbol. EvalOp.
 - subst. rewrite <- Val.add_assoc. apply eval_addimm. EvalOp.
-- subst. rewrite Val.add_permut. apply eval_addsymbol. EvalOp. 
-- TrivialExists. 
+- subst. rewrite Val.add_permut. apply eval_addsymbol. EvalOp.
+- TrivialExists.
 Qed.
 
 Theorem eval_subimm:
   forall n, unary_constructor_sound (subimm n) (fun v => Val.sub (Vint n) v).
 Proof.
   intros; red; intros until x. unfold subimm. destruct (subimm_match a); intros.
-  InvEval. TrivialExists. 
+  InvEval. TrivialExists.
   InvEval. subst x. TrivialExists. unfold eval_operation. destruct v1; simpl; auto.
   rewrite ! Int.sub_add_opp. rewrite Int.add_assoc. f_equal. f_equal. f_equal.
   rewrite Int.neg_add_distr.  apply Int.add_commut.
@@ -229,7 +229,7 @@ Proof.
   unfold sub; case (sub_match a b); intros; InvEval.
   rewrite Val.sub_add_opp. apply eval_addimm; auto.
   apply eval_subimm; auto.
-  subst. rewrite Val.sub_add_l. rewrite Val.sub_add_r. 
+  subst. rewrite Val.sub_add_l. rewrite Val.sub_add_r.
     rewrite Val.add_assoc. simpl. rewrite Int.add_commut. rewrite <- Int.sub_add_opp.
     apply eval_addimm; EvalOp.
   subst. rewrite Val.sub_add_l. apply eval_addimm; EvalOp.
@@ -239,7 +239,7 @@ Qed.
 
 Theorem eval_negint: unary_constructor_sound negint (fun v => Val.sub Vzero v).
 Proof.
-  red; intros. unfold negint. apply eval_subimm; auto. 
+  red; intros. unfold negint. apply eval_subimm; auto.
 Qed.
 
 Lemma eval_rolm:
@@ -248,7 +248,7 @@ Lemma eval_rolm:
                           (fun x => Val.rolm x amount mask).
 Proof.
   red; intros until x. unfold rolm; case (rolm_match a); intros; InvEval.
-  TrivialExists. 
+  TrivialExists.
   subst. rewrite Val.rolm_rolm. TrivialExists.
   subst. rewrite <- Val.rolm_zero. rewrite Val.rolm_rolm.
   rewrite (Int.add_commut Int.zero). rewrite Int.add_zero. TrivialExists.
@@ -262,8 +262,8 @@ Proof.
   red; intros.  unfold shlimm.
   predSpec Int.eq Int.eq_spec n Int.zero.
   subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shl_zero; auto.
-  destruct (Int.ltu n Int.iwordsize) eqn:?. 
-  rewrite Val.shl_rolm; auto. apply eval_rolm; auto. 
+  destruct (Int.ltu n Int.iwordsize) eqn:?.
+  rewrite Val.shl_rolm; auto. apply eval_rolm; auto.
   TrivialExists. econstructor. eauto. econstructor. EvalOp. simpl; eauto. constructor. auto.
 Qed.
 
@@ -274,8 +274,8 @@ Proof.
   red; intros.  unfold shruimm.
   predSpec Int.eq Int.eq_spec n Int.zero.
   subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shru_zero; auto.
-  destruct (Int.ltu n Int.iwordsize) eqn:?. 
-  rewrite Val.shru_rolm; auto. apply eval_rolm; auto. 
+  destruct (Int.ltu n Int.iwordsize) eqn:?.
+  rewrite Val.shru_rolm; auto. apply eval_rolm; auto.
   TrivialExists. econstructor. eauto. econstructor. EvalOp. simpl; eauto. constructor. auto.
 Qed.
 
@@ -283,18 +283,18 @@ Theorem eval_shrimm:
   forall n, unary_constructor_sound (fun a => shrimm a n)
                                     (fun x => Val.shr x (Vint n)).
 Proof.
-  red; intros until x. unfold shrimm. 
+  red; intros until x. unfold shrimm.
   predSpec Int.eq Int.eq_spec n Int.zero.
   intros. subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shr_zero; auto.
   destruct (Int.ltu n Int.iwordsize) eqn:WS.
   case (shrimm_match a); intros.
   InvEval. exists (Vint (Int.shr n1 n)); split. EvalOp. simpl; rewrite WS; auto.
-  simpl; destruct (Int.lt mask1 Int.zero) eqn:?. 
+  simpl; destruct (Int.lt mask1 Int.zero) eqn:?.
   TrivialExists.
-  replace (Val.shr x (Vint n)) with (Val.shru x (Vint n)). 
+  replace (Val.shr x (Vint n)) with (Val.shru x (Vint n)).
   apply eval_shruimm; auto.
   destruct x; simpl; auto. rewrite WS.
-  decEq. symmetry. InvEval. destruct v1; simpl in H0; inv H0. 
+  decEq. symmetry. InvEval. destruct v1; simpl in H0; inv H0.
   apply Int.shr_and_is_shru_and; auto.
   simpl. TrivialExists.
   intros. simpl. TrivialExists.
@@ -304,13 +304,13 @@ Qed.
 Lemma eval_mulimm_base:
   forall n, unary_constructor_sound (mulimm_base n) (fun x => Val.mul x (Vint n)).
 Proof.
-  intros; red; intros; unfold mulimm_base. 
-  generalize (Int.one_bits_decomp n). 
+  intros; red; intros; unfold mulimm_base.
+  generalize (Int.one_bits_decomp n).
   generalize (Int.one_bits_range n).
   destruct (Int.one_bits n).
-  intros. TrivialExists. 
+  intros. TrivialExists.
   destruct l.
-  intros. rewrite H1. simpl. 
+  intros. rewrite H1. simpl.
   rewrite Int.add_zero.
   replace (Vint (Int.shl Int.one i)) with (Val.shl Vone (Vint i)). rewrite Val.shl_mul.
   apply eval_shlimm. auto. simpl. rewrite H0; auto with coqlib.
@@ -325,27 +325,27 @@ Proof.
   replace (Vint (Int.add (Int.shl Int.one i) (Int.shl Int.one i0)))
      with (Val.add (Val.shl Vone (Vint i)) (Val.shl Vone (Vint i0))).
   rewrite Val.mul_add_distr_r.
-  repeat rewrite Val.shl_mul. apply Val.add_lessdef; auto. 
-  simpl. repeat rewrite H0; auto with coqlib. 
-  intros. TrivialExists. 
+  repeat rewrite Val.shl_mul. apply Val.add_lessdef; auto.
+  simpl. repeat rewrite H0; auto with coqlib.
+  intros. TrivialExists.
 Qed.
 
 Theorem eval_mulimm:
   forall n, unary_constructor_sound (mulimm n) (fun x => Val.mul x (Vint n)).
 Proof.
   intros; red; intros until x; unfold mulimm.
-  predSpec Int.eq Int.eq_spec n Int.zero. 
-  intros. exists (Vint Int.zero); split. EvalOp. 
+  predSpec Int.eq Int.eq_spec n Int.zero.
+  intros. exists (Vint Int.zero); split. EvalOp.
   destruct x; simpl; auto. subst n. rewrite Int.mul_zero. auto.
   predSpec Int.eq Int.eq_spec n Int.one.
   intros. exists x; split; auto.
   destruct x; simpl; auto. subst n. rewrite Int.mul_one. auto.
   case (mulimm_match a); intros; InvEval.
   TrivialExists. simpl. rewrite Int.mul_commut; auto.
-  subst. rewrite Val.mul_add_distr_l. 
+  subst. rewrite Val.mul_add_distr_l.
   exploit eval_mulimm_base; eauto. instantiate (1 := n). intros [v' [A1 B1]].
   exploit (eval_addimm (Int.mul n n2) le (mulimm_base n t2) v'). auto. intros [v'' [A2 B2]].
-  exists v''; split; auto. eapply Val.lessdef_trans. eapply Val.add_lessdef; eauto. 
+  exists v''; split; auto. eapply Val.lessdef_trans. eapply Val.add_lessdef; eauto.
   rewrite Val.mul_commut; auto.
   apply eval_mulimm_base; auto.
 Qed.
@@ -354,7 +354,7 @@ Theorem eval_mul: binary_constructor_sound mul Val.mul.
 Proof.
   red; intros until y.
   unfold mul; case (mul_match a b); intros; InvEval.
-  rewrite Val.mul_commut. apply eval_mulimm. auto. 
+  rewrite Val.mul_commut. apply eval_mulimm. auto.
   apply eval_mulimm. auto.
   TrivialExists.
 Qed.
@@ -362,9 +362,9 @@ Qed.
 Theorem eval_andimm:
   forall n, unary_constructor_sound (andimm n) (fun x => Val.and x (Vint n)).
 Proof.
-  intros; red; intros until x. unfold andimm. 
+  intros; red; intros until x. unfold andimm.
   predSpec Int.eq Int.eq_spec n Int.zero.
-  intros. subst. exists (Vint Int.zero); split. EvalOp. 
+  intros. subst. exists (Vint Int.zero); split. EvalOp.
   destruct x; simpl; auto. rewrite Int.and_zero; auto.
   predSpec Int.eq Int.eq_spec n Int.mone.
   intros. subst. exists x; split. auto.
@@ -372,10 +372,10 @@ Proof.
   clear H H0.
   case (andimm_match a); intros.
   InvEval. TrivialExists. simpl. rewrite Int.and_commut; auto.
-  set (n' := Int.and n n2). 
+  set (n' := Int.and n n2).
   destruct (Int.eq (Int.shru (Int.shl n' amount) amount) n' &&
             Int.ltu amount Int.iwordsize) eqn:?.
-  InvEval. destruct (andb_prop _ _ Heqb). 
+  InvEval. destruct (andb_prop _ _ Heqb).
   generalize (Int.eq_spec (Int.shru (Int.shl n' amount) amount) n'). rewrite H1; intros.
   replace (Val.and x (Vint n))
      with (Val.rolm v0 (Int.sub Int.iwordsize amount) (Int.and (Int.shru Int.mone amount) n')).
@@ -383,26 +383,26 @@ Proof.
   subst. destruct v0; simpl; auto. rewrite H3. simpl. decEq. rewrite Int.and_assoc.
   rewrite (Int.and_commut n2 n).
   transitivity (Int.and (Int.shru i amount) (Int.and n n2)).
-  rewrite (Int.shru_rolm i); auto. unfold Int.rolm. rewrite Int.and_assoc; auto. 
+  rewrite (Int.shru_rolm i); auto. unfold Int.rolm. rewrite Int.and_assoc; auto.
   symmetry. apply Int.shr_and_shru_and. auto.
   set (e2 := Eop (Oshrimm amount) (t2 ::: Enil)) in *.
-  InvEval. subst. rewrite Val.and_assoc. simpl. rewrite Int.and_commut. TrivialExists.  
-  InvEval. subst. rewrite Val.and_assoc. simpl. rewrite Int.and_commut. TrivialExists. 
-  InvEval. subst. TrivialExists. simpl. 
-  destruct v1; auto. simpl. unfold Int.rolm. rewrite Int.and_assoc. 
+  InvEval. subst. rewrite Val.and_assoc. simpl. rewrite Int.and_commut. TrivialExists.
+  InvEval. subst. rewrite Val.and_assoc. simpl. rewrite Int.and_commut. TrivialExists.
+  InvEval. subst. TrivialExists. simpl.
+  destruct v1; auto. simpl. unfold Int.rolm. rewrite Int.and_assoc.
   decEq. decEq. decEq. apply Int.and_commut.
   destruct (Int.eq (Int.shru (Int.shl n amount) amount) n &&
             Int.ltu amount Int.iwordsize) eqn:?.
-  InvEval. destruct (andb_prop _ _ Heqb). 
+  InvEval. destruct (andb_prop _ _ Heqb).
   generalize (Int.eq_spec (Int.shru (Int.shl n amount) amount) n). rewrite H0; intros.
   replace (Val.and x (Vint n))
      with (Val.rolm v1 (Int.sub Int.iwordsize amount) (Int.and (Int.shru Int.mone amount) n)).
   apply eval_rolm; auto.
-  subst x. destruct v1; simpl; auto. rewrite H1; simpl. decEq. 
+  subst x. destruct v1; simpl; auto. rewrite H1; simpl. decEq.
   transitivity (Int.and (Int.shru i amount) n).
-  rewrite (Int.shru_rolm i); auto. unfold Int.rolm. rewrite Int.and_assoc; auto. 
+  rewrite (Int.shru_rolm i); auto. unfold Int.rolm. rewrite Int.and_assoc; auto.
   symmetry. apply Int.shr_and_shru_and. auto.
-  TrivialExists. 
+  TrivialExists.
   TrivialExists.
 Qed.
 
@@ -426,7 +426,7 @@ Proof.
   intros. subst. exists (Vint Int.mone); split. EvalOp. destruct x; simpl; auto. rewrite Int.or_mone; auto.
   clear H H0. destruct (orimm_match a); intros; InvEval.
   TrivialExists. simpl. rewrite Int.or_commut; auto.
-  subst. rewrite Val.or_assoc. simpl. rewrite Int.or_commut. TrivialExists. 
+  subst. rewrite Val.or_assoc. simpl. rewrite Int.or_commut. TrivialExists.
   TrivialExists.
 Qed.
 
@@ -438,10 +438,10 @@ Remark eval_same_expr:
   a1 = a2 /\ v1 = v2.
 Proof.
   intros until v2.
-  destruct a1; simpl; try (intros; discriminate). 
+  destruct a1; simpl; try (intros; discriminate).
   destruct a2; simpl; try (intros; discriminate).
   case (ident_eq i i0); intros.
-  subst i0. inversion H0. inversion H1. split. auto. congruence. 
+  subst i0. inversion H0. inversion H1. split. auto. congruence.
   discriminate.
 Qed.
 
@@ -452,29 +452,29 @@ Proof.
   destruct (Int.eq amount1 amount2 && same_expr_pure t1 t2) eqn:?.
   destruct (andb_prop _ _ Heqb0).
   generalize (Int.eq_spec amount1 amount2). rewrite H1. intro. subst amount2.
-  InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]. subst. 
+  InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]. subst.
   rewrite Val.or_rolm. TrivialExists.
   TrivialExists.
 (* andimm - rolm *)
   destruct (Int.eq mask1 (Int.not mask2) && is_rlw_mask mask2) eqn:?.
-  destruct (andb_prop _ _ Heqb0). 
+  destruct (andb_prop _ _ Heqb0).
   generalize (Int.eq_spec mask1 (Int.not mask2)); rewrite H1; intros.
-  InvEval. subst. TrivialExists. 
+  InvEval. subst. TrivialExists.
   TrivialExists.
 (* rolm - andimm *)
   destruct (Int.eq mask2 (Int.not mask1) && is_rlw_mask mask1) eqn:?.
-  destruct (andb_prop _ _ Heqb0). 
+  destruct (andb_prop _ _ Heqb0).
   generalize (Int.eq_spec mask2 (Int.not mask1)); rewrite H1; intros.
   InvEval. subst. rewrite Val.or_commut. TrivialExists.
   TrivialExists.
 (* intconst *)
-  InvEval. rewrite Val.or_commut. apply eval_orimm; auto. 
+  InvEval. rewrite Val.or_commut. apply eval_orimm; auto.
   InvEval. apply eval_orimm; auto.
 (* orc *)
   InvEval. subst. rewrite Val.or_commut. TrivialExists.
   InvEval. subst. TrivialExists.
 (* default *)
-  TrivialExists. 
+  TrivialExists.
 Qed.
 
 Theorem eval_xorimm:
@@ -484,11 +484,11 @@ Proof.
   predSpec Int.eq Int.eq_spec n Int.zero.
   intros. subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.xor_zero; auto.
   predSpec Int.eq Int.eq_spec n Int.mone.
-  intros. subst. rewrite <- Val.not_xor. apply eval_notint; auto. 
+  intros. subst. rewrite <- Val.not_xor. apply eval_notint; auto.
   clear H H0. destruct (xorimm_match a); intros; InvEval.
   TrivialExists. simpl. rewrite Int.xor_commut; auto.
   subst. rewrite Val.xor_assoc. simpl. rewrite Int.xor_commut. TrivialExists.
-  subst x. TrivialExists. simpl. rewrite Val.not_xor. rewrite Val.xor_assoc. 
+  subst x. TrivialExists. simpl. rewrite Val.not_xor. rewrite Val.xor_assoc.
   simpl. rewrite Int.xor_commut; auto.
   TrivialExists.
 Qed.
@@ -498,7 +498,7 @@ Proof.
   red; intros until y; unfold xor; case (xor_match a b); intros; InvEval.
   rewrite Val.xor_commut. apply eval_xorimm; auto.
   apply eval_xorimm; auto.
-  subst. rewrite Val.xor_commut. rewrite Val.not_xor. rewrite <- Val.xor_assoc. 
+  subst. rewrite Val.xor_commut. rewrite Val.not_xor. rewrite <- Val.xor_assoc.
   rewrite <- Val.not_xor. rewrite Val.xor_commut. TrivialExists.
   subst. rewrite Val.not_xor. rewrite <- Val.xor_assoc. rewrite <- Val.not_xor. TrivialExists.
   TrivialExists.
@@ -524,19 +524,19 @@ Lemma eval_mod_aux:
   eval_expr ge sp e m le (mod_aux divop a b) (Val.sub x (Val.mul z y)).
 Proof.
   intros; unfold mod_aux.
-  eapply eval_Elet. eexact H0. eapply eval_Elet. 
+  eapply eval_Elet. eexact H0. eapply eval_Elet.
   apply eval_lift. eexact H1.
-  eapply eval_Eop. eapply eval_Econs. 
+  eapply eval_Eop. eapply eval_Econs.
   eapply eval_Eletvar. simpl; reflexivity.
-  eapply eval_Econs. eapply eval_Eop. 
+  eapply eval_Econs. eapply eval_Eop.
   eapply eval_Econs. eapply eval_Eop.
   eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity.
   eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity.
-  apply eval_Enil.  
+  apply eval_Enil.
   rewrite H. eauto.
   eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity.
-  apply eval_Enil.  
-  simpl; reflexivity. apply eval_Enil. 
+  apply eval_Enil.
+  simpl; reflexivity. apply eval_Enil.
   reflexivity.
 Qed.
 
@@ -547,7 +547,7 @@ Theorem eval_mods_base:
   Val.mods x y = Some z ->
   exists v, eval_expr ge sp e m le (mods_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros; unfold mods_base. 
+  intros; unfold mods_base.
   exploit Val.mods_divs; eauto. intros [v [A B]].
   subst. econstructor; split; eauto.
   apply eval_mod_aux with (semdivop := Val.divs); auto.
@@ -570,7 +570,7 @@ Theorem eval_modu_base:
   Val.modu x y = Some z ->
   exists v, eval_expr ge sp e m le (modu_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros; unfold modu_base. 
+  intros; unfold modu_base.
   exploit Val.modu_divu; eauto. intros [v [A B]].
   subst. econstructor; split; eauto.
   apply eval_mod_aux with (semdivop := Val.divu); auto.
@@ -582,13 +582,13 @@ Theorem eval_shrximm:
   Val.shrx x (Vint n) = Some z ->
   exists v, eval_expr ge sp e m le (shrximm a n) v /\ Val.lessdef z v.
 Proof.
-  intros. unfold shrximm. 
+  intros. unfold shrximm.
   predSpec Int.eq Int.eq_spec n Int.zero.
-  subst n. exists x; split; auto. 
+  subst n. exists x; split; auto.
   destruct x; simpl in H0; try discriminate.
   destruct (Int.ltu Int.zero (Int.repr 31)); inv H0.
-  replace (Int.shrx i Int.zero) with i. auto. 
-  unfold Int.shrx, Int.divs. rewrite Int.shl_zero. 
+  replace (Int.shrx i Int.zero) with i. auto.
+  unfold Int.shrx, Int.divs. rewrite Int.shl_zero.
   change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed; auto.
   econstructor; split. EvalOp. auto.
 Qed.
@@ -597,38 +597,38 @@ Theorem eval_shl: binary_constructor_sound shl Val.shl.
 Proof.
   red; intros until y; unfold shl; case (shl_match b); intros.
   InvEval. apply eval_shlimm; auto.
-  TrivialExists. 
+  TrivialExists.
 Qed.
 
 Theorem eval_shr: binary_constructor_sound shr Val.shr.
 Proof.
   red; intros until y; unfold shr; case (shr_match b); intros.
   InvEval. apply eval_shrimm; auto.
-  TrivialExists. 
+  TrivialExists.
 Qed.
 
 Theorem eval_shru: binary_constructor_sound shru Val.shru.
 Proof.
   red; intros until y; unfold shru; case (shru_match b); intros.
   InvEval. apply eval_shruimm; auto.
-  TrivialExists. 
+  TrivialExists.
 Qed.
 
 Theorem eval_negf: unary_constructor_sound negf Val.negf.
 Proof.
-  red; intros. TrivialExists. 
+  red; intros. TrivialExists.
 Qed.
 
 Theorem eval_absf: unary_constructor_sound absf Val.absf.
 Proof.
-  red; intros. TrivialExists. 
+  red; intros. TrivialExists.
 Qed.
 
 Theorem eval_addf: binary_constructor_sound addf Val.addf.
 Proof.
   red; intros; TrivialExists.
 Qed.
- 
+
 Theorem eval_subf: binary_constructor_sound subf Val.subf.
 Proof.
   red; intros; TrivialExists.
@@ -641,19 +641,19 @@ Qed.
 
 Theorem eval_negfs: unary_constructor_sound negfs Val.negfs.
 Proof.
-  red; intros. TrivialExists. 
+  red; intros. TrivialExists.
 Qed.
 
 Theorem eval_absfs: unary_constructor_sound absfs Val.absfs.
 Proof.
-  red; intros. TrivialExists. 
+  red; intros. TrivialExists.
 Qed.
 
 Theorem eval_addfs: binary_constructor_sound addfs Val.addfs.
 Proof.
   red; intros; TrivialExists.
 Qed.
- 
+
 Theorem eval_subfs: binary_constructor_sound subfs Val.subfs.
 Proof.
   red; intros; TrivialExists.
@@ -687,8 +687,8 @@ Proof.
 (* constant *)
   InvEval. rewrite sem_int. TrivialExists. simpl. destruct (intsem c0 n1 n2); auto.
 (* eq cmp *)
-  InvEval. inv H. simpl in H5. inv H5. 
-  destruct (Int.eq_dec n2 Int.zero). subst n2. TrivialExists. 
+  InvEval. inv H. simpl in H5. inv H5.
+  destruct (Int.eq_dec n2 Int.zero). subst n2. TrivialExists.
   simpl. rewrite eval_negate_condition.
   destruct (eval_condition c0 vl m); simpl.
   unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_eq; auto.
@@ -697,13 +697,13 @@ Proof.
   simpl. destruct (eval_condition c0 vl m); simpl.
   unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_eq; auto.
   rewrite sem_undef; auto.
-  exists (Vint Int.zero); split. EvalOp. 
+  exists (Vint Int.zero); split. EvalOp.
   destruct (eval_condition c0 vl m); simpl.
   unfold Vtrue, Vfalse. destruct b; rewrite sem_eq; rewrite Int.eq_false; auto.
   rewrite sem_undef; auto.
 (* ne cmp *)
-  InvEval. inv H. simpl in H5. inv H5. 
-  destruct (Int.eq_dec n2 Int.zero). subst n2. TrivialExists. 
+  InvEval. inv H. simpl in H5. inv H5.
+  destruct (Int.eq_dec n2 Int.zero). subst n2. TrivialExists.
   simpl. destruct (eval_condition c0 vl m); simpl.
   unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_ne; auto.
   rewrite sem_undef; auto.
@@ -711,21 +711,21 @@ Proof.
   simpl. rewrite eval_negate_condition. destruct (eval_condition c0 vl m); simpl.
   unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_ne; auto.
   rewrite sem_undef; auto.
-  exists (Vint Int.one); split. EvalOp. 
+  exists (Vint Int.one); split. EvalOp.
   destruct (eval_condition c0 vl m); simpl.
   unfold Vtrue, Vfalse. destruct b; rewrite sem_ne; rewrite Int.eq_false; auto.
   rewrite sem_undef; auto.
 (* eq andimm *)
   destruct (Int.eq_dec n2 Int.zero). InvEval; subst.
-  econstructor; split. EvalOp. simpl; eauto. 
-  destruct v1; simpl; try (rewrite sem_undef; auto). rewrite sem_eq. 
-  destruct (Int.eq (Int.and i n1) Int.zero); auto. 
+  econstructor; split. EvalOp. simpl; eauto.
+  destruct v1; simpl; try (rewrite sem_undef; auto). rewrite sem_eq.
+  destruct (Int.eq (Int.and i n1) Int.zero); auto.
   TrivialExists. simpl. rewrite sem_default. auto.
 (* ne andimm *)
   destruct (Int.eq_dec n2 Int.zero). InvEval; subst.
-  econstructor; split. EvalOp. simpl; eauto. 
-  destruct v1; simpl; try (rewrite sem_undef; auto). rewrite sem_ne. 
-  destruct (Int.eq (Int.and i n1) Int.zero); auto. 
+  econstructor; split. EvalOp. simpl; eauto.
+  destruct v1; simpl; try (rewrite sem_undef; auto). rewrite sem_ne.
+  destruct (Int.eq (Int.and i n1) Int.zero); auto.
   TrivialExists. simpl. rewrite sem_default. auto.
 (* default *)
   TrivialExists. simpl. rewrite sem_default. auto.
@@ -740,7 +740,7 @@ Lemma eval_compimm_swap:
   exists v, eval_expr ge sp e m le (compimm default intsem (swap_comparison c) a n2) v
          /\ Val.lessdef (sem c (Vint n2) x) v.
 Proof.
-  intros. rewrite <- sem_swap. eapply eval_compimm; eauto. 
+  intros. rewrite <- sem_swap. eapply eval_compimm; eauto.
 Qed.
 
 End COMP_IMM.
@@ -749,9 +749,9 @@ Theorem eval_comp:
   forall c, binary_constructor_sound (comp c) (Val.cmp c).
 Proof.
   intros; red; intros until y. unfold comp; case (comp_match a b); intros; InvEval.
-  eapply eval_compimm_swap; eauto. 
+  eapply eval_compimm_swap; eauto.
   intros. unfold Val.cmp. rewrite Val.swap_cmp_bool; auto.
-  eapply eval_compimm; eauto. 
+  eapply eval_compimm; eauto.
   TrivialExists.
 Qed.
 
@@ -759,9 +759,9 @@ Theorem eval_compu:
   forall c, binary_constructor_sound (compu c) (Val.cmpu (Mem.valid_pointer m) c).
 Proof.
   intros; red; intros until y. unfold compu; case (compu_match a b); intros; InvEval.
-  eapply eval_compimm_swap; eauto. 
+  eapply eval_compimm_swap; eauto.
   intros. unfold Val.cmpu. rewrite Val.swap_cmpu_bool; auto.
-  eapply eval_compimm; eauto. 
+  eapply eval_compimm; eauto.
   TrivialExists.
 Qed.
 
@@ -777,11 +777,11 @@ Proof.
   intros; red; intros. unfold compfs.
   replace (Val.cmpfs c x y) with
           (Val.cmpf c (Val.floatofsingle x) (Val.floatofsingle y)).
-  TrivialExists. constructor. EvalOp. simpl; reflexivity. 
+  TrivialExists. constructor. EvalOp. simpl; reflexivity.
   constructor. EvalOp. simpl; reflexivity. constructor.
-  auto. 
-  destruct x; auto. destruct y; auto. unfold Val.cmpf, Val.cmpfs; simpl. 
-  rewrite Float32.cmp_double. auto. 
+  auto.
+  destruct x; auto. destruct y; auto. unfold Val.cmpf, Val.cmpfs; simpl.
+  rewrite Float32.cmp_double. auto.
 Qed.
 
 Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8).
@@ -826,7 +826,7 @@ Theorem eval_intoffloat:
   Val.intoffloat x = Some y ->
   exists v, eval_expr ge sp e m le (intoffloat a) v /\ Val.lessdef y v.
 Proof.
-  intros; unfold intoffloat. TrivialExists. 
+  intros; unfold intoffloat. TrivialExists.
 Qed.
 
 Theorem eval_intuoffloat:
@@ -847,24 +847,24 @@ Proof.
   assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar O) (Vfloat fm)).
     constructor. auto.
   econstructor. eauto.
-  econstructor. instantiate (1 := Vfloat fm). EvalOp. 
+  econstructor. instantiate (1 := Vfloat fm). EvalOp.
   eapply eval_Econdition with (va := Float.cmp Clt f fm).
   eauto with evalexpr.
   destruct (Float.cmp Clt f fm) eqn:?.
   exploit Float.to_intu_to_int_1; eauto. intro EQ.
   EvalOp. simpl. rewrite EQ; auto.
-  exploit Float.to_intu_to_int_2; eauto. 
+  exploit Float.to_intu_to_int_2; eauto.
   change Float.ox8000_0000 with im. fold fm. intro EQ.
   set (t2 := subf (Eletvar (S O)) (Eletvar O)).
   set (t3 := intoffloat t2).
   exploit (eval_subf (Vfloat fm :: Vfloat f :: le) (Eletvar (S O)) (Vfloat f) (Eletvar O)); eauto.
-  fold t2. intros [v2 [A2 B2]]. simpl in B2. inv B2. 
+  fold t2. intros [v2 [A2 B2]]. simpl in B2. inv B2.
   exploit (eval_addimm Float.ox8000_0000 (Vfloat fm :: Vfloat f :: le) t3).
-    unfold t3. unfold intoffloat. EvalOp. simpl. rewrite EQ. simpl. eauto. 
-  intros [v4 [A4 B4]]. simpl in B4. inv B4. 
-  rewrite Int.sub_add_opp in A4. rewrite Int.add_assoc in A4. 
-  rewrite (Int.add_commut (Int.neg im)) in A4. 
-  rewrite Int.add_neg_zero in A4. 
+    unfold t3. unfold intoffloat. EvalOp. simpl. rewrite EQ. simpl. eauto.
+  intros [v4 [A4 B4]]. simpl in B4. inv B4.
+  rewrite Int.sub_add_opp in A4. rewrite Int.add_assoc in A4.
+  rewrite (Int.add_commut (Int.neg im)) in A4.
+  rewrite Int.add_neg_zero in A4.
   rewrite Int.add_zero in A4.
   auto.
 Qed.
@@ -876,20 +876,20 @@ Theorem eval_floatofint:
   exists v, eval_expr ge sp e m le (floatofint a) v /\ Val.lessdef y v.
 Proof.
   intros until y. unfold floatofint. destruct (floatofint_match a); intros.
-  InvEval. TrivialExists. 
+  InvEval. TrivialExists.
   destruct Archi.ppc64.
-  TrivialExists. 
+  TrivialExists.
   rename e0 into a. destruct x; simpl in H0; inv H0.
   exists (Vfloat (Float.of_int i)); split; auto.
   set (t1 := addimm Float.ox8000_0000 a).
   set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: t1 ::: Enil)).
   set (t3 := Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil).
-  exploit (eval_addimm Float.ox8000_0000 le a). eauto. fold t1. 
+  exploit (eval_addimm Float.ox8000_0000 le a). eauto. fold t1.
   intros [v1 [A1 B1]]. simpl in B1. inv B1.
-  exploit (eval_subf le t2). 
-  unfold t2. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. 
-  unfold eval_operation. eauto. 
-  instantiate (2 := t3). unfold t3. EvalOp. simpl; eauto.  
+  exploit (eval_subf le t2).
+  unfold t2. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor.
+  unfold eval_operation. eauto.
+  instantiate (2 := t3). unfold t3. EvalOp. simpl; eauto.
   intros [v2 [A2 B2]]. simpl in B2. inv B2. rewrite Float.of_int_from_words. auto.
 Qed.
 
@@ -902,15 +902,15 @@ Proof.
   intros until y. unfold floatofintu. destruct (floatofintu_match a); intros.
   InvEval. TrivialExists.
   destruct Archi.ppc64.
-  TrivialExists. 
+  TrivialExists.
   rename e0 into a. destruct x; simpl in H0; inv H0.
   exists (Vfloat (Float.of_intu i)); split; auto.
   unfold floatofintu.
   set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: a ::: Enil)).
   set (t3 := Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil).
-  exploit (eval_subf le t2). 
-  unfold t2. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. 
-  unfold eval_operation. eauto. 
+  exploit (eval_subf le t2).
+  unfold t2. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor.
+  unfold eval_operation. eauto.
   instantiate (2 := t3). unfold t3. EvalOp. simpl; eauto.
   intros [v2 [A2 B2]]. simpl in B2. inv B2. rewrite Float.of_intu_from_words. auto.
 Qed.
@@ -921,14 +921,14 @@ Theorem eval_intofsingle:
   Val.intofsingle x = Some y ->
   exists v, eval_expr ge sp e m le (intofsingle a) v /\ Val.lessdef y v.
 Proof.
-  intros; unfold intofsingle. 
+  intros; unfold intofsingle.
   assert (Val.intoffloat (Val.floatofsingle x) = Some y).
   { destruct x; simpl in H0; try discriminate.
-    destruct (Float32.to_int f) eqn:F; inv H0. 
-    apply Float32.to_int_double in F. 
-    simpl. unfold Float32.to_double in F; rewrite F; auto.  
+    destruct (Float32.to_int f) eqn:F; inv H0.
+    apply Float32.to_int_double in F.
+    simpl. unfold Float32.to_double in F; rewrite F; auto.
   }
-  apply eval_intoffloat with (Val.floatofsingle x); auto. EvalOp. 
+  apply eval_intoffloat with (Val.floatofsingle x); auto. EvalOp.
 Qed.
 
 Theorem eval_singleofint:
@@ -941,11 +941,11 @@ Proof.
   assert (exists z, Val.floatofint x = Some z /\ y = Val.singleoffloat z).
   {
     destruct x; inv H0. simpl. exists (Vfloat (Float.of_int i)); simpl; split; auto.
-    f_equal. apply Float32.of_int_double. 
+    f_equal. apply Float32.of_int_double.
   }
-  destruct H1 as (z & A & B). subst y. 
-  exploit eval_floatofint; eauto. intros (v & C & D). 
-  exists (Val.singleoffloat v); split. EvalOp. inv D; auto. 
+  destruct H1 as (z & A & B). subst y.
+  exploit eval_floatofint; eauto. intros (v & C & D).
+  exists (Val.singleoffloat v); split. EvalOp. inv D; auto.
 Qed.
 
 Theorem eval_intuofsingle:
@@ -954,14 +954,14 @@ Theorem eval_intuofsingle:
   Val.intuofsingle x = Some y ->
   exists v, eval_expr ge sp e m le (intuofsingle a) v /\ Val.lessdef y v.
 Proof.
-  intros; unfold intuofsingle. 
+  intros; unfold intuofsingle.
   assert (Val.intuoffloat (Val.floatofsingle x) = Some y).
   { destruct x; simpl in H0; try discriminate.
-    destruct (Float32.to_intu f) eqn:F; inv H0. 
-    apply Float32.to_intu_double in F. 
-    simpl. unfold Float32.to_double in F; rewrite F; auto.  
+    destruct (Float32.to_intu f) eqn:F; inv H0.
+    apply Float32.to_intu_double in F.
+    simpl. unfold Float32.to_double in F; rewrite F; auto.
   }
-  apply eval_intuoffloat with (Val.floatofsingle x); auto. EvalOp. 
+  apply eval_intuoffloat with (Val.floatofsingle x); auto. EvalOp.
 Qed.
 
 Theorem eval_singleofintu:
@@ -974,11 +974,11 @@ Proof.
   assert (exists z, Val.floatofintu x = Some z /\ y = Val.singleoffloat z).
   {
     destruct x; inv H0. simpl. exists (Vfloat (Float.of_intu i)); simpl; split; auto.
-    f_equal. apply Float32.of_intu_double. 
+    f_equal. apply Float32.of_intu_double.
   }
-  destruct H1 as (z & A & B). subst y. 
-  exploit eval_floatofintu; eauto. intros (v & C & D). 
-  exists (Val.singleoffloat v); split. EvalOp. inv D; auto. 
+  destruct H1 as (z & A & B). subst y.
+  exploit eval_floatofintu; eauto. intros (v & C & D).
+  exists (Val.singleoffloat v); split. EvalOp. inv D; auto.
 Qed.
 
 Theorem eval_addressing:
@@ -987,7 +987,7 @@ Theorem eval_addressing:
   v = Vptr b ofs ->
   match addressing chunk a with (mode, args) =>
     exists vl,
-    eval_exprlist ge sp e m le args vl /\ 
+    eval_exprlist ge sp e m le args vl /\
     eval_addressing ge sp mode vl = Some v
   end.
 Proof.
@@ -996,12 +996,12 @@ Proof.
   exists (@nil val). split. eauto with evalexpr. simpl. auto.
   exists (v1 :: nil). split. eauto with evalexpr. simpl. congruence.
   exists (v1 :: nil). split. eauto with evalexpr. simpl. congruence.
-  destruct (can_use_Aindexed2 chunk). 
+  destruct (can_use_Aindexed2 chunk).
   exists (v1 :: v0 :: nil). split. eauto with evalexpr. simpl. congruence.
   exists (Vptr b ofs :: nil). split.
-  constructor. EvalOp. simpl; congruence. constructor. 
+  constructor. EvalOp. simpl; congruence. constructor.
   simpl. rewrite Int.add_zero. auto.
-  exists (v :: nil). split. eauto with evalexpr. subst v. simpl. 
+  exists (v :: nil). split. eauto with evalexpr. subst v. simpl.
   rewrite Int.add_zero. auto.
 Qed.
 
@@ -1013,7 +1013,7 @@ Proof.
   intros until v. unfold builtin_arg; case (builtin_arg_match a); intros; InvEval.
 - constructor.
 - constructor.
-- constructor. 
+- constructor.
 - simpl in H5. inv H5. constructor.
 - subst v. constructor; auto.
 - inv H. InvEval. simpl in H6; inv H6. constructor; auto.
diff --git a/powerpc/Stacklayout.v b/powerpc/Stacklayout.v
index be823c1e..a751fd98 100644
--- a/powerpc/Stacklayout.v
+++ b/powerpc/Stacklayout.v
@@ -117,10 +117,10 @@ Proof.
     fe_ofs_float_callee_save, fe_num_float_callee_save,
     fe_stack_data.
   set (x1 := align (8 + 4 * bound_outgoing b) 8).
-  assert (8 | x1). unfold x1; apply align_divides. omega. 
+  assert (8 | x1). unfold x1; apply align_divides. omega.
   set (x2 := x1 + 4 * bound_local b).
   assert (4 | x2). unfold x2; apply Zdivide_plus_r; auto.
-  apply Zdivides_trans with 8. exists 2; auto. auto. 
+  apply Zdivides_trans with 8. exists 2; auto. auto.
   exists (bound_local b); ring.
   set (x3 := x2 + 4).
   assert (4 | x3). unfold x3; apply Zdivide_plus_r; auto. exists 1; auto.
diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v
index bcd1e80e..fe5a0792 100644
--- a/powerpc/ValueAOp.v
+++ b/powerpc/ValueAOp.v
@@ -162,7 +162,7 @@ Theorem eval_static_addressing_sound:
 Proof.
   unfold eval_addressing, eval_static_addressing; intros;
   destruct addr; InvHyps; eauto with va.
-  rewrite Int.add_zero_l; auto with va. 
+  rewrite Int.add_zero_l; auto with va.
 Qed.
 
 Theorem eval_static_operation_sound:
@@ -177,8 +177,8 @@ Proof.
   destruct (propagate_float_constants tt); constructor.
   rewrite Int.add_zero_l; eauto with va.
   fold (Val.sub (Vint i) a1). auto with va.
-  apply floatofwords_sound; auto. 
-  apply of_optbool_sound. eapply eval_static_condition_sound; eauto. 
+  apply floatofwords_sound; auto.
+  apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
 Qed.
 
 End SOUNDNESS.