Updated PR by removing whitespaces. Bug 17450.

17 files changed, 621 insertions, 621 deletions

diff --git a/ia32/Archi.v b/ia32/Archi.v
index 674b2761..267c0eee 100644
--- a/ia32/Archi.v
+++ b/ia32/Archi.v
@@ -25,13 +25,13 @@ Definition big_endian := false.
 Notation align_int64 := 4%Z (only parsing).
 Notation align_float64 := 4%Z (only parsing).
 
-Program Definition default_pl_64 : bool * nan_pl 53 := 
+Program Definition default_pl_64 : bool * nan_pl 53 :=
   (true, 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 :=
   (true, 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/ia32/Asm.v b/ia32/Asm.v
index 979041ba..f3ec3703 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -50,7 +50,7 @@ Proof. decide equality. Defined.
 
 (** Bits of the flags register. *)
 
-Inductive crbit: Type := 
+Inductive crbit: Type :=
   | ZF | CF | PF | SF | OF.
 
 (** All registers modeled here. *)
@@ -169,7 +169,7 @@ Inductive instruction: Type :=
   | Psar_ri (rd: ireg) (n: int)
   | Pshld_ri (rd: ireg) (r1: ireg) (n: int)
   | Pror_ri (rd: ireg) (n: int)
-  | Pcmp_rr (r1 r2: ireg) 
+  | Pcmp_rr (r1 r2: ireg)
   | Pcmp_ri (r1: ireg) (n: int)
   | Ptest_rr (r1 r2: ireg)
   | Ptest_ri (r1: ireg) (n: int)
@@ -517,7 +517,7 @@ Definition exec_store (chunk: memory_chunk) (m: mem)
     that correspond to actual IA32 instructions, the cases are
     straightforward transliterations of the informal descriptions
     given in the IA32 reference manuals.  For pseudo-instructions,
-    refer to the informal descriptions given above.  
+    refer to the informal descriptions given above.
 
     Note that we set to [Vundef] the registers used as temporaries by
     the expansions of the pseudo-instructions, so that the IA32 code
@@ -735,7 +735,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       end
   | Pjmptbl 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 m
@@ -818,14 +818,14 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pminsd _ _
   | Pmovb_rm _ _
   | Pmovq_rm _ _
-  | Pmovq_mr _ _   
+  | Pmovq_mr _ _
   | Pmovsb
   | Pmovsw
-  | Pmovw_rm _ _ 
+  | Pmovw_rm _ _
   | Prep_movsl
   | Psbb_rr _ _
   | Psqrtsd _ _
-  | Psub_ri _ _ => Stuck 
+  | Psub_ri _ _ => Stuck
   end.
 
 (** Translation of the LTL/Linear/Mach view of machine registers
@@ -891,7 +891,7 @@ Inductive step: state -> trace -> state -> Prop :=
       find_instr (Int.unsigned ofs) f.(fn_code) = Some (Pbuiltin ef args res) ->
       eval_builtin_args ge rs (rs ESP) m args vargs ->
       external_call ef ge vargs m t vres m' ->
-      rs' = nextinstr_nf 
+      rs' = nextinstr_nf
              (set_res res vres
                (undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) ->
       step (State rs m) t (State rs' m')
@@ -924,7 +924,7 @@ Inductive final_state: state -> int -> Prop :=
       rs#PC = Vzero ->
       rs#EAX = Vint r ->
       final_state (State rs m) r.
-      
+
 Definition semantics (p: program) :=
   Semantics step (initial_state p) final_state (Genv.globalenv p).
 
@@ -939,9 +939,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/ia32/Asmexpand.ml b/ia32/Asmexpand.ml
index 99babeb4..d11d9d23 100644
--- a/ia32/Asmexpand.ml
+++ b/ia32/Asmexpand.ml
@@ -21,7 +21,7 @@ open AST
 open Camlcoq
 open Datatypes
 open Integers
-       
+
 exception Error of string
 
 (* Useful constants and helper functions *)
@@ -35,14 +35,14 @@ let _8 = coqint_of_camlint 8l
 let stack_alignment () =
   if Configuration.system = "macoxs" then 16
   else 8
-	 
+
 (* SP adjustment to allocate or free a stack frame *)
-			   
+
 let int32_align n a =
   if n >= 0l
   then Int32.logand (Int32.add n (Int32.of_int (a-1))) (Int32.of_int (-a))
   else Int32.logand n (Int32.of_int (-a))
-		    
+
 let sp_adjustment sz =
   let sz = camlint_of_coqint sz in
   (* Preserve proper alignment of the stack *)
@@ -50,9 +50,9 @@ let sp_adjustment sz =
   (* The top 4 bytes have already been allocated by the "call" instruction. *)
   let sz = Int32.sub sz 4l in
   sz
-			   
-			   
-(* Built-ins.  They come in two flavors: 
+
+
+(* Built-ins.  They come in two flavors:
    - annotation statements: take their arguments in registers or stack
    locations; generate no code;
    - inlined by the compiler: take their arguments in arbitrary
@@ -88,7 +88,7 @@ let offset_addressing (Addrmode(base, ofs, cst)) delta =
 
 let linear_addr reg ofs = Addrmode(Some reg, None, Coq_inl ofs)
 let global_addr id ofs = Addrmode(None, None, Coq_inr(id, ofs))
-			   
+
 (* Handling of memcpy *)
 
 (* Unaligned memory accesses are quite fast on IA32, so use large
@@ -128,7 +128,7 @@ let expand_builtin_memcpy sz al args =
   if sz <= 32
   then expand_builtin_memcpy_small sz al src dst
   else expand_builtin_memcpy_big sz al src dst
- 	   
+
 (* Handling of volatile reads and writes *)
 
 let expand_builtin_vload_common chunk addr res =
@@ -197,9 +197,9 @@ let expand_builtin_vstore chunk args =
      expand_builtin_vstore_common chunk addr src
        (if Asmgen.addressing_mentions addr EAX then ECX else EAX)
   | _ -> assert false
-		 
+
 (* Handling of varargs *)
-		 
+
 let expand_builtin_va_start r =
   if not !current_function.fn_sig.sig_cc.cc_vararg then
     invalid_arg "Fatal error: va_start used in non-vararg function";
@@ -231,7 +231,7 @@ let expand_fma args res i132 i213 i231 =
       end
   | _ ->
      invalid_arg ("ill-formed fma builtin")
-	   
+
 (* Handling of compiler-inlined builtins *)
 
 let expand_builtin_inline name args res =
@@ -348,7 +348,7 @@ let expand_builtin_inline name args res =
      raise (Error ("unrecognized builtin " ^ name))
 
 (* Expansion of instructions *)
-       
+
 let expand_instruction instr =
   match instr with
   | Pallocframe (sz, ofs_ra, ofs_link) ->
@@ -379,14 +379,14 @@ let expand_instruction instr =
 	    (Int32.to_int (camlint_of_coqint al))
             args
        | EF_annot_val(txt, targ) ->
-          expand_annot_val txt targ args res      
+          expand_annot_val txt targ args res
        | EF_annot _ | EF_debug _ | EF_inline_asm _ ->
           emit instr
        | _ ->
           assert false
      end
   | _ -> emit instr
-       
+
 let int_reg_to_dwarf = function
   | EAX -> 0
   | EBX -> 3
diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v
index 1ccde43b..91122898 100644
--- a/ia32/Asmgen.v
+++ b/ia32/Asmgen.v
@@ -78,7 +78,7 @@ Definition addressing_mentions (addr: addrmode) (r: ireg) : bool :=
    || match displ with Some(r', sc) => ireg_eq r r' | None => false end
   end.
 
-Definition mk_smallstore (sto: addrmode -> ireg ->instruction) 
+Definition mk_smallstore (sto: addrmode -> ireg ->instruction)
                          (addr: addrmode) (rs: ireg) (k: code) :=
   if low_ireg rs then
     OK (sto addr rs :: k)
@@ -252,7 +252,7 @@ Definition mk_setcc_base (cond: extcond) (rd: ireg) (k: code) :=
       if ireg_eq rd EAX
       then Psetcc c1 EAX :: Psetcc c2 ECX :: Pand_rr EAX ECX :: k
       else Psetcc c1 EAX :: Psetcc c2 rd  :: Pand_rr rd EAX :: k
-  | Cond_or c1 c2 => 
+  | Cond_or c1 c2 =>
       if ireg_eq rd EAX
       then Psetcc c1 EAX :: Psetcc c2 ECX :: Por_rr EAX ECX :: k
       else Psetcc c1 EAX :: Psetcc c2 rd  :: Por_rr rd EAX :: k
@@ -282,10 +282,10 @@ Definition transl_op
       do r <- ireg_of res;
       OK ((if Int.eq_dec n Int.zero then Pxor_r r else Pmov_ri r n) :: k)
   | Ofloatconst f, nil =>
-      do r <- freg_of res; 
+      do r <- freg_of res;
       OK ((if Float.eq_dec f Float.zero then Pxorpd_f r else Pmovsd_fi r f) :: k)
   | Osingleconst f, nil =>
-      do r <- freg_of res; 
+      do r <- freg_of res;
       OK ((if Float32.eq_dec f Float32.zero then Pxorps_f r else Pmovss_fi r f) :: k)
   | Oindirectsymbol id, nil =>
       do r <- ireg_of res;
@@ -518,11 +518,11 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
   | Mcall sig (inr symb) =>
       OK (Pcall_s symb sig :: k)
   | Mtailcall sig (inl reg) =>
-      do r <- ireg_of reg; 
-      OK (Pfreeframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) :: 
+      do r <- ireg_of reg;
+      OK (Pfreeframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) ::
           Pjmp_r r sig :: k)
   | Mtailcall sig (inr symb) =>
-      OK (Pfreeframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) :: 
+      OK (Pfreeframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) ::
           Pjmp_s symb sig :: k)
   | Mlabel lbl =>
       OK(Plabel lbl :: k)
@@ -533,7 +533,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
   | Mjumptable arg tbl =>
       do r <- ireg_of arg; OK (Pjmptbl r tbl :: k)
   | Mreturn =>
-      OK (Pfreeframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) :: 
+      OK (Pfreeframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) ::
           Pret :: 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/ia32/Asmgenproof.v b/ia32/Asmgenproof.v
index d91e17a2..105347e7 100644
--- a/ia32/Asmgenproof.v
+++ b/ia32/Asmgenproof.v
@@ -43,17 +43,17 @@ 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 functions_translated:
@@ -70,15 +70,15 @@ Lemma functions_transl:
   Genv.find_funct_ptr tge fb = Some (Internal tf).
 Proof.
   intros. exploit functions_translated; eauto. intros [tf' [A B]].
-  monadInv B. rewrite H0 in EQ; inv EQ; auto. 
+  monadInv B. rewrite H0 in EQ; inv EQ; auto.
 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.
 
 (** * Properties of control flow *)
@@ -88,7 +88,7 @@ Lemma transf_function_no_overflow:
   transf_function f = OK tf -> list_length_z (fn_code tf) <= Int.max_unsigned.
 Proof.
   intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z (fn_code x))); monadInv EQ0.
-  omega. 
+  omega.
 Qed.
 
 Lemma exec_straight_exec:
@@ -100,7 +100,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:
@@ -110,8 +110,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 mk_mov_label:
   forall rd rs k c, mk_mov rd rs k = OK c -> tail_nolabel k c.
 Proof.
-  unfold mk_mov; intros. 
+  unfold mk_mov; intros.
   destruct rd; try discriminate; destruct rs; TailNoLabel.
 Qed.
 Hint Resolve mk_mov_label: labels.
@@ -154,20 +154,20 @@ Qed.
 Hint Resolve mk_shrximm_label: labels.
 
 Remark mk_intconv_label:
-  forall f r1 r2 k c, mk_intconv f r1 r2 k = OK c -> 
+  forall f r1 r2 k c, mk_intconv f r1 r2 k = OK c ->
   (forall r r', nolabel (f r r')) ->
   tail_nolabel k c.
 Proof.
-  unfold mk_intconv; intros. TailNoLabel. 
+  unfold mk_intconv; intros. TailNoLabel.
 Qed.
 Hint Resolve mk_intconv_label: labels.
 
 Remark mk_smallstore_label:
-  forall f addr r k c, mk_smallstore f addr r k = OK c -> 
+  forall f addr r k c, mk_smallstore f addr r k = OK c ->
   (forall r addr, nolabel (f r addr)) ->
   tail_nolabel k c.
 Proof.
-  unfold mk_smallstore; intros. TailNoLabel. 
+  unfold mk_smallstore; intros. TailNoLabel.
 Qed.
 Hint Resolve mk_smallstore_label: labels.
 
@@ -233,7 +233,7 @@ Proof.
   destruct (Int.eq_dec i Int.zero); TailNoLabel.
   destruct (Float.eq_dec f Float.zero); TailNoLabel.
   destruct (Float32.eq_dec f Float32.zero); TailNoLabel.
-  eapply tail_nolabel_trans. eapply transl_cond_label; eauto. eapply mk_setcc_label.  
+  eapply tail_nolabel_trans. eapply transl_cond_label; eauto. eapply mk_setcc_label.
 Qed.
 
 Remark transl_load_label:
@@ -262,13 +262,13 @@ Opaque loadind.
   eapply loadind_label; eauto.
   eapply storeind_label; eauto.
   eapply loadind_label; eauto.
-  eapply tail_nolabel_trans; eapply loadind_label; eauto. 
+  eapply tail_nolabel_trans; eapply loadind_label; eauto.
   eapply transl_op_label; eauto.
   eapply transl_load_label; eauto.
   eapply transl_store_label; eauto.
   destruct s0; TailNoLabel.
   destruct s0; TailNoLabel.
-  eapply tail_nolabel_trans. eapply transl_cond_label; eauto. eapply mk_jcc_label.  
+  eapply tail_nolabel_trans. eapply transl_cond_label; eauto. eapply mk_jcc_label.
 Qed.
 
 Lemma transl_instr_label':
@@ -277,7 +277,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.
 
@@ -292,7 +292,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.
@@ -307,7 +307,7 @@ Lemma transl_find_label:
   end.
 Proof.
   intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z (fn_code x))); inv EQ0.
-  monadInv EQ. simpl. eapply transl_code_label; eauto. rewrite transl_code'_transl_code in EQ0; eauto. 
+  monadInv EQ. simpl. eapply transl_code_label; eauto. rewrite transl_code'_transl_code in EQ0; eauto.
 Qed.
 
 End TRANSL_LABEL.
@@ -322,17 +322,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.
@@ -345,10 +345,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 (fn_code x))); inv EQ0.
   monadInv EQ. rewrite transl_code'_transl_code in EQ0.
   exists x; exists true; split; auto. unfold fn_code. repeat constructor.
@@ -417,10 +417,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.
 
@@ -445,15 +445,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.
@@ -487,8 +487,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 *)
@@ -504,88 +504,88 @@ 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. intros [rs' [P Q]].
   exists rs'; split. eauto.
-  split. eapply agree_undef_regs; eauto. 
+  split. eapply agree_undef_regs; eauto.
   simpl; intros. rewrite Q; auto with asmgen.
 Local Transparent destroyed_by_setstack.
   destruct ty; simpl; intuition congruence.
 
 - (* 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. 
+  left; eapply exec_straight_steps; eauto; intros.
   assert (DIFF: negb (mreg_eq dst DX) = true -> IR EDX <> preg_of dst).
-    intros. change (IR EDX) with (preg_of DX). red; intros. 
+    intros. change (IR EDX) with (preg_of DX). red; intros.
     unfold proj_sumbool in H1. destruct (mreg_eq dst DX); try discriminate.
     elim n. eapply preg_of_injective; eauto.
   destruct ep; simpl in TR.
 (* EDX contains parent *)
   exploit loadind_correct. eexact TR.
-  instantiate (2 := rs0). rewrite DXP; eauto.  
+  instantiate (2 := rs0). rewrite DXP; eauto.
   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.
   simpl; intros. rewrite R; auto.
 (* EDX does not contain parent *)
   monadInv TR.
   exploit loadind_correct. eexact EQ0. eauto. intros [rs1 [P [Q R]]]. simpl in Q.
   exploit loadind_correct. eexact EQ. instantiate (2 := rs1). rewrite Q. eauto.
-  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. congruence. auto.
   simpl; intros. rewrite U; 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]]]. 
+  exploit transl_op_correct; eauto. intros [rs2 [P [Q R]]].
   assert (S: Val.lessdef v (rs2 (preg_of res))) by (eapply Val.lessdef_trans; eauto).
   exists rs2; split. eauto.
   split. eapply agree_set_undef_mreg; eauto.
   simpl; congruence.
 
 - (* 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.
   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.  
+  split. eapply agree_undef_regs; eauto.
   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.
@@ -601,13 +601,13 @@ Opaque loadind.
   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. 
-  simpl. eauto. 
-  econstructor; eauto. 
+  eapply functions_transl; eauto. eapply find_instr_tail; eauto.
+  simpl. eauto.
+  econstructor; eauto.
   econstructor; eauto.
   eapply agree_sp_def; eauto.
   simpl. eapply agree_exten; eauto. intros. Simplifs.
-  Simplifs. rewrite <- H2. auto. 
+  Simplifs. 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).
@@ -615,9 +615,9 @@ Opaque loadind.
   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. Simplifs.
@@ -625,7 +625,7 @@ Opaque loadind.
 
 - (* Mtailcall *)
   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.
   rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *.
@@ -633,7 +633,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).
@@ -644,26 +644,26 @@ Opaque loadind.
   generalize (code_tail_next_int _ _ _ _ NOOV H8). intro CT1.
   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. rewrite C. rewrite A. rewrite <- (sp_val _ _ _ AG). rewrite E. eauto.
-  apply star_one. eapply exec_step_internal. 
+  apply star_one. eapply exec_step_internal.
   transitivity (Val.add rs0#PC Vone). auto. rewrite <- H4. 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.
   apply agree_set_other; auto. apply agree_nextinstr. apply agree_set_other; auto.
   eapply agree_change_sp; eauto. eapply parent_sp_def; eauto.
-  Simplifs. rewrite Pregmap.gso; auto. 
+  Simplifs. rewrite Pregmap.gso; auto.
   generalize (preg_of_not_SP rf). rewrite (ireg_of_eq _ _ EQ1). congruence.
 + (* Direct call *)
   generalize (code_tail_next_int _ _ _ _ NOOV H8). intro CT1.
   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. rewrite C. rewrite A. rewrite <- (sp_val _ _ _ AG). rewrite E. eauto.
-  apply star_one. eapply exec_step_internal. 
+  apply star_one. eapply exec_step_internal.
   transitivity (Val.add rs0#PC Vone). auto. rewrite <- H4. 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.
   apply agree_set_other; auto. apply agree_nextinstr. apply agree_set_other; auto.
@@ -671,16 +671,16 @@ Opaque loadind.
   rewrite Pregmap.gss. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. auto.
 
 - (* 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.
@@ -695,12 +695,12 @@ Opaque loadind.
   auto with asmgen.
   simpl; intros. intuition congruence.
   apply agree_nextinstr_nf. 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.
@@ -717,26 +717,26 @@ Opaque loadind.
   left; eapply exec_straight_steps_goto; eauto.
   intros. simpl in TR.
   destruct (transl_cond_correct tge tf cond args _ _ rs0 m' TR)
-  as [rs' [A [B C]]]. 
+  as [rs' [A [B C]]].
   rewrite EC in B.
   destruct (testcond_for_condition cond); simpl in *.
 (* simple jcc *)
   exists (Pjcc c1 lbl); exists k; exists rs'.
   split. eexact A.
-  split. eapply agree_exten; eauto. 
+  split. eapply agree_exten; eauto.
   simpl. rewrite B. auto.
 (* jcc; jcc *)
   destruct (eval_testcond c1 rs') as [b1|] eqn:TC1;
   destruct (eval_testcond c2 rs') as [b2|] eqn:TC2; inv B.
-  destruct b1.   
+  destruct b1.
   (* first jcc jumps *)
   exists (Pjcc c1 lbl); exists (Pjcc c2 lbl :: k); exists rs'.
   split. eexact A.
-  split. eapply agree_exten; eauto. 
+  split. eapply agree_exten; eauto.
   simpl. rewrite TC1. auto.
   (* second jcc jumps *)
   exists (Pjcc c2 lbl); exists k; exists (nextinstr rs').
-  split. eapply exec_straight_trans. eexact A. 
+  split. eapply exec_straight_trans. eexact A.
   eapply exec_straight_one. simpl. rewrite TC1. auto. auto.
   split. eapply agree_exten; eauto.
   intros; Simplifs.
@@ -745,23 +745,23 @@ Opaque loadind.
 (* jcc2 *)
   destruct (eval_testcond c1 rs') as [b1|] eqn:TC1;
   destruct (eval_testcond c2 rs') as [b2|] eqn:TC2; inv B.
-  destruct (andb_prop _ _ H3). subst. 
+  destruct (andb_prop _ _ H3). subst.
   exists (Pjcc2 c1 c2 lbl); exists k; exists rs'.
   split. eexact A.
-  split. eapply agree_exten; eauto. 
+  split. eapply agree_exten; eauto.
   simpl. rewrite TC1; rewrite TC2; auto.
 
 - (* Mcond false *)
   exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
-  left; eapply exec_straight_steps; eauto. intros. simpl in TR. 
+  left; eapply exec_straight_steps; eauto. intros. simpl in TR.
   destruct (transl_cond_correct tge tf cond args _ _ rs0 m' TR)
-  as [rs' [A [B C]]]. 
+  as [rs' [A [B C]]].
   rewrite EC in B.
   destruct (testcond_for_condition cond); simpl in *.
 (* simple jcc *)
   econstructor; split.
-  eapply exec_straight_trans. eexact A. 
-  apply exec_straight_one. simpl. rewrite B. eauto. auto. 
+  eapply exec_straight_trans. eexact A.
+  apply exec_straight_one. simpl. rewrite B. eauto. auto.
   split. apply agree_nextinstr. eapply agree_exten; eauto.
   simpl; congruence.
 (* jcc ; jcc *)
@@ -769,8 +769,8 @@ Opaque loadind.
   destruct (eval_testcond c2 rs') as [b2|] eqn:TC2; inv B.
   destruct (orb_false_elim _ _ H1); subst.
   econstructor; split.
-  eapply exec_straight_trans. eexact A. 
-  eapply exec_straight_two. simpl. rewrite TC1. eauto. auto. 
+  eapply exec_straight_trans. eexact A.
+  eapply exec_straight_two. simpl. rewrite TC1. eauto. auto.
   simpl. rewrite eval_testcond_nextinstr. rewrite TC2. eauto. auto. auto.
   split. apply agree_nextinstr. apply agree_nextinstr. eapply agree_exten; eauto.
   simpl; congruence.
@@ -778,9 +778,9 @@ Opaque loadind.
   destruct (eval_testcond c1 rs') as [b1|] eqn:TC1;
   destruct (eval_testcond c2 rs') as [b2|] eqn:TC2; inv B.
   exists (nextinstr rs'); split.
-  eapply exec_straight_trans. eexact A. 
-  apply exec_straight_one. simpl. 
-  rewrite TC1; rewrite TC2. 
+  eapply exec_straight_trans. eexact A.
+  apply exec_straight_one. simpl.
+  rewrite TC1; rewrite TC2.
   destruct b1. simpl in *. subst b2. auto. auto.
   auto.
   split. apply agree_nextinstr. eapply agree_exten; eauto.
@@ -788,41 +788,41 @@ Opaque loadind.
 
 - (* 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. 
+  exploit find_label_goto_label; 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. eauto.
-  econstructor; eauto. 
-Transparent destroyed_by_jumptable. 
+  econstructor; eauto.
+Transparent destroyed_by_jumptable.
   simpl. eapply agree_exten; eauto. intros. rewrite C; auto with asmgen.
   congruence.
 
 - (* Mreturn *)
   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.
   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.
   exploit code_tail_next_int; eauto. intro CT1.
   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. rewrite C. rewrite A. rewrite <- (sp_val _ _ _ AG). rewrite E. eauto.
-  apply star_one. eapply exec_step_internal. 
+  apply star_one. eapply exec_step_internal.
   transitivity (Val.add rs0#PC Vone). auto. rewrite <- H3. simpl. eauto.
-  eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
+  eapply functions_transl; eauto. eapply find_instr_tail; eauto.
   simpl. eauto. traceEq.
   constructor; auto.
   apply agree_set_other; auto. apply agree_nextinstr. apply agree_set_other; auto.
@@ -833,40 +833,40 @@ Transparent destroyed_by_jumptable.
   generalize EQ; intros EQ'. monadInv EQ'.
   destruct (zlt Int.max_unsigned (list_length_z (fn_code x0))); inv EQ1.
   monadInv EQ0. rewrite transl_code'_transl_code in 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]].
-  exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto. 
+  exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto.
   intros [m3' [P Q]].
   left; econstructor; split.
-  apply plus_one. econstructor; eauto. 
+  apply plus_one. econstructor; eauto.
   simpl. rewrite Int.unsigned_zero. simpl. eauto.
   simpl. rewrite C. simpl in F. rewrite (sp_val _ _ _ AG) in F. rewrite F.
   simpl in P. rewrite ATLR. rewrite P. eauto.
   econstructor; eauto.
-  unfold nextinstr. rewrite Pregmap.gss. repeat rewrite Pregmap.gso; auto with asmgen. 
+  unfold nextinstr. rewrite Pregmap.gss. repeat rewrite Pregmap.gso; auto with asmgen.
   rewrite ATPC. simpl. constructor; eauto.
-  unfold fn_code. eapply code_tail_next_int. simpl in g. omega. 
-  constructor. 
+  unfold fn_code. eapply code_tail_next_int. simpl in g. omega.
+  constructor.
   apply agree_nextinstr. eapply agree_change_sp; eauto.
 Transparent destroyed_at_function_entry.
   apply agree_undef_regs with rs0; eauto.
-  simpl; intros. apply Pregmap.gso; auto with asmgen. tauto. 
-  congruence. 
+  simpl; intros. apply Pregmap.gso; auto with asmgen. tauto.
+  congruence.
   intros. Simplifs. eapply agree_sp; eauto.
 
 - (* 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.
@@ -891,19 +891,19 @@ Proof.
   econstructor; eauto.
   constructor.
   apply Mem.extends_refl.
-  split. auto. simpl. unfold Vzero; congruence. intros. rewrite Regmap.gi. auto. 
+  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 _ _ _ AX AG). rewrite H2. intros LD; inv LD. auto.
 Qed.
 
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index 0ca343fb..d2a8206e 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -36,19 +36,19 @@ Lemma agree_nextinstr_nf:
   forall ms sp rs,
   agree ms sp rs -> agree ms sp (nextinstr_nf rs).
 Proof.
-  intros. unfold nextinstr_nf. apply agree_nextinstr. 
+  intros. unfold nextinstr_nf. apply agree_nextinstr.
   apply agree_undef_nondata_regs. auto.
-  intro. simpl. ElimOrEq; auto. 
+  intro. simpl. ElimOrEq; auto.
 Qed.
 
 (** Useful properties of the PC register. *)
 
 Lemma nextinstr_nf_inv:
-  forall r rs, 
+  forall r rs,
   match r with PC => False | CR _ => False | _ => True end ->
   (nextinstr_nf rs)#r = rs#r.
 Proof.
-  intros. unfold nextinstr_nf. rewrite nextinstr_inv. 
+  intros. unfold nextinstr_nf. rewrite nextinstr_inv.
   simpl. repeat rewrite Pregmap.gso; auto;
   red; intro; subst; contradiction.
   red; intro; subst; contradiction.
@@ -109,13 +109,13 @@ Lemma mk_mov_correct:
   /\ rs2#rd = rs1#rs
   /\ forall r, data_preg r = true -> r <> rd -> rs2#r = rs1#r.
 Proof.
-  unfold mk_mov; intros. 
+  unfold mk_mov; intros.
   destruct rd; try (monadInv H); destruct rs; monadInv H.
 (* mov *)
-  econstructor. split. apply exec_straight_one. simpl. eauto. auto. 
-  split. Simplifs. intros; Simplifs. 
+  econstructor. split. apply exec_straight_one. simpl. eauto. auto.
+  split. Simplifs. intros; Simplifs.
 (* movd *)
-  econstructor. split. apply exec_straight_one. simpl. eauto. auto. 
+  econstructor. split. apply exec_straight_one. simpl. eauto. auto.
   split. Simplifs. intros; Simplifs.
 Qed.
 
@@ -130,7 +130,7 @@ Remark divs_mods_exist:
   end.
 Proof.
   intros. unfold Val.divs, Val.mods. destruct v1; auto. destruct v2; auto.
-  destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); auto. 
+  destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); auto.
 Qed.
 
 Remark divu_modu_exist:
@@ -142,7 +142,7 @@ Remark divu_modu_exist:
   end.
 Proof.
   intros. unfold Val.divu, Val.modu. destruct v1; auto. destruct v2; auto.
-  destruct (Int.eq i0 Int.zero); auto. 
+  destruct (Int.eq i0 Int.zero); auto.
 Qed.
 
 (** Smart constructor for [shrx] *)
@@ -167,10 +167,10 @@ Proof.
   set (rs5 := nextinstr_nf (rs4#EAX <- (Val.shr rs4#EAX (Vint n)))).
   assert (rs3#EAX = Vint x). unfold rs3. Simplifs.
   assert (rs3#ECX = Vint x'). unfold rs3. Simplifs.
-  exists rs5. split. 
+  exists rs5. split.
   apply exec_straight_step with rs2 m. simpl. rewrite A. simpl. rewrite Int.and_idem. auto. auto.
-  apply exec_straight_step with rs3 m. simpl. 
-  change (rs2 EAX) with (rs1 EAX). rewrite A. simpl. 
+  apply exec_straight_step with rs3 m. simpl.
+  change (rs2 EAX) with (rs1 EAX). rewrite A. simpl.
   rewrite (Int.add_commut Int.zero tnm1). rewrite Int.add_zero. auto. auto.
   apply exec_straight_step with rs4 m. simpl.
   rewrite Int.lt_sub_overflow. unfold rs4. destruct (Int.lt x Int.zero); simpl; auto.
@@ -178,10 +178,10 @@ Proof.
   apply exec_straight_one. auto. auto.
   split. unfold rs5. Simplifs. unfold rs4. rewrite nextinstr_inv; auto with asmgen.
   destruct (Int.lt x Int.zero). rewrite Pregmap.gss. rewrite A; auto. rewrite A; rewrite H; auto.
-  intros. unfold rs5. Simplifs. unfold rs4. Simplifs. 
-  transitivity (rs3#r). destruct (Int.lt x Int.zero). Simplifs. auto. 
-  unfold rs3. Simplifs. unfold rs2. Simplifs.  
-  unfold compare_ints. Simplifs.  
+  intros. unfold rs5. Simplifs. unfold rs4. Simplifs.
+  transitivity (rs3#r). destruct (Int.lt x Int.zero). Simplifs. auto.
+  unfold rs3. Simplifs. unfold rs2. Simplifs.
+  unfold compare_ints. Simplifs.
 Qed.
 
 (** Smart constructor for integer conversions *)
@@ -197,11 +197,11 @@ Lemma mk_intconv_correct:
   /\ forall r, data_preg r = true -> r <> rd -> r <> EAX -> rs2#r = rs1#r.
 Proof.
   unfold mk_intconv; intros. destruct (low_ireg rs); monadInv H.
-  econstructor. split. apply exec_straight_one. rewrite H0. eauto. auto. 
+  econstructor. split. apply exec_straight_one. rewrite H0. eauto. auto.
+  split. Simplifs. intros. Simplifs.
+  econstructor. split. eapply exec_straight_two.
+  simpl. eauto. apply H0. auto. auto.
   split. Simplifs. intros. Simplifs.
-  econstructor. split. eapply exec_straight_two. 
-  simpl. eauto. apply H0. auto. auto. 
-  split. Simplifs. intros. Simplifs.  
 Qed.
 
 (** Smart constructor for small stores *)
@@ -228,40 +228,40 @@ Lemma mk_smallstore_correct:
      exec_straight ge fn c rs1 m1 k rs2 m2
   /\ forall r, data_preg r = true -> r <> EAX /\ r <> ECX -> rs2#r = rs1#r.
 Proof.
-  unfold mk_smallstore; intros. 
+  unfold mk_smallstore; intros.
   remember (low_ireg r) as low. destruct low.
 (* low reg *)
-  monadInv H. econstructor; split. apply exec_straight_one. rewrite H1. 
+  monadInv H. econstructor; split. apply exec_straight_one. rewrite H1.
   unfold exec_store. rewrite H0. eauto. auto.
   intros; Simplifs.
 (* high reg *)
    remember (addressing_mentions addr EAX) as mentions. destruct mentions; monadInv H.
 (* EAX is mentioned. *)
-  assert (r <> ECX). red; intros; subst r; discriminate. 
+  assert (r <> ECX). red; intros; subst r; discriminate.
   set (rs2 := nextinstr (rs1#ECX <- (eval_addrmode ge addr rs1))).
   set (rs3 := nextinstr (rs2#EAX <- (rs1 r))).
   econstructor; split.
-  apply exec_straight_three with rs2 m1 rs3 m1. 
-  simpl. auto. 
-  simpl. replace (rs2 r) with (rs1 r). auto. symmetry. unfold rs2; Simplifs. 
-  rewrite H1. unfold exec_store. simpl. rewrite Int.add_zero. 
+  apply exec_straight_three with rs2 m1 rs3 m1.
+  simpl. auto.
+  simpl. replace (rs2 r) with (rs1 r). auto. symmetry. unfold rs2; Simplifs.
+  rewrite H1. unfold exec_store. simpl. rewrite Int.add_zero.
   change (rs3 EAX) with (rs1 r).
   change (rs3 ECX) with (eval_addrmode ge addr rs1).
   replace (Val.add (eval_addrmode ge addr rs1) (Vint Int.zero))
      with (eval_addrmode ge addr rs1).
   rewrite H0. eauto.
   destruct (eval_addrmode ge addr rs1); simpl in H0; try discriminate.
-  simpl. rewrite Int.add_zero; auto. 
-  auto. auto. auto. 
-  intros. destruct H3. Simplifs. unfold rs3; Simplifs. unfold rs2; Simplifs. 
+  simpl. rewrite Int.add_zero; auto.
+  auto. auto. auto.
+  intros. destruct H3. Simplifs. unfold rs3; Simplifs. unfold rs2; Simplifs.
 (* EAX is not mentioned *)
   set (rs2 := nextinstr (rs1#EAX <- (rs1 r))).
   econstructor; split.
   apply exec_straight_two with rs2 m1.
   simpl. auto.
-  rewrite H1. unfold exec_store. 
+  rewrite H1. unfold exec_store.
   rewrite (addressing_mentions_correct addr EAX rs2 rs1); auto.
-  change (rs2 EAX) with (rs1 r). rewrite H0. eauto. 
+  change (rs2 EAX) with (rs1 r). rewrite H0. eauto.
   intros. unfold rs2; Simplifs.
   auto. auto.
   intros. destruct H2. simpl. Simplifs. unfold rs2; Simplifs.
@@ -281,7 +281,7 @@ Proof.
   unfold loadind; intros.
   set (addr := Addrmode (Some base) None (inl (ident * int) ofs)) in *.
   assert (eval_addrmode ge addr rs = Val.add rs#base (Vint ofs)).
-    unfold addr. simpl. rewrite Int.add_commut; rewrite Int.add_zero; auto. 
+    unfold addr. simpl. rewrite Int.add_commut; rewrite Int.add_zero; auto.
   exists (nextinstr_nf (rs#(preg_of dst) <- v)); split.
 - destruct ty; try discriminate; destruct (preg_of dst); inv H; simpl in H0;
   apply exec_straight_one; auto; simpl; unfold exec_load; rewrite H1, H0; auto.
@@ -300,7 +300,7 @@ Local Transparent destroyed_by_setstack.
   unfold storeind; intros.
   set (addr := Addrmode (Some base) None (inl (ident * int) ofs)) in *.
   assert (eval_addrmode ge addr rs = Val.add rs#base (Vint ofs)).
-    unfold addr. simpl. rewrite Int.add_commut; rewrite Int.add_zero; auto. 
+    unfold addr. simpl. rewrite Int.add_commut; rewrite Int.add_zero; auto.
   destruct ty; try discriminate; destruct (preg_of src); inv H; simpl in H0;
   (econstructor; split;
   [apply exec_straight_one; [simpl; unfold exec_store; rewrite H1, H0; eauto|auto]
@@ -315,10 +315,10 @@ Lemma transl_addressing_mode_correct:
   eval_addressing ge (rs ESP) addr (List.map rs (List.map preg_of args)) = Some v ->
   Val.lessdef v (eval_addrmode ge am rs).
 Proof.
-  assert (A: forall n, Int.add Int.zero n = n). 
+  assert (A: forall n, Int.add Int.zero n = n).
     intros. rewrite Int.add_commut. apply Int.add_zero.
   assert (B: forall n i, (if Int.eq i Int.one then Vint n else Vint (Int.mul n i)) = Vint (Int.mul n i)).
-    intros. predSpec Int.eq Int.eq_spec i Int.one. 
+    intros. predSpec Int.eq Int.eq_spec i Int.one.
     subst i. rewrite Int.mul_one. auto. auto.
   assert (C: forall v i,
     Val.lessdef (Val.mul v (Vint i))
@@ -332,22 +332,22 @@ Proof.
   monadInv H. rewrite (ireg_of_eq _ _ EQ). simpl. rewrite A; auto.
 (* indexed2 *)
   monadInv H. rewrite (ireg_of_eq _ _ EQ); rewrite (ireg_of_eq _ _ EQ1). simpl.
-  rewrite Val.add_assoc; auto. 
+  rewrite Val.add_assoc; auto.
 (* scaled *)
-  monadInv H. rewrite (ireg_of_eq _ _ EQ). unfold eval_addrmode. 
-  rewrite Val.add_permut. simpl. rewrite A. apply Val.add_lessdef; auto. 
+  monadInv H. rewrite (ireg_of_eq _ _ EQ). unfold eval_addrmode.
+  rewrite Val.add_permut. simpl. rewrite A. apply Val.add_lessdef; auto.
 (* indexed2scaled *)
   monadInv H. rewrite (ireg_of_eq _ _ EQ); rewrite (ireg_of_eq _ _ EQ1); simpl.
-  apply Val.add_lessdef; auto. apply Val.add_lessdef; auto. 
+  apply Val.add_lessdef; auto. apply Val.add_lessdef; auto.
 (* global *)
   inv H. simpl. unfold Genv.symbol_address.
   destruct (Genv.find_symbol ge i); simpl; auto. repeat rewrite Int.add_zero. auto.
 (* based *)
   monadInv H. rewrite (ireg_of_eq _ _ EQ). simpl.
   unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); simpl; auto.
-  rewrite Int.add_zero. rewrite Val.add_commut. auto. 
+  rewrite Int.add_zero. rewrite Val.add_commut. auto.
 (* basedscaled *)
-  monadInv H. rewrite (ireg_of_eq _ _ EQ). unfold eval_addrmode. 
+  monadInv H. rewrite (ireg_of_eq _ _ EQ). unfold eval_addrmode.
   rewrite (Val.add_commut Vzero). rewrite Val.add_assoc. rewrite Val.add_permut.
   apply Val.add_lessdef; auto. destruct (rs x); simpl; auto. rewrite B. simpl.
   rewrite Int.add_zero. auto.
@@ -367,7 +367,7 @@ Lemma compare_ints_spec:
   /\ (forall r, data_preg r = true -> rs'#r = rs#r).
 Proof.
   intros. unfold rs'; unfold compare_ints.
-  split. auto. 
+  split. auto.
   split. auto.
   split. auto.
   split. auto.
@@ -377,13 +377,13 @@ Qed.
 Lemma int_signed_eq:
   forall x y, Int.eq x y = zeq (Int.signed x) (Int.signed y).
 Proof.
-  intros. unfold Int.eq. unfold proj_sumbool. 
+  intros. unfold Int.eq. unfold proj_sumbool.
   destruct (zeq (Int.unsigned x) (Int.unsigned y));
   destruct (zeq (Int.signed x) (Int.signed y)); auto.
   elim n. unfold Int.signed. rewrite e; auto.
-  elim n. apply Int.eqm_small_eq; auto with ints. 
+  elim n. apply Int.eqm_small_eq; auto with ints.
   eapply Int.eqm_trans. apply Int.eqm_sym. apply Int.eqm_signed_unsigned.
-  rewrite e. apply Int.eqm_signed_unsigned. 
+  rewrite e. apply Int.eqm_signed_unsigned.
 Qed.
 
 Lemma int_not_lt:
@@ -392,8 +392,8 @@ Proof.
   intros. unfold Int.lt. rewrite int_signed_eq. unfold proj_sumbool.
   destruct (zlt (Int.signed y) (Int.signed x)).
   rewrite zlt_false. rewrite zeq_false. auto. omega. omega.
-  destruct (zeq (Int.signed x) (Int.signed y)). 
-  rewrite zlt_false. auto. omega. 
+  destruct (zeq (Int.signed x) (Int.signed y)).
+  rewrite zlt_false. auto. omega.
   rewrite zlt_true. auto. omega.
 Qed.
 
@@ -409,8 +409,8 @@ Proof.
   intros. unfold Int.ltu, Int.eq.
   destruct (zlt (Int.unsigned y) (Int.unsigned x)).
   rewrite zlt_false. rewrite zeq_false. auto. omega. omega.
-  destruct (zeq (Int.unsigned x) (Int.unsigned y)). 
-  rewrite zlt_false. auto. omega. 
+  destruct (zeq (Int.unsigned x) (Int.unsigned y)).
+  rewrite zlt_false. auto. omega.
   rewrite zlt_true. auto. omega.
 Qed.
 
@@ -465,16 +465,16 @@ Proof.
   destruct (Int.eq i Int.zero &&
     (Mem.valid_pointer m b0 (Int.unsigned i0) || Mem.valid_pointer m b0 (Int.unsigned i0 - 1))) eqn:?; try discriminate.
   destruct c; simpl in *; inv H1.
-  rewrite Heqb1; reflexivity. 
+  rewrite Heqb1; reflexivity.
   rewrite Heqb1; reflexivity.
 (* ptr int *)
   destruct (Int.eq i0 Int.zero &&
     (Mem.valid_pointer m b0 (Int.unsigned i) || Mem.valid_pointer m b0 (Int.unsigned i - 1))) eqn:?; try discriminate.
   destruct c; simpl in *; inv H1.
-  rewrite Heqb1; reflexivity. 
+  rewrite Heqb1; reflexivity.
   rewrite Heqb1; reflexivity.
 (* ptr ptr *)
-  simpl. 
+  simpl.
   fold (Mem.weak_valid_pointer m b0 (Int.unsigned i)) in *.
   fold (Mem.weak_valid_pointer m b1 (Int.unsigned i0)) in *.
   destruct (eq_block b0 b1).
@@ -501,7 +501,7 @@ Lemma compare_floats_spec:
   /\ (forall r, data_preg r = true -> rs'#r = rs#r).
 Proof.
   intros. unfold rs'; unfold compare_floats.
-  split. auto. 
+  split. auto.
   split. auto.
   split. auto.
   intros. Simplifs.
@@ -516,7 +516,7 @@ Lemma compare_floats32_spec:
   /\ (forall r, data_preg r = true -> rs'#r = rs#r).
 Proof.
   intros. unfold rs'; unfold compare_floats32.
-  split. auto. 
+  split. auto.
   split. auto.
   split. auto.
   intros. Simplifs.
@@ -574,19 +574,19 @@ Proof.
   simpl.
   rewrite Float.cmp_ne_eq. rewrite Float.cmp_le_lt_eq.
   caseEq (Float.cmp Clt n1 n2); intros; simpl.
-  caseEq (Float.cmp Ceq n1 n2); intros; simpl. 
-  elimtype False. eapply Float.cmp_lt_eq_false; eauto. 
-  auto. 
+  caseEq (Float.cmp Ceq n1 n2); intros; simpl.
+  elimtype False. eapply Float.cmp_lt_eq_false; eauto.
+  auto.
   destruct (Float.cmp Ceq n1 n2); auto.
 (* le *)
   rewrite <- (Float.cmp_swap Cge n1 n2). simpl.
   destruct (Float.cmp Cle n1 n2); auto.
 (* gt *)
-  rewrite Float.cmp_ne_eq. rewrite Float.cmp_ge_gt_eq. 
+  rewrite Float.cmp_ne_eq. rewrite Float.cmp_ge_gt_eq.
   caseEq (Float.cmp Cgt n1 n2); intros; simpl.
-  caseEq (Float.cmp Ceq n1 n2); intros; simpl. 
-  elimtype False. eapply Float.cmp_gt_eq_false; eauto. 
-  auto. 
+  caseEq (Float.cmp Ceq n1 n2); intros; simpl.
+  elimtype False. eapply Float.cmp_gt_eq_false; eauto.
+  auto.
   destruct (Float.cmp Ceq n1 n2); auto.
 (* ge *)
   destruct (Float.cmp Cge n1 n2); auto.
@@ -622,19 +622,19 @@ Proof.
   simpl.
   rewrite Float.cmp_ne_eq. rewrite Float.cmp_le_lt_eq.
   caseEq (Float.cmp Clt n1 n2); intros; simpl.
-  caseEq (Float.cmp Ceq n1 n2); intros; simpl. 
+  caseEq (Float.cmp Ceq n1 n2); intros; simpl.
   elimtype False. eapply Float.cmp_lt_eq_false; eauto.
-  auto. 
+  auto.
   destruct (Float.cmp Ceq n1 n2); auto.
 (* le *)
   rewrite <- (Float.cmp_swap Cge n1 n2). simpl.
   destruct (Float.cmp Cle n1 n2); auto.
 (* gt *)
-  rewrite Float.cmp_ne_eq. rewrite Float.cmp_ge_gt_eq. 
+  rewrite Float.cmp_ne_eq. rewrite Float.cmp_ge_gt_eq.
   caseEq (Float.cmp Cgt n1 n2); intros; simpl.
-  caseEq (Float.cmp Ceq n1 n2); intros; simpl. 
-  elimtype False. eapply Float.cmp_gt_eq_false; eauto. 
-  auto. 
+  caseEq (Float.cmp Ceq n1 n2); intros; simpl.
+  elimtype False. eapply Float.cmp_gt_eq_false; eauto.
+  auto.
   destruct (Float.cmp Ceq n1 n2); auto.
 (* ge *)
   destruct (Float.cmp Cge n1 n2); auto.
@@ -670,19 +670,19 @@ Proof.
   simpl.
   rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_le_lt_eq.
   caseEq (Float32.cmp Clt n1 n2); intros; simpl.
-  caseEq (Float32.cmp Ceq n1 n2); intros; simpl. 
-  elimtype False. eapply Float32.cmp_lt_eq_false; eauto. 
-  auto. 
+  caseEq (Float32.cmp Ceq n1 n2); intros; simpl.
+  elimtype False. eapply Float32.cmp_lt_eq_false; eauto.
+  auto.
   destruct (Float32.cmp Ceq n1 n2); auto.
 (* le *)
   rewrite <- (Float32.cmp_swap Cge n1 n2). simpl.
   destruct (Float32.cmp Cle n1 n2); auto.
 (* gt *)
-  rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_ge_gt_eq. 
+  rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_ge_gt_eq.
   caseEq (Float32.cmp Cgt n1 n2); intros; simpl.
-  caseEq (Float32.cmp Ceq n1 n2); intros; simpl. 
-  elimtype False. eapply Float32.cmp_gt_eq_false; eauto. 
-  auto. 
+  caseEq (Float32.cmp Ceq n1 n2); intros; simpl.
+  elimtype False. eapply Float32.cmp_gt_eq_false; eauto.
+  auto.
   destruct (Float32.cmp Ceq n1 n2); auto.
 (* ge *)
   destruct (Float32.cmp Cge n1 n2); auto.
@@ -718,19 +718,19 @@ Proof.
   simpl.
   rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_le_lt_eq.
   caseEq (Float32.cmp Clt n1 n2); intros; simpl.
-  caseEq (Float32.cmp Ceq n1 n2); intros; simpl. 
+  caseEq (Float32.cmp Ceq n1 n2); intros; simpl.
   elimtype False. eapply Float32.cmp_lt_eq_false; eauto.
-  auto. 
+  auto.
   destruct (Float32.cmp Ceq n1 n2); auto.
 (* le *)
   rewrite <- (Float32.cmp_swap Cge n1 n2). simpl.
   destruct (Float32.cmp Cle n1 n2); auto.
 (* gt *)
-  rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_ge_gt_eq. 
+  rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_ge_gt_eq.
   caseEq (Float32.cmp Cgt n1 n2); intros; simpl.
-  caseEq (Float32.cmp Ceq n1 n2); intros; simpl. 
-  elimtype False. eapply Float32.cmp_gt_eq_false; eauto. 
-  auto. 
+  caseEq (Float32.cmp Ceq n1 n2); intros; simpl.
+  elimtype False. eapply Float32.cmp_gt_eq_false; eauto.
+  auto.
   destruct (Float32.cmp Ceq n1 n2); auto.
 (* ge *)
   destruct (Float32.cmp Cge n1 n2); auto.
@@ -739,7 +739,7 @@ Qed.
 Remark swap_floats_commut:
   forall (A B: Type) c (f: A -> B) x y, swap_floats c (f x) (f y) = f (swap_floats c x y).
 Proof.
-  intros. destruct c; auto. 
+  intros. destruct c; auto.
 Qed.
 
 Remark compare_floats_inv:
@@ -747,10 +747,10 @@ Remark compare_floats_inv:
   r <> CR ZF -> r <> CR CF -> r <> CR PF -> r <> CR SF -> r <> CR OF ->
   compare_floats vx vy rs r = rs r.
 Proof.
-  intros. 
+  intros.
   assert (DFL: undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil) rs r = rs r).
-    simpl. Simplifs. 
-  unfold compare_floats; destruct vx; destruct vy; auto. Simplifs. 
+    simpl. Simplifs.
+  unfold compare_floats; destruct vx; destruct vy; auto. Simplifs.
 Qed.
 
 Remark compare_floats32_inv:
@@ -758,10 +758,10 @@ Remark compare_floats32_inv:
   r <> CR ZF -> r <> CR CF -> r <> CR PF -> r <> CR SF -> r <> CR OF ->
   compare_floats32 vx vy rs r = rs r.
 Proof.
-  intros. 
+  intros.
   assert (DFL: undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil) rs r = rs r).
-    simpl. Simplifs. 
-  unfold compare_floats32; destruct vx; destruct vy; auto. Simplifs. 
+    simpl. Simplifs.
+  unfold compare_floats32; destruct vx; destruct vy; auto. Simplifs.
 Qed.
 
 Lemma transl_cond_correct:
@@ -775,83 +775,83 @@ Lemma transl_cond_correct:
      end
   /\ forall r, data_preg r = true -> rs'#r = rs r.
 Proof.
-  unfold transl_cond; intros. 
+  unfold transl_cond; intros.
   destruct cond; repeat (destruct args; try discriminate); monadInv H.
 (* comp *)
   simpl. rewrite (ireg_of_eq _ _ EQ). rewrite (ireg_of_eq _ _ EQ1).
   econstructor. split. apply exec_straight_one. simpl. eauto. auto.
   split. destruct (Val.cmp_bool c0 (rs x) (rs x0)) eqn:?; auto.
-  eapply testcond_for_signed_comparison_correct; eauto. 
+  eapply testcond_for_signed_comparison_correct; eauto.
   intros. unfold compare_ints. Simplifs.
 (* compu *)
   simpl. rewrite (ireg_of_eq _ _ EQ). rewrite (ireg_of_eq _ _ EQ1).
   econstructor. split. apply exec_straight_one. simpl. eauto. auto.
   split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (rs x0)) eqn:?; auto.
-  eapply testcond_for_unsigned_comparison_correct; eauto. 
+  eapply testcond_for_unsigned_comparison_correct; eauto.
   intros. unfold compare_ints. Simplifs.
 (* compimm *)
   simpl. rewrite (ireg_of_eq _ _ EQ). destruct (Int.eq_dec i Int.zero).
-  econstructor; split. apply exec_straight_one. simpl; eauto. auto. 
+  econstructor; split. apply exec_straight_one. simpl; eauto. auto.
   split. destruct (rs x); simpl; auto. subst. rewrite Int.and_idem.
-  eapply testcond_for_signed_comparison_correct; eauto. 
+  eapply testcond_for_signed_comparison_correct; eauto.
   intros. unfold compare_ints. Simplifs.
-  econstructor; split. apply exec_straight_one. simpl; eauto. auto. 
+  econstructor; split. apply exec_straight_one. simpl; eauto. auto.
   split. destruct (Val.cmp_bool c0 (rs x) (Vint i)) eqn:?; auto.
-  eapply testcond_for_signed_comparison_correct; eauto. 
+  eapply testcond_for_signed_comparison_correct; eauto.
   intros. unfold compare_ints. Simplifs.
 (* compuimm *)
   simpl. rewrite (ireg_of_eq _ _ EQ).
   econstructor. split. apply exec_straight_one. simpl. eauto. auto.
   split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (Vint i)) eqn:?; auto.
-  eapply testcond_for_unsigned_comparison_correct; eauto. 
+  eapply testcond_for_unsigned_comparison_correct; eauto.
   intros. unfold compare_ints. Simplifs.
 (* compf *)
   simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1).
   exists (nextinstr (compare_floats (swap_floats c0 (rs x) (rs x0)) (swap_floats c0 (rs x0) (rs x)) rs)).
-  split. apply exec_straight_one. 
+  split. apply exec_straight_one.
   destruct c0; simpl; auto.
-  unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats_inv; auto with asmgen. 
+  unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats_inv; auto with asmgen.
   split. destruct (rs x); destruct (rs x0); simpl; auto.
   repeat rewrite swap_floats_commut. apply testcond_for_float_comparison_correct.
-  intros. Simplifs. apply compare_floats_inv; auto with asmgen. 
+  intros. Simplifs. apply compare_floats_inv; auto with asmgen.
 (* notcompf *)
   simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1).
   exists (nextinstr (compare_floats (swap_floats c0 (rs x) (rs x0)) (swap_floats c0 (rs x0) (rs x)) rs)).
-  split. apply exec_straight_one. 
+  split. apply exec_straight_one.
   destruct c0; simpl; auto.
-  unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats_inv; auto with asmgen. 
+  unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats_inv; auto with asmgen.
   split. destruct (rs x); destruct (rs x0); simpl; auto.
   repeat rewrite swap_floats_commut. apply testcond_for_neg_float_comparison_correct.
-  intros. Simplifs. apply compare_floats_inv; auto with asmgen. 
+  intros. Simplifs. apply compare_floats_inv; auto with asmgen.
 (* compfs *)
   simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1).
   exists (nextinstr (compare_floats32 (swap_floats c0 (rs x) (rs x0)) (swap_floats c0 (rs x0) (rs x)) rs)).
-  split. apply exec_straight_one. 
+  split. apply exec_straight_one.
   destruct c0; simpl; auto.
-  unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats32_inv; auto with asmgen. 
+  unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats32_inv; auto with asmgen.
   split. destruct (rs x); destruct (rs x0); simpl; auto.
   repeat rewrite swap_floats_commut. apply testcond_for_float32_comparison_correct.
-  intros. Simplifs. apply compare_floats32_inv; auto with asmgen. 
+  intros. Simplifs. apply compare_floats32_inv; auto with asmgen.
 (* notcompfs *)
   simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1).
   exists (nextinstr (compare_floats32 (swap_floats c0 (rs x) (rs x0)) (swap_floats c0 (rs x0) (rs x)) rs)).
-  split. apply exec_straight_one. 
+  split. apply exec_straight_one.
   destruct c0; simpl; auto.
-  unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats32_inv; auto with asmgen. 
+  unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats32_inv; auto with asmgen.
   split. destruct (rs x); destruct (rs x0); simpl; auto.
   repeat rewrite swap_floats_commut. apply testcond_for_neg_float32_comparison_correct.
-  intros. Simplifs. apply compare_floats32_inv; auto with asmgen. 
+  intros. Simplifs. apply compare_floats32_inv; auto with asmgen.
 (* maskzero *)
   simpl. rewrite (ireg_of_eq _ _ EQ).
   econstructor. split. apply exec_straight_one. simpl; eauto. auto.
-  split. destruct (rs x); simpl; auto. 
+  split. destruct (rs x); simpl; auto.
   generalize (compare_ints_spec rs (Vint (Int.and i0 i)) Vzero m).
   intros [A B]. rewrite A. unfold Val.cmpu; simpl. destruct (Int.eq (Int.and i0 i) Int.zero); auto.
   intros. unfold compare_ints. Simplifs.
 (* masknotzero *)
   simpl. rewrite (ireg_of_eq _ _ EQ).
   econstructor. split. apply exec_straight_one. simpl; eauto. auto.
-  split. destruct (rs x); simpl; auto. 
+  split. destruct (rs x); simpl; auto.
   generalize (compare_ints_spec rs (Vint (Int.and i0 i)) Vzero m).
   intros [A B]. rewrite A. unfold Val.cmpu; simpl. destruct (Int.eq (Int.and i0 i) Int.zero); auto.
   intros. unfold compare_ints. Simplifs.
@@ -879,8 +879,8 @@ Proof.
   intros. destruct cond; simpl in *.
 - (* base *)
   econstructor; split.
-  apply exec_straight_one. simpl; eauto. auto. 
-  split. Simplifs. intros; Simplifs. 
+  apply exec_straight_one. simpl; eauto. auto.
+  split. Simplifs. intros; Simplifs.
 - (* or *)
   assert (Val.of_optbool
     match eval_testcond c1 rs1 with
@@ -892,7 +892,7 @@ Proof.
     | None => None
     end =
     Val.or (Val.of_optbool (eval_testcond c1 rs1)) (Val.of_optbool (eval_testcond c2 rs1))).
-  destruct (eval_testcond c1 rs1). destruct (eval_testcond c2 rs1). 
+  destruct (eval_testcond c1 rs1). destruct (eval_testcond c2 rs1).
   destruct b; destruct b0; auto.
   destruct b; auto.
   auto.
@@ -908,11 +908,11 @@ Proof.
   econstructor; split.
   eapply exec_straight_three.
   simpl; eauto.
-  simpl. rewrite eval_testcond_nextinstr. repeat rewrite eval_testcond_set_ireg. eauto. 
-  simpl. eauto. 
+  simpl. rewrite eval_testcond_nextinstr. repeat rewrite eval_testcond_set_ireg. eauto.
+  simpl. eauto.
   auto. auto. auto.
   split. Simplifs. rewrite Val.or_commut. decEq; Simplifs.
-  intros. destruct H0; Simplifs. 
+  intros. destruct H0; Simplifs.
 - (* and *)
   assert (Val.of_optbool
     match eval_testcond c1 rs1 with
@@ -925,7 +925,7 @@ Proof.
     end =
     Val.and (Val.of_optbool (eval_testcond c1 rs1)) (Val.of_optbool (eval_testcond c2 rs1))).
   {
-    destruct (eval_testcond c1 rs1). destruct (eval_testcond c2 rs1). 
+    destruct (eval_testcond c1 rs1). destruct (eval_testcond c2 rs1).
     destruct b; destruct b0; auto.
     destruct b; auto.
     auto.
@@ -942,11 +942,11 @@ Proof.
   econstructor; split.
   eapply exec_straight_three.
   simpl; eauto.
-  simpl. rewrite eval_testcond_nextinstr. repeat rewrite eval_testcond_set_ireg. eauto. 
-  simpl. eauto. 
+  simpl. rewrite eval_testcond_nextinstr. repeat rewrite eval_testcond_set_ireg. eauto.
+  simpl. eauto.
   auto. auto. auto.
   split. Simplifs. rewrite Val.and_commut. decEq; Simplifs.
-  intros. destruct H0; Simplifs. 
+  intros. destruct H0; Simplifs.
 Qed.
 
 Lemma mk_setcc_correct:
@@ -959,10 +959,10 @@ Proof.
   intros. unfold mk_setcc. destruct (low_ireg rd).
 - apply mk_setcc_base_correct.
 - exploit mk_setcc_base_correct. intros [rs2 [A [B C]]].
-  econstructor; split. eapply exec_straight_trans. eexact A. apply exec_straight_one. 
+  econstructor; split. eapply exec_straight_trans. eexact A. apply exec_straight_one.
     simpl. eauto. simpl. auto.
-  intuition Simplifs. 
-Qed. 
+  intuition Simplifs.
+Qed.
 
 (** Translation of arithmetic operations. *)
 
@@ -980,7 +980,7 @@ Ltac ArgsInv :=
 
 Ltac TranslOp :=
   econstructor; split;
-  [ apply exec_straight_one; [ simpl; eauto | auto ] 
+  [ apply exec_straight_one; [ simpl; eauto | auto ]
   | split; [ Simplifs | intros; Simplifs ]].
 
 Lemma transl_op_correct:
@@ -1005,12 +1005,12 @@ Transparent destroyed_by_op.
   /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r).
   {
     intros [rs' [A [B C]]]. subst v. exists rs'; auto.
-  } 
+  }
 
   destruct op; simpl in TR; ArgsInv; simpl in EV; try (inv EV); try (apply SAME; TranslOp; fail).
 (* move *)
-  exploit mk_mov_correct; eauto. intros [rs2 [A [B C]]]. 
-  apply SAME. exists rs2. eauto. 
+  exploit mk_mov_correct; eauto. intros [rs2 [A [B C]]].
+  apply SAME. exists rs2. eauto.
 (* intconst *)
   apply SAME. destruct (Int.eq_dec i Int.zero). subst i. TranslOp. TranslOp.
 (* floatconst *)
@@ -1020,39 +1020,39 @@ Transparent destroyed_by_op.
 (* cast8signed *)
   apply SAME. eapply mk_intconv_correct; eauto.
 (* cast8unsigned *)
-  apply SAME. eapply mk_intconv_correct; eauto. 
+  apply SAME. eapply mk_intconv_correct; eauto.
 (* cast16signed *)
   apply SAME. eapply mk_intconv_correct; eauto.
 (* cast16unsigned *)
   apply SAME. eapply mk_intconv_correct; eauto.
 (* mulhs *)
-  apply SAME. TranslOp. destruct H1. Simplifs. 
+  apply SAME. TranslOp. destruct H1. Simplifs.
 (* mulhu *)
-  apply SAME. TranslOp. destruct H1. Simplifs. 
+  apply SAME. TranslOp. destruct H1. Simplifs.
 (* div *)
   apply SAME.
-  specialize (divs_mods_exist (rs EAX) (rs ECX)). rewrite H0. 
+  specialize (divs_mods_exist (rs EAX) (rs ECX)). rewrite H0.
   destruct (Val.mods (rs EAX) (rs ECX)) as [vr|] eqn:?; intros; try contradiction.
   TranslOp. change (rs#EDX<-Vundef ECX) with (rs#ECX). rewrite H0; rewrite Heqo. eauto.
   auto. auto.
   simpl in H3. destruct H3; Simplifs.
 (* divu *)
   apply SAME.
-  specialize (divu_modu_exist (rs EAX) (rs ECX)). rewrite H0. 
+  specialize (divu_modu_exist (rs EAX) (rs ECX)). rewrite H0.
   destruct (Val.modu (rs EAX) (rs ECX)) as [vr|] eqn:?; intros; try contradiction.
   TranslOp. change (rs#EDX<-Vundef ECX) with (rs#ECX). rewrite H0; rewrite Heqo. eauto.
   auto. auto.
   simpl in H3. destruct H3; Simplifs.
 (* mod *)
   apply SAME.
-  specialize (divs_mods_exist (rs EAX) (rs ECX)). rewrite H0. 
+  specialize (divs_mods_exist (rs EAX) (rs ECX)). rewrite H0.
   destruct (Val.divs (rs EAX) (rs ECX)) as [vr|] eqn:?; intros; try contradiction.
   TranslOp. change (rs#EDX<-Vundef ECX) with (rs#ECX). rewrite H0; rewrite Heqo. eauto.
   auto. auto.
   simpl in H3. destruct H3; Simplifs.
 (* modu *)
   apply SAME.
-  specialize (divu_modu_exist (rs EAX) (rs ECX)). rewrite H0. 
+  specialize (divu_modu_exist (rs EAX) (rs ECX)). rewrite H0.
   destruct (Val.divu (rs EAX) (rs ECX)) as [vr|] eqn:?; intros; try contradiction.
   TranslOp. change (rs#EDX<-Vundef ECX) with (rs#ECX). rewrite H0; rewrite Heqo. eauto.
   auto. auto.
@@ -1093,7 +1093,7 @@ Lemma transl_load_correct:
   /\ rs'#(preg_of dest) = v
   /\ forall r, data_preg r = true -> r <> preg_of dest -> rs'#r = rs#r.
 Proof.
-  unfold transl_load; intros. monadInv H. 
+  unfold transl_load; intros. monadInv H.
   exploit transl_addressing_mode_correct; eauto. intro EA.
   assert (EA': eval_addrmode ge x rs = a). destruct a; simpl in H1; try discriminate; inv EA; auto.
   set (rs2 := nextinstr_nf (rs#(preg_of dest) <- v)).
@@ -1102,10 +1102,10 @@ Proof.
   assert (rs2 PC = Val.add (rs PC) Vone).
     transitivity (Val.add ((rs#(preg_of dest) <- v) PC) Vone).
     auto. decEq. apply Pregmap.gso; auto with asmgen.
-  exists rs2. split. 
+  exists rs2. split.
   destruct chunk; ArgsInv; apply exec_straight_one; auto.
   split. unfold rs2. rewrite nextinstr_nf_inv1. Simplifs. apply preg_of_data.
-  intros. unfold rs2. Simplifs. 
+  intros. unfold rs2. Simplifs.
 Qed.
 
 Lemma transl_store_correct:
@@ -1117,7 +1117,7 @@ Lemma transl_store_correct:
      exec_straight ge fn c rs m k rs' m'
   /\ forall r, data_preg r = true -> preg_notin r (destroyed_by_store chunk addr) -> rs'#r = rs#r.
 Proof.
-  unfold transl_store; intros. monadInv H. 
+  unfold transl_store; intros. monadInv H.
   exploit transl_addressing_mode_correct; eauto. intro EA.
   assert (EA': eval_addrmode ge x rs = a). destruct a; simpl in H1; try discriminate; inv EA; auto.
   rewrite <- EA' in H1. destruct chunk; ArgsInv.
@@ -1129,7 +1129,7 @@ Proof.
   eapply mk_smallstore_correct; eauto.
 (* int16signed *)
   econstructor; split.
-  apply exec_straight_one. simpl. unfold exec_store. 
+  apply exec_straight_one. simpl. unfold exec_store.
   replace (Mem.storev Mint16unsigned m (eval_addrmode ge x rs) (rs x0))
      with (Mem.storev Mint16signed m (eval_addrmode ge x rs) (rs x0)).
   rewrite H1. eauto.
diff --git a/ia32/CBuiltins.ml b/ia32/CBuiltins.ml
index b1be612b..125e71d5 100644
--- a/ia32/CBuiltins.ml
+++ b/ia32/CBuiltins.ml
@@ -41,19 +41,19 @@ let builtins = {
     "__builtin_fmin",
       (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false);
     "__builtin_fmadd",
-      (TFloat(FDouble, []), 
+      (TFloat(FDouble, []),
        [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])],
        false);
     "__builtin_fmsub",
-      (TFloat(FDouble, []), 
+      (TFloat(FDouble, []),
        [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])],
        false);
     "__builtin_fnmadd",
-      (TFloat(FDouble, []), 
+      (TFloat(FDouble, []),
        [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])],
        false);
     "__builtin_fnmsub",
-      (TFloat(FDouble, []), 
+      (TFloat(FDouble, []),
        [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])],
        false);
     (* Memory accesses *)
diff --git a/ia32/CombineOp.v b/ia32/CombineOp.v
index ca54ba1b..cdd16071 100644
--- a/ia32/CombineOp.v
+++ b/ia32/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.
diff --git a/ia32/CombineOpproof.v b/ia32/CombineOpproof.v
index 1e5b9321..8f600054 100644
--- a/ia32/CombineOpproof.v
+++ b/ia32/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.
@@ -34,7 +34,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 :=
@@ -42,7 +42,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) ->
@@ -51,11 +51,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:
@@ -67,10 +67,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:
@@ -81,7 +81,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.
 
@@ -93,7 +93,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.
@@ -129,7 +129,7 @@ Theorem combine_addr_sound:
 Proof.
   intros. functional inversion H; subst.
   (* indexed - lea *)
-  UseGetSound. simpl. eapply eval_offset_addressing_total; eauto. 
+  UseGetSound. simpl. eapply eval_offset_addressing_total; eauto.
 Qed.
 
 Theorem combine_op_sound:
@@ -139,7 +139,7 @@ Theorem combine_op_sound:
 Proof.
   intros. functional inversion H; subst.
 (* lea-lea *)
-  simpl. eapply combine_addr_sound; eauto. 
+  simpl. eapply combine_addr_sound; eauto.
 (* andimm - andimm *)
   UseGetSound; simpl. rewrite <- H0. rewrite Val.and_assoc. auto.
 (* orimm - orimm *)
diff --git a/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v
index 47a6c536..3dfb8ccf 100644
--- a/ia32/ConstpropOpproof.v
+++ b/ia32/ConstpropOpproof.v
@@ -48,7 +48,7 @@ Lemma match_G:
   forall r id ofs,
   AE.get r ae = Ptr(Gl id ofs) -> Val.lessdef e#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:
@@ -60,9 +60,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.
@@ -83,11 +83,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.
@@ -120,35 +120,35 @@ Proof.
 - rewrite Genv.shift_symbol_address. econstructor; split. eauto. apply Val.add_lessdef; auto.
 - econstructor; split; eauto. rewrite Int.add_zero_l.
   change (Vptr sp (Int.add n ofs)) with (Val.add (Vptr sp n) (Vint ofs)). apply Val.add_lessdef; auto.
-- econstructor; split; eauto. rewrite Int.add_assoc. rewrite Genv.shift_symbol_address. 
+- econstructor; split; eauto. rewrite Int.add_assoc. rewrite Genv.shift_symbol_address.
   rewrite Val.add_assoc. apply Val.add_lessdef; auto.
 - econstructor; split; eauto.
   fold (Val.add (Vint n1) e#r2). rewrite (Val.add_commut (Vint n1)).
   rewrite Genv.shift_symbol_address. apply Val.add_lessdef; auto.
-  rewrite Int.add_commut. rewrite Genv.shift_symbol_address. apply Val.add_lessdef; auto. 
-- econstructor; split; eauto. rewrite Int.add_zero_l. rewrite Int.add_assoc. 
+  rewrite Int.add_commut. rewrite Genv.shift_symbol_address. apply Val.add_lessdef; auto.
+- econstructor; split; eauto. rewrite Int.add_zero_l. rewrite Int.add_assoc.
   change (Vptr sp (Int.add n1 (Int.add n2 ofs)))
     with (Val.add (Vptr sp n1) (Vint (Int.add n2 ofs))).
-  rewrite Val.add_assoc. apply Val.add_lessdef; auto. 
-- econstructor; split; eauto. rewrite Int.add_zero_l. 
-  fold (Val.add (Vint n1) e#r2). rewrite (Int.add_commut n1). 
+  rewrite Val.add_assoc. apply Val.add_lessdef; auto.
+- econstructor; split; eauto. rewrite Int.add_zero_l.
+  fold (Val.add (Vint n1) e#r2). rewrite (Int.add_commut n1).
   change (Vptr sp (Int.add (Int.add n2 n1) ofs))
     with (Val.add (Val.add (Vint n1) (Vptr sp n2)) (Vint ofs)).
-  apply Val.add_lessdef; auto. apply Val.add_lessdef; auto. 
-- econstructor; split; eauto. rewrite Genv.shift_symbol_address. 
-  rewrite ! Val.add_assoc. apply Val.add_lessdef; auto. 
-  rewrite Val.add_commut. apply Val.add_lessdef; auto. 
+  apply Val.add_lessdef; auto. apply Val.add_lessdef; auto.
+- econstructor; split; eauto. rewrite Genv.shift_symbol_address.
+  rewrite ! Val.add_assoc. apply Val.add_lessdef; auto.
+  rewrite Val.add_commut. apply Val.add_lessdef; auto.
 - econstructor; split; eauto. rewrite Genv.shift_symbol_address.
   rewrite (Val.add_commut e#r1). rewrite ! Val.add_assoc.
   apply Val.add_lessdef; auto. rewrite Val.add_commut. apply Val.add_lessdef; auto.
-- fold (Val.add (Vint n1) e#r2). econstructor; split; eauto. 
-  rewrite (Val.add_commut (Vint n1)). rewrite Val.add_assoc. 
-  apply Val.add_lessdef; eauto. 
+- fold (Val.add (Vint n1) e#r2). econstructor; split; eauto.
+  rewrite (Val.add_commut (Vint n1)). rewrite Val.add_assoc.
+  apply Val.add_lessdef; eauto.
 - econstructor; split; eauto.  rewrite ! Val.add_assoc.
-  apply Val.add_lessdef; eauto. 
-- econstructor; split; eauto. rewrite Int.add_assoc. 
-  rewrite Genv.shift_symbol_address. apply Val.add_lessdef; auto. 
-- econstructor; split; eauto. 
+  apply Val.add_lessdef; eauto.
+- econstructor; split; eauto. rewrite Int.add_assoc.
+  rewrite Genv.shift_symbol_address. apply Val.add_lessdef; auto.
+- econstructor; split; eauto.
   rewrite Genv.shift_symbol_address. rewrite ! Val.add_assoc. apply Val.add_lessdef; auto.
   rewrite Val.add_commut; auto.
 - econstructor; split; eauto.
@@ -161,20 +161,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' e##args' m = Some v 
+  exists v, eval_operation ge (Vptr sp Int.zero) op' e##args' m = Some v
          /\ Val.lessdef (Val.of_optbool (eval_condition c e##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' e##args' m = Some v 
+  exists v, eval_operation ge (Vptr sp Int.zero) op' e##args' m = Some v
          /\ Val.lessdef (Val.of_optbool (eval_condition c e##args m)) v.
 Proof.
   intros c args vl.
@@ -183,20 +183,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 (e#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 e#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 (e#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 e#r1 (Vint Int.one)); split; auto. simpl.
   exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
   apply make_cmp_base_correct; auto.
@@ -209,11 +209,11 @@ Lemma make_addimm_correct:
   exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.add e#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 (e#r); split; auto. destruct (e#r); simpl; auto; rewrite Int.add_zero; auto.
   exists (Val.add e#r (Vint n)); auto.
 Qed.
-  
+
 Lemma make_shlimm_correct:
   forall n r1 r2,
   e#r2 = Vint n ->
@@ -223,7 +223,7 @@ Proof.
   intros; unfold make_shlimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
   exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.shl_zero. auto.
-  destruct (Int.ltu n Int.iwordsize). 
+  destruct (Int.ltu n Int.iwordsize).
   econstructor; split. simpl. eauto. auto.
   econstructor; split. simpl. eauto. rewrite H; auto.
 Qed.
@@ -237,7 +237,7 @@ Proof.
   intros; unfold make_shrimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
   exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.shr_zero. auto.
-  destruct (Int.ltu n Int.iwordsize). 
+  destruct (Int.ltu n Int.iwordsize).
   econstructor; split. simpl. eauto. auto.
   econstructor; split. simpl. eauto. rewrite H; auto.
 Qed.
@@ -251,7 +251,7 @@ Proof.
   intros; unfold make_shruimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
   exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.shru_zero. auto.
-  destruct (Int.ltu n Int.iwordsize). 
+  destruct (Int.ltu n Int.iwordsize).
   econstructor; split. simpl. eauto. auto.
   econstructor; split. simpl. eauto. rewrite H; auto.
 Qed.
@@ -268,7 +268,7 @@ Proof.
   exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.mul_one; auto.
   destruct (Int.is_power2 n) eqn:?; intros.
   rewrite (Val.mul_pow2 e#r1 _ _ Heqo). econstructor; split. simpl; eauto. auto.
-  econstructor; split; eauto. auto. 
+  econstructor; split; eauto. auto.
 Qed.
 
 Lemma make_divimm_correct:
@@ -281,7 +281,7 @@ Proof.
   intros; unfold make_divimm.
   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.
@@ -295,7 +295,7 @@ Lemma make_divuimm_correct:
 Proof.
   intros; unfold make_divuimm.
   destruct (Int.is_power2 n) eqn:?.
-  econstructor; split. simpl; eauto. 
+  econstructor; split. simpl; eauto.
   rewrite H0 in H. erewrite Val.divu_pow2 by eauto. auto.
   exists v; auto.
 Qed.
@@ -326,17 +326,17 @@ Proof.
   subst n. exists (e#r); split; auto. destruct (e#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 (e#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:
@@ -349,7 +349,7 @@ Proof.
   subst n. exists (e#r); split; auto. destruct (e#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 (e#r); simpl; auto. rewrite Int.or_mone; auto.
-  econstructor; split; eauto. auto. 
+  econstructor; split; eauto. auto.
 Qed.
 
 Lemma make_xorimm_correct:
@@ -361,8 +361,8 @@ Proof.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
   subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int.xor_zero; auto.
   predSpec Int.eq Int.eq_spec n Int.mone; intros.
-  subst n. exists (Val.notint e#r); split; auto. 
-  econstructor; split; eauto. auto. 
+  subst n. exists (Val.notint e#r); split; auto.
+  econstructor; split; eauto. auto.
 Qed.
 
 Lemma make_mulfimm_correct:
@@ -371,11 +371,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 e##args m = Some v /\ Val.lessdef (Val.mulf e#r1 e#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 (e#r1); simpl; auto. rewrite Float.mul2_add; auto. 
-  simpl. econstructor; split; eauto. 
+  destruct (e#r1); simpl; auto. rewrite Float.mul2_add; auto.
+  simpl. econstructor; split; eauto.
 Qed.
 
 Lemma make_mulfimm_correct_2:
@@ -384,12 +384,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 e##args m = Some v /\ Val.lessdef (Val.mulf e#r1 e#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 (e#r2); simpl; auto. rewrite Float.mul2_add; auto. 
-  rewrite Float.mul_commut; auto. 
-  simpl. econstructor; split; eauto. 
+  destruct (e#r2); simpl; auto. rewrite Float.mul2_add; auto.
+  rewrite Float.mul_commut; auto.
+  simpl. econstructor; split; eauto.
 Qed.
 
 Lemma make_mulfsimm_correct:
@@ -398,11 +398,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 e##args m = Some v /\ Val.lessdef (Val.mulfs e#r1 e#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 (e#r1); simpl; auto. rewrite Float32.mul2_add; auto. 
-  simpl. econstructor; split; eauto. 
+  destruct (e#r1); simpl; auto. rewrite Float32.mul2_add; auto.
+  simpl. econstructor; split; eauto.
 Qed.
 
 Lemma make_mulfsimm_correct_2:
@@ -411,12 +411,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 e##args m = Some v /\ Val.lessdef (Val.mulfs e#r1 e#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 (e#r2); simpl; auto. rewrite Float32.mul2_add; auto. 
-  rewrite Float32.mul_commut; auto. 
-  simpl. econstructor; split; eauto. 
+  destruct (e#r2); simpl; auto. rewrite Float32.mul2_add; auto.
+  rewrite Float32.mul_commut; auto.
+  simpl. econstructor; split; eauto.
 Qed.
 
 Lemma make_cast8signed_correct:
@@ -425,8 +425,8 @@ Lemma make_cast8signed_correct:
   let (op, args) := make_cast8signed r x in
   exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.sign_ext 8 e#r) v.
 Proof.
-  intros; unfold make_cast8signed. destruct (vincl x (Sgn Ptop 8)) eqn:INCL. 
-  exists e#r; split; auto. 
+  intros; unfold make_cast8signed. destruct (vincl x (Sgn Ptop 8)) eqn:INCL.
+  exists e#r; split; auto.
   assert (V: vmatch bc e#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.
@@ -439,8 +439,8 @@ Lemma make_cast8unsigned_correct:
   let (op, args) := make_cast8unsigned r x in
   exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.zero_ext 8 e#r) v.
 Proof.
-  intros; unfold make_cast8unsigned. destruct (vincl x (Uns Ptop 8)) eqn:INCL. 
-  exists e#r; split; auto. 
+  intros; unfold make_cast8unsigned. destruct (vincl x (Uns Ptop 8)) eqn:INCL.
+  exists e#r; split; auto.
   assert (V: vmatch bc e#r (Uns Ptop 8)).
   { eapply vmatch_ge; eauto. apply vincl_ge; auto. }
   inv V; simpl; auto. rewrite is_uns_zero_ext in H4 by auto. rewrite H4; auto.
@@ -453,8 +453,8 @@ Lemma make_cast16signed_correct:
   let (op, args) := make_cast16signed r x in
   exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.sign_ext 16 e#r) v.
 Proof.
-  intros; unfold make_cast16signed. destruct (vincl x (Sgn Ptop 16)) eqn:INCL. 
-  exists e#r; split; auto. 
+  intros; unfold make_cast16signed. destruct (vincl x (Sgn Ptop 16)) eqn:INCL.
+  exists e#r; split; auto.
   assert (V: vmatch bc e#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.
@@ -467,8 +467,8 @@ Lemma make_cast16unsigned_correct:
   let (op, args) := make_cast16unsigned r x in
   exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.zero_ext 16 e#r) v.
 Proof.
-  intros; unfold make_cast16unsigned. destruct (vincl x (Uns Ptop 16)) eqn:INCL. 
-  exists e#r; split; auto. 
+  intros; unfold make_cast16unsigned. destruct (vincl x (Uns Ptop 16)) eqn:INCL.
+  exists e#r; split; auto.
   assert (V: vmatch bc e#r (Uns Ptop 16)).
   { eapply vmatch_ge; eauto. apply vincl_ge; auto. }
   inv V; simpl; auto. rewrite is_uns_zero_ext in H4 by auto. rewrite H4; auto.
@@ -493,17 +493,17 @@ Proof.
 (* cast16unsigned *)
   InvApproxRegs; SimplVM; inv H0. apply make_cast16unsigned_correct; auto.
 (* sub *)
-  InvApproxRegs; SimplVM; inv H0. rewrite Val.sub_add_opp. apply make_addimm_correct; auto. 
+  InvApproxRegs; SimplVM; inv H0. rewrite Val.sub_add_opp. apply make_addimm_correct; auto.
 (* mul *)
   rewrite Val.mul_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_mulimm_correct; auto.
   InvApproxRegs; SimplVM; inv H0. apply make_mulimm_correct; auto.
-(* divs *) 
+(* divs *)
   assert (e#r2 = Vint n2). clear H0. InvApproxRegs; SimplVM; auto.
   apply make_divimm_correct; auto.
-(* divu *) 
+(* divu *)
   assert (e#r2 = Vint n2). clear H0. InvApproxRegs; SimplVM; auto.
   apply make_divuimm_correct; auto.
-(* modu *) 
+(* modu *)
   assert (e#r2 = Vint n2). clear H0. InvApproxRegs; SimplVM; auto.
   apply make_moduimm_correct; auto.
 (* and *)
@@ -523,7 +523,7 @@ Proof.
 (* shru *)
   InvApproxRegs; SimplVM; inv H0. apply make_shruimm_correct; auto.
 (* lea *)
-  exploit addr_strength_reduction_correct; eauto. 
+  exploit addr_strength_reduction_correct; eauto.
   destruct (addr_strength_reduction addr args0 vl0) as [addr' args'].
   auto.
 (* cond *)
diff --git a/ia32/Conventions1.v b/ia32/Conventions1.v
index ef9ab6b9..11420d48 100644
--- a/ia32/Conventions1.v
+++ b/ia32/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.
@@ -106,19 +106,19 @@ 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 ->
@@ -138,24 +138,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.
@@ -198,9 +198,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.
 
@@ -282,7 +282,7 @@ Fixpoint size_arguments_rec
 Definition size_arguments (s: signature) : Z :=
   size_arguments_rec s.(sig_args) 0.
 
-(** 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 :=
@@ -302,7 +302,7 @@ Remark loc_arguments_rec_charact:
 Proof.
   induction tyl; simpl loc_arguments_rec; intros.
 - destruct H.
-- assert (REC: forall ofs1, In l (loc_arguments_rec tyl ofs1) -> ofs1 > ofs -> 
+- assert (REC: forall ofs1, In l (loc_arguments_rec tyl ofs1) -> ofs1 > ofs ->
                match l with
                | R _ => False
                | S Local _ _ => False
@@ -320,7 +320,7 @@ Lemma loc_arguments_acceptable:
   In l (loc_arguments s) -> loc_argument_acceptable l.
 Proof.
   unfold loc_arguments; intros.
-  exploit loc_arguments_rec_charact; eauto. 
+  exploit loc_arguments_rec_charact; eauto.
   unfold loc_argument_acceptable.
   destruct l; tauto.
 Qed.
@@ -334,14 +334,14 @@ Remark size_arguments_rec_above:
 Proof.
   induction tyl; simpl; intros.
   omega.
-  apply Zle_trans with (ofs0 + typesize a); auto. 
+  apply Zle_trans with (ofs0 + typesize a); auto.
   generalize (typesize_pos a); omega.
 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.
 
diff --git a/ia32/Machregs.v b/ia32/Machregs.v
index f3801900..34eb0ac8 100644
--- a/ia32/Machregs.v
+++ b/ia32/Machregs.v
@@ -32,7 +32,7 @@ Inductive mreg: Type :=
   (** Allocatable integer regs *)
   | AX: mreg | BX: mreg | CX: mreg | DX: mreg | SI: mreg | DI: mreg | BP: mreg
   (** Allocatable float regs *)
-  | X0: mreg | X1: mreg | X2: mreg | X3: mreg 
+  | X0: mreg | X1: mreg | X2: mreg | X3: mreg
   | X4: mreg | X5: mreg | X6: mreg | X7: mreg
   (** Special float reg *)
   | FP0: mreg (**r top of x87 FP stack *).
diff --git a/ia32/NeedOp.v b/ia32/NeedOp.v
index 52b9fcbe..07eec160 100644
--- a/ia32/NeedOp.v
+++ b/ia32/NeedOp.v
@@ -116,7 +116,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.
@@ -132,8 +132,8 @@ Proof.
   unfold needs_of_addressing; intros.
   destruct addr; simpl in *; FuncInv; InvAgree; TrivialExists;
   auto using add_sound, mul_sound with na.
-  apply add_sound; auto with na. apply add_sound; rewrite modarith_idem; auto. 
-  apply add_sound; auto. apply add_sound; rewrite modarith_idem; auto with na. 
+  apply add_sound; auto with na. apply add_sound; rewrite modarith_idem; auto.
+  apply add_sound; auto. apply add_sound; rewrite modarith_idem; auto with na.
   apply mul_sound; rewrite modarith_idem; auto with na.
 Qed.
 
@@ -148,9 +148,9 @@ 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 zero_ext_sound; auto. omega.
-- apply sign_ext_sound; auto. compute; auto. 
+- apply sign_ext_sound; auto. compute; auto.
 - apply zero_ext_sound; auto. omega.
 - apply neg_sound; auto.
 - apply mul_sound; auto.
@@ -164,10 +164,10 @@ Proof.
 - apply notint_sound; auto.
 - apply shlimm_sound; auto.
 - apply shrimm_sound; auto.
-- apply shruimm_sound; auto. 
-- apply ror_sound; auto. 
+- apply shruimm_sound; auto.
+- apply ror_sound; auto.
 - eapply needs_of_addressing_sound; eauto.
-- destruct (eval_condition c args m) as [b|] eqn:EC; simpl in H2. 
+- 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.
@@ -185,7 +185,7 @@ Proof.
 - apply zero_ext_redundant_sound; auto. omega.
 - apply sign_ext_redundant_sound; auto. omega.
 - apply zero_ext_redundant_sound; auto. omega.
-- apply andimm_redundant_sound; auto. 
+- apply andimm_redundant_sound; auto.
 - apply orimm_redundant_sound; auto.
 Qed.
 
diff --git a/ia32/Op.v b/ia32/Op.v
index 33f30aa5..e6df3f2d 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -17,7 +17,7 @@
 - [operation]: arithmetic and logical operations;
 - [addressing]: addressing modes for load and store operations.
 
-  These types are IA32-specific and correspond roughly to what the 
+  These types are IA32-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
@@ -49,7 +49,7 @@ Inductive condition : Type :=
   | Cmaskzero: int -> condition         (**r test [(arg & constant) == 0] *)
   | Cmasknotzero: int -> condition.     (**r test [(arg & constant) != 0] *)
 
-(** Addressing modes.  [r1], [r2], etc, are the arguments to the 
+(** Addressing modes.  [r1], [r2], etc, are the arguments to the
   addressing. *)
 
 Inductive addressing: Type :=
@@ -475,7 +475,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.
@@ -499,7 +499,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.
 
@@ -529,9 +529,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) as [[]|]; auto.
-  repeat (destruct vl; auto). 
+  repeat (destruct vl; auto).
   repeat (destruct vl; auto). destruct (Val.cmpfs_bool c v v0) as [[]|]; auto.
   destruct vl; auto. destruct vl; auto.
   destruct vl; auto. destruct vl; auto. destruct (Val.maskzero_bool v i) as [[]|]; auto.
@@ -554,13 +554,13 @@ 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:
   forall delta op, type_of_operation (shift_stack_operation delta op) = type_of_operation op.
 Proof.
-  intros. destruct op; auto. simpl. decEq. apply type_shift_stack_addressing. 
+  intros. destruct op; auto. simpl. decEq. apply type_shift_stack_addressing.
 Qed.
 
 Lemma eval_shift_stack_addressing:
@@ -578,7 +578,7 @@ Lemma eval_shift_stack_operation:
   eval_operation ge (Val.add sp (Vint delta)) op vl m.
 Proof.
   intros. destruct op; simpl; auto.
-  apply eval_shift_stack_addressing. 
+  apply eval_shift_stack_addressing.
 Qed.
 
 (** Offset an addressing mode [addr] by a quantity [delta], so that
@@ -613,12 +613,12 @@ Proof.
   rewrite !Val.add_assoc; auto.
   rewrite !Val.add_assoc; auto.
   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. 
+  unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto.
+  rewrite Val.add_assoc. rewrite Val.add_permut. rewrite Val.add_commut. auto.
   unfold Genv.symbol_address. destruct (Genv.find_symbol ge i0); auto.
-  rewrite Val.add_assoc. rewrite Val.add_permut. rewrite Val.add_commut. auto. 
-  rewrite Val.add_assoc. auto. 
+  rewrite Val.add_assoc. rewrite Val.add_permut. rewrite Val.add_commut. auto.
+  rewrite Val.add_assoc. auto.
 Qed.
 
 Lemma eval_offset_addressing:
@@ -627,7 +627,7 @@ Lemma eval_offset_addressing:
   eval_addressing ge sp addr args = Some v ->
   eval_addressing ge sp addr' args = Some(Val.add v (Vint delta)).
 Proof.
-  intros. unfold offset_addressing in H; inv H. 
+  intros. unfold offset_addressing in H; inv H.
   eapply eval_offset_addressing_total; eauto.
 Qed.
 
@@ -832,9 +832,9 @@ Proof.
   inv H4; simpl; auto.
   inv H4; simpl; auto.
   inv H4; 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; inv H2; simpl; auto.
   inv H4; simpl; auto.
@@ -842,11 +842,11 @@ Proof.
   inv H4; inv H2; simpl; auto.
   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 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.
@@ -859,14 +859,14 @@ Proof.
   inv H4; simpl; auto. destruct (Int.ltu i Int.iwordsize); auto.
   inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto.
   inv H4; simpl; auto. destruct (Int.ltu i Int.iwordsize); auto.
-  inv H4; simpl in H1; try discriminate. simpl. 
+  inv H4; simpl in H1; try discriminate. simpl.
   destruct (Int.ltu i (Int.repr 31)); inv H1. TrivialExists.
   inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto.
   inv H4; simpl; auto. destruct (Int.ltu i Int.iwordsize); auto.
   inv H4; simpl; auto. destruct (Int.ltu i Int.iwordsize); auto.
   inv H4; simpl; auto. destruct (Int.ltu i Int.iwordsize); auto.
   inv H2; simpl; auto. destruct (Int.ltu (Int.sub Int.iwordsize i) Int.iwordsize); auto.
-  eapply eval_addressing_inj; eauto. 
+  eapply eval_addressing_inj; eauto.
   inv H4; simpl; auto.
   inv H4; simpl; auto.
   inv H4; inv H2; simpl; auto.
@@ -912,7 +912,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:
@@ -922,7 +922,7 @@ Remark weak_valid_pointer_extends:
   Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
   Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
 Proof.
-  intros. inv H0. rewrite Int.add_zero. eapply Mem.weak_valid_pointer_extends; eauto. 
+  intros. inv H0. rewrite Int.add_zero. eapply Mem.weak_valid_pointer_extends; eauto.
 Qed.
 
 Remark weak_valid_pointer_no_overflow_extends:
@@ -978,11 +978,11 @@ Proof.
   apply weak_valid_pointer_extends; auto.
   apply weak_valid_pointer_no_overflow_extends.
   apply valid_different_pointers_extends; auto.
-  intros. apply val_inject_lessdef. auto. 
+  intros. apply val_inject_lessdef. auto.
   apply val_inject_lessdef; auto.
-  eauto. 
+  eauto.
   auto.
-  destruct H2 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. 
+  destruct H2 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto.
 Qed.
 
 Lemma eval_addressing_lessdef:
@@ -998,8 +998,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.
@@ -1021,7 +1021,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.
 
@@ -1043,11 +1043,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.
@@ -1062,14 +1062,14 @@ 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.
   intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
   intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
   intros; eapply Mem.different_pointers_inject; eauto.
-  intros. apply symbol_address_inject. 
+  intros. apply symbol_address_inject.
 Qed.
 
 End EVAL_INJECT.
diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v
index d40ec7af..bcfc13c9 100644
--- a/ia32/SelectOpproof.v
+++ b/ia32/SelectOpproof.v
@@ -30,7 +30,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.
 
@@ -119,9 +119,9 @@ Proof.
   destruct (symbol_is_external id).
   predSpec Int.eq Int.eq_spec ofs Int.zero.
   subst. EvalOp.
-  EvalOp. econstructor. EvalOp. simpl; eauto. econstructor. simpl. 
-  unfold Genv.symbol_address. destruct (Genv.find_symbol ge id); auto. 
-  simpl. rewrite Int.add_commut. rewrite Int.add_zero. auto. 
+  EvalOp. econstructor. EvalOp. simpl; eauto. econstructor. simpl.
+  unfold Genv.symbol_address. destruct (Genv.find_symbol ge id); auto.
+  simpl. rewrite Int.add_commut. rewrite Int.add_zero. auto.
   EvalOp.
 Qed.
 
@@ -130,7 +130,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.
 
@@ -147,12 +147,12 @@ 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.
   inv H0. simpl in H6. TrivialExists. simpl. eapply eval_offset_addressing_total; eauto.
-  TrivialExists. 
+  TrivialExists.
 Qed.
 
 Theorem eval_add: binary_constructor_sound add Val.add.
@@ -164,11 +164,11 @@ Proof.
   subst. TrivialExists. simpl. rewrite Val.add_permut_4. auto.
   subst. TrivialExists. simpl. rewrite Val.add_assoc. decEq; decEq. rewrite Val.add_permut. auto.
   subst. TrivialExists. simpl. rewrite Val.add_permut_4. rewrite <- Val.add_permut. rewrite <- Val.add_assoc. auto.
-  subst. TrivialExists. simpl. rewrite Genv.shift_symbol_address. 
+  subst. TrivialExists. simpl. rewrite Genv.shift_symbol_address.
     rewrite Val.add_commut. rewrite Val.add_assoc. decEq. decEq. apply Val.add_commut.
   subst. TrivialExists. simpl. rewrite Genv.shift_symbol_address. rewrite Val.add_assoc.
     decEq; decEq. apply Val.add_commut.
-  subst. TrivialExists. simpl. rewrite Genv.shift_symbol_address. rewrite Val.add_commut. 
+  subst. TrivialExists. simpl. rewrite Genv.shift_symbol_address. rewrite Val.add_commut.
     rewrite Val.add_assoc. decEq; decEq. apply Val.add_commut.
   subst. TrivialExists. simpl. rewrite Genv.shift_symbol_address.
     rewrite Val.add_assoc. decEq; decEq. apply Val.add_commut.
@@ -185,7 +185,7 @@ Proof.
   red; intros until y.
   unfold sub; case (sub_match a b); intros; InvEval.
   rewrite Val.sub_add_opp. apply eval_addimm; 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.
@@ -197,7 +197,7 @@ Theorem eval_negint: unary_constructor_sound negint (fun v => Val.sub Vzero v).
 Proof.
   red; intros until x. unfold negint. case (negint_match a); intros; InvEval.
   TrivialExists.
-  TrivialExists. 
+  TrivialExists.
 Qed.
 
 Theorem eval_shlimm:
@@ -209,28 +209,28 @@ Proof.
   intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shl_zero; auto.
   destruct (Int.ltu n Int.iwordsize) eqn:LT; simpl.
   destruct (shlimm_match a); intros; InvEval.
-  exists (Vint (Int.shl n1 n)); split. EvalOp. 
+  exists (Vint (Int.shl n1 n)); split. EvalOp.
   simpl. rewrite LT. auto.
   destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?.
   exists (Val.shl v1 (Vint (Int.add n n1))); split. EvalOp.
-  subst. destruct v1; simpl; auto. 
+  subst. destruct v1; simpl; auto.
   rewrite Heqb.
   destruct (Int.ltu n1 Int.iwordsize) eqn:?; simpl; auto.
   destruct (Int.ltu n Int.iwordsize) eqn:?; simpl; auto.
   rewrite Int.add_commut. rewrite Int.shl_shl; auto. rewrite Int.add_commut; auto.
-  subst. TrivialExists. econstructor. EvalOp. simpl; eauto. constructor. 
+  subst. TrivialExists. econstructor. EvalOp. simpl; eauto. constructor.
   simpl. auto.
   subst. destruct (shift_is_scale n).
   econstructor; split. EvalOp. simpl. eauto.
-  destruct v1; simpl; auto. rewrite LT. 
+  destruct v1; simpl; auto. rewrite LT.
   rewrite Int.shl_mul. rewrite Int.mul_add_distr_l. rewrite (Int.shl_mul n1). auto.
-  TrivialExists. econstructor. EvalOp. simpl; eauto. constructor. auto. 
+  TrivialExists. econstructor. EvalOp. simpl; eauto. constructor. auto.
   destruct (shift_is_scale n).
-  econstructor; split. EvalOp. simpl. eauto. 
+  econstructor; split. EvalOp. simpl. eauto.
   destruct x; simpl; auto. rewrite LT.
-  rewrite Int.add_zero. rewrite Int.shl_mul. auto. 
+  rewrite Int.add_zero. rewrite Int.shl_mul. auto.
   TrivialExists.
-  intros; TrivialExists. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. 
+  intros; TrivialExists. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor.
   auto.
 Qed.
 
@@ -243,18 +243,18 @@ Proof.
   intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shru_zero; auto.
   destruct (Int.ltu n Int.iwordsize) eqn:LT; simpl.
   destruct (shruimm_match a); intros; InvEval.
-  exists (Vint (Int.shru n1 n)); split. EvalOp. 
-  simpl. rewrite LT; auto. 
+  exists (Vint (Int.shru n1 n)); split. EvalOp.
+  simpl. rewrite LT; auto.
   destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?.
   exists (Val.shru v1 (Vint (Int.add n n1))); split. EvalOp.
-  subst. destruct v1; simpl; auto. 
+  subst. destruct v1; simpl; auto.
   rewrite Heqb.
   destruct (Int.ltu n1 Int.iwordsize) eqn:?; simpl; auto.
   rewrite LT. rewrite Int.add_commut. rewrite Int.shru_shru; auto. rewrite Int.add_commut; auto.
-  subst. TrivialExists. econstructor. EvalOp. simpl; eauto. constructor. 
+  subst. TrivialExists. econstructor. EvalOp. simpl; eauto. constructor.
   simpl. auto.
   TrivialExists.
-  intros; TrivialExists. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. 
+  intros; TrivialExists. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor.
   auto.
 Qed.
 
@@ -267,32 +267,32 @@ Proof.
   intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shr_zero; auto.
   destruct (Int.ltu n Int.iwordsize) eqn:LT; simpl.
   destruct (shrimm_match a); intros; InvEval.
-  exists (Vint (Int.shr n1 n)); split. EvalOp. 
-  simpl. rewrite LT; auto. 
+  exists (Vint (Int.shr n1 n)); split. EvalOp.
+  simpl. rewrite LT; auto.
   destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?.
   exists (Val.shr v1 (Vint (Int.add n n1))); split. EvalOp.
-  subst. destruct v1; simpl; auto. 
+  subst. destruct v1; simpl; auto.
   rewrite Heqb.
   destruct (Int.ltu n1 Int.iwordsize) eqn:?; simpl; auto.
-  rewrite LT. 
+  rewrite LT.
   rewrite Int.add_commut. rewrite Int.shr_shr; auto. rewrite Int.add_commut; auto.
-  subst. TrivialExists. econstructor. EvalOp. simpl; eauto. constructor. 
+  subst. TrivialExists. econstructor. EvalOp. simpl; eauto. constructor.
   simpl. auto.
   TrivialExists.
-  intros; TrivialExists. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. 
+  intros; TrivialExists. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor.
   auto.
 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.
@@ -301,33 +301,33 @@ Proof.
   exploit (eval_shlimm i (x :: le) (Eletvar 0) x). constructor; auto. intros [v1 [A1 B1]].
   exploit (eval_shlimm i0 (x :: le) (Eletvar 0) x). constructor; auto. intros [v2 [A2 B2]].
   exploit eval_add. eexact A1. eexact A2. intros [v3 [A3 B3]].
-  exists v3; split. econstructor; eauto. 
+  exists v3; split. econstructor; eauto.
   rewrite Int.add_zero.
   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.lessdef_trans with (Val.add v1 v2); auto. apply Val.add_lessdef; auto. 
-  simpl. repeat rewrite H0; auto with coqlib. 
-  intros. TrivialExists. 
+  repeat rewrite Val.shl_mul.
+  apply Val.lessdef_trans with (Val.add v1 v2); auto. 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.
@@ -336,7 +336,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.
@@ -345,8 +345,8 @@ 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.
-  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.and_zero. auto.
   predSpec Int.eq Int.eq_spec n Int.mone.
   intros. exists x; split; auto.
@@ -354,9 +354,9 @@ Proof.
   case (andimm_match a); intros; InvEval.
   TrivialExists. simpl. rewrite Int.and_commut; auto.
   subst. TrivialExists. simpl. rewrite Val.and_assoc. rewrite Int.and_commut. auto.
-  subst. rewrite Val.zero_ext_and. TrivialExists. rewrite Val.and_assoc. 
+  subst. rewrite Val.zero_ext_and. TrivialExists. rewrite Val.and_assoc.
   rewrite Int.and_commut. auto. compute; auto.
-  subst. rewrite Val.zero_ext_and. TrivialExists. rewrite Val.and_assoc. 
+  subst. rewrite Val.zero_ext_and. TrivialExists. rewrite Val.and_assoc.
   rewrite Int.and_commut. auto. compute; auto.
   TrivialExists.
 Qed.
@@ -373,15 +373,15 @@ Theorem eval_orimm:
   forall n, unary_constructor_sound (orimm n) (fun x => Val.or x (Vint n)).
 Proof.
   intros; red; intros until x. unfold orimm.
-  predSpec Int.eq Int.eq_spec n Int.zero. 
-  intros. exists x; split. auto.  
+  predSpec Int.eq Int.eq_spec n Int.zero.
+  intros. exists x; split. auto.
   destruct x; simpl; auto. subst n. rewrite Int.or_zero. auto.
   predSpec Int.eq Int.eq_spec n Int.mone.
   intros. exists (Vint Int.mone); split. EvalOp.
   destruct x; simpl; auto. subst n. rewrite Int.or_mone. auto.
   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.
 
@@ -393,10 +393,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.
 
@@ -410,33 +410,33 @@ Lemma eval_or: binary_constructor_sound or Val.or.
 Proof.
   red; intros until y; unfold or; case (or_match a b); intros.
 (* intconst *)
-  InvEval. rewrite Val.or_commut. apply eval_orimm; auto. 
+  InvEval. rewrite Val.or_commut. apply eval_orimm; auto.
   InvEval. apply eval_orimm; auto.
 (* shlimm - shruimm *)
   predSpec Int.eq Int.eq_spec (Int.add n1 n2) Int.iwordsize.
   destruct (same_expr_pure t1 t2) eqn:?.
-  InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]; subst. 
+  InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]; subst.
   exists (Val.ror v0 (Vint n2)); split. EvalOp.
-  destruct v0; simpl; auto. 
+  destruct v0; simpl; auto.
   destruct (Int.ltu n1 Int.iwordsize) eqn:?; auto.
   destruct (Int.ltu n2 Int.iwordsize) eqn:?; auto.
   simpl. rewrite <- Int.or_ror; auto.
-  InvEval. exists (Val.or x y); split. EvalOp. 
+  InvEval. exists (Val.or x y); split. EvalOp.
   simpl. erewrite int_add_sub_eq; eauto. rewrite H0; rewrite H; auto. auto.
-  TrivialExists. 
-(* shruimm - shlimm *) 
+  TrivialExists.
+(* shruimm - shlimm *)
   predSpec Int.eq Int.eq_spec (Int.add n1 n2) Int.iwordsize.
   destruct (same_expr_pure t1 t2) eqn:?.
-  InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]; subst. 
+  InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]; subst.
   exists (Val.ror v1 (Vint n2)); split. EvalOp.
-  destruct v1; simpl; auto. 
+  destruct v1; simpl; auto.
   destruct (Int.ltu n2 Int.iwordsize) eqn:?; auto.
   destruct (Int.ltu n1 Int.iwordsize) eqn:?; auto.
   simpl. rewrite Int.or_commut. rewrite <- Int.or_ror; auto.
-  InvEval. exists (Val.or y x); split. EvalOp. 
+  InvEval. exists (Val.or y x); split. EvalOp.
   simpl. erewrite int_add_sub_eq; eauto. rewrite H0; rewrite H; auto.
   rewrite Val.or_commut; auto.
-  TrivialExists. 
+  TrivialExists.
 (* default *)
   TrivialExists.
 Qed.
@@ -445,13 +445,13 @@ Theorem eval_xorimm:
   forall n, unary_constructor_sound (xorimm n) (fun x => Val.xor x (Vint n)).
 Proof.
   intros; red; intros until x. unfold xorimm.
-  predSpec Int.eq Int.eq_spec n Int.zero. 
-  intros. exists x; split. auto.  
+  predSpec Int.eq Int.eq_spec n Int.zero.
+  intros. exists x; split. auto.
   destruct x; simpl; auto. subst n. rewrite Int.xor_zero. auto.
   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. rewrite Val.not_xor. rewrite Val.xor_assoc. 
+  subst. rewrite Val.not_xor. rewrite Val.xor_assoc.
   rewrite (Val.xor_commut (Vint Int.mone)). TrivialExists.
   TrivialExists.
 Qed.
@@ -510,13 +510,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.
@@ -525,38 +525,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.
@@ -569,19 +569,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.
@@ -615,8 +615,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.
@@ -625,13 +625,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.
@@ -639,21 +639,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.
@@ -668,7 +668,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.
@@ -677,9 +677,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.
 
@@ -687,9 +687,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.
 
@@ -732,7 +732,7 @@ Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ex
 Proof.
   red; intros until x. unfold cast16unsigned. destruct (cast16unsigned_match a); intros; InvEval.
   TrivialExists.
-  subst. rewrite Val.zero_ext_and. rewrite Val.and_assoc. 
+  subst. rewrite Val.zero_ext_and. rewrite Val.and_assoc.
   rewrite Int.and_commut. apply eval_andimm; auto. compute; auto.
   TrivialExists.
 Qed.
@@ -753,7 +753,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_floatofint:
@@ -764,7 +764,7 @@ Theorem eval_floatofint:
 Proof.
   intros until y; unfold floatofint. case (floatofint_match a); intros; InvEval.
   TrivialExists.
-  TrivialExists. 
+  TrivialExists.
 Qed.
 
 Theorem eval_intuoffloat:
@@ -783,24 +783,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.
@@ -815,20 +815,20 @@ Proof.
   InvEval. TrivialExists.
   destruct x; simpl in H0; try discriminate. inv H0.
   exists (Vfloat (Float.of_intu i)); split; auto.
-  econstructor. eauto. 
+  econstructor. eauto.
   set (fm := Float.of_intu Float.ox8000_0000).
   assert (eval_expr ge sp e m (Vint i :: le) (Eletvar O) (Vint i)).
-    constructor. auto. 
+    constructor. auto.
   eapply eval_Econdition with (va := Int.ltu i Float.ox8000_0000).
   eauto with evalexpr.
   destruct (Int.ltu i Float.ox8000_0000) eqn:?.
   rewrite Float.of_intu_of_int_1; auto.
-  unfold floatofint. EvalOp. 
+  unfold floatofint. EvalOp.
   exploit (eval_addimm (Int.neg Float.ox8000_0000) (Vint i :: le) (Eletvar 0)); eauto.
-  simpl. intros [v [A B]]. inv B. 
-  unfold addf. EvalOp. 
-  constructor. unfold floatofint. EvalOp. simpl; eauto. 
-  constructor. EvalOp. simpl; eauto. constructor. simpl; eauto. 
+  simpl. intros [v [A B]]. inv B.
+  unfold addf. EvalOp.
+  constructor. unfold floatofint. EvalOp. simpl; eauto.
+  constructor. EvalOp. simpl; eauto. constructor. simpl; eauto.
   fold fm. rewrite Float.of_intu_of_int_2; auto.
   rewrite Int.sub_add_opp. auto.
 Qed.
@@ -839,7 +839,7 @@ 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. TrivialExists. 
+  intros; unfold intofsingle. TrivialExists.
 Qed.
 
 Theorem eval_singleofint:
@@ -850,7 +850,7 @@ Theorem eval_singleofint:
 Proof.
   intros until y; unfold singleofint. case (singleofint_match a); intros; InvEval.
   TrivialExists.
-  TrivialExists. 
+  TrivialExists.
 Qed.
 
 Theorem eval_intuofsingle:
@@ -862,9 +862,9 @@ Proof.
   intros. destruct x; simpl in H0; try discriminate.
   destruct (Float32.to_intu f) as [n|] eqn:?; simpl in H0; inv H0.
   unfold intuofsingle. apply eval_intuoffloat with (Vfloat (Float.of_single f)).
-  unfold floatofsingle. EvalOp. 
-  simpl. change (Float.of_single f) with (Float32.to_double f). 
-  erewrite Float32.to_intu_double; eauto. auto. 
+  unfold floatofsingle. EvalOp.
+  simpl. change (Float.of_single f) with (Float32.to_double f).
+  erewrite Float32.to_intu_double; eauto. auto.
 Qed.
 
 Theorem eval_singleofintu:
@@ -876,11 +876,11 @@ Proof.
   intros until y; unfold singleofintu. case (singleofintu_match a); intros.
   InvEval. TrivialExists.
   destruct x; simpl in H0; try discriminate. inv H0.
-  exploit eval_floatofintu. eauto. simpl. reflexivity. 
+  exploit eval_floatofintu. eauto. simpl. reflexivity.
   intros (v & A & B).
   exists (Val.singleoffloat v); split.
   unfold singleoffloat; EvalOp.
-  inv B; simpl. rewrite Float32.of_intu_double. auto. 
+  inv B; simpl. rewrite Float32.of_intu_double. auto.
 Qed.
 
 Theorem eval_addressing:
@@ -889,13 +889,13 @@ 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.
   intros until v. unfold addressing; case (addressing_match a); intros; InvEval.
   inv H. exists vl; auto.
-  exists (v :: nil); split. constructor; auto. constructor. subst; simpl. rewrite Int.add_zero; auto. 
+  exists (v :: nil); split. constructor; auto. constructor. subst; simpl. rewrite Int.add_zero; auto.
 Qed.
 
 Theorem eval_builtin_arg:
@@ -906,7 +906,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/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
index 3f5e6cfe..fe2c2998 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -83,13 +83,13 @@ module Cygwin_System : SYSTEM =
 
     let raw_symbol oc s =
        fprintf oc "_%s" s
-        
+
     let symbol oc symb =
       raw_symbol oc (extern_atom symb)
 
     let label oc lbl =
        fprintf oc "L%d" lbl
-        
+
     let name_of_section = function
       | Section_text -> ".text"
       | Section_data i | Section_small_data i ->
@@ -111,12 +111,12 @@ module Cygwin_System : SYSTEM =
 
     let print_align oc n =
       fprintf oc "	.align	%d\n" n
-    
-    let print_mov_ra oc rd id =   
+
+    let print_mov_ra oc rd id =
       fprintf oc "	movl	$%a, %a\n" symbol id ireg rd
 
     let print_fun_info _ _  = ()
-        
+
     let print_var_info _ _ = ()
 
     let print_epilogue _ = ()
@@ -133,10 +133,10 @@ module Cygwin_System : SYSTEM =
 (* Printer functions for ELF *)
 module ELF_System : SYSTEM =
   struct
-    
+
     let raw_symbol oc s =
       fprintf oc "%s" s
-  
+
     let symbol = elf_symbol
 
     let label = elf_label
@@ -157,19 +157,19 @@ module ELF_System : SYSTEM =
       | Section_debug_loc -> ".section	.debug_loc,\"\",@progbits"
       | Section_debug_line _ -> ".section	.debug_line,\"\",@progbits"
       | Section_debug_abbrev -> ".section	.debug_abbrev,\"\",@progbits"
-            
+
     let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *)
-                    
+
     let print_align oc n =
       fprintf oc "	.align	%d\n" n
-        
-    let print_mov_ra  oc rd id = 
+
+    let print_mov_ra  oc rd id =
          fprintf oc "	movl	$%a, %a\n" symbol id ireg rd
 
     let print_fun_info = elf_print_fun_info
-      
+
     let print_var_info = elf_print_var_info
-      
+
     let print_epilogue _ = ()
 
     let print_comm_decl oc name sz al =
@@ -184,7 +184,7 @@ module ELF_System : SYSTEM =
 (* Printer functions for MacOS *)
 module MacOS_System : SYSTEM =
   struct
-    
+
     let raw_symbol oc s =
      fprintf oc "_%s" s
 
@@ -211,30 +211,30 @@ module MacOS_System : SYSTEM =
       | Section_debug_loc  -> ".section	__DWARF,__debug_loc,regular,debug"
       | Section_debug_line _ -> ".section	__DWARF,__debug_line,regular,debug"
       | Section_debug_abbrev -> ".section	__DWARF,__debug_abbrev,regular,debug" (* Dummy value *)
-    
-    
+
+
     let stack_alignment =  16 (* mandatory *)
-         
-    (* Base-2 log of a Caml integer *)           
+
+    (* Base-2 log of a Caml integer *)
     let rec log2 n =
       assert (n > 0);
       if n = 1 then 0 else 1 + log2 (n lsr 1)
 
     let print_align oc n =
       fprintf oc "	.align	%d\n" (log2 n)
-        
+
     let indirect_symbols : StringSet.t ref = ref StringSet.empty
 
-    let print_mov_ra oc rd id = 
+    let print_mov_ra oc rd id =
       let id = extern_atom id in
       indirect_symbols := StringSet.add id !indirect_symbols;
       fprintf oc "	movl	L%a$non_lazy_ptr, %a\n" raw_symbol id ireg rd
 
     let print_fun_info _ _ = ()
- 
+
     let print_var_info _ _ = ()
-    
-    let print_epilogue oc = 
+
+    let print_epilogue oc =
       fprintf oc "	.section __IMPORT,__pointers,non_lazy_symbol_pointers\n";
       StringSet.iter
         (fun s ->
@@ -272,7 +272,7 @@ module Target(System: SYSTEM):TARGET =
       | Coq_inl n ->
           let n = camlint_of_coqint n in
           fprintf oc "%ld" n
-      | Coq_inr(id, ofs) -> 
+      | Coq_inr(id, ofs) ->
           let ofs = camlint_of_coqint ofs in
           if ofs = 0l
           then symbol oc id
@@ -289,13 +289,13 @@ module Target(System: SYSTEM):TARGET =
       | Cond_e -> "e" | Cond_ne -> "ne"
       | Cond_b -> "b" | Cond_be -> "be" | Cond_ae -> "ae" | Cond_a -> "a"
       | Cond_l -> "l" | Cond_le -> "le" | Cond_ge -> "ge" | Cond_g -> "g"
-      | Cond_p -> "p" | Cond_np -> "np" 
+      | Cond_p -> "p" | Cond_np -> "np"
 
     let name_of_neg_condition = function
       | Cond_e -> "ne" | Cond_ne -> "e"
       | Cond_b -> "ae" | Cond_be -> "a" | Cond_ae -> "b" | Cond_a -> "be"
       | Cond_l -> "ge" | Cond_le -> "g" | Cond_ge -> "l" | Cond_g -> "le"
-      | Cond_p -> "np" | Cond_np -> "p" 
+      | Cond_p -> "np" | Cond_np -> "p"
 
 
 (* Names of sections *)
@@ -339,7 +339,7 @@ module Target(System: SYSTEM):TARGET =
 
 (* Built-in functions *)
 
-(* Built-ins.  They come in two flavors: 
+(* Built-ins.  They come in two flavors:
    - annotation statements: take their arguments in registers or stack
    locations; generate no code;
    - inlined by the compiler: take their arguments in arbitrary
@@ -649,7 +649,7 @@ module Target(System: SYSTEM):TARGET =
       (** Pseudo-instructions *)
       | Plabel(l) ->
           fprintf oc "%a:\n" label (transl_label l)
-      | Pallocframe(sz, ofs_ra, ofs_link) 
+      | Pallocframe(sz, ofs_ra, ofs_link)
       | Pfreeframe(sz, ofs_ra, ofs_link) ->
 	 assert false
       | Pbuiltin(ef, args, res) ->
@@ -667,13 +667,13 @@ module Target(System: SYSTEM):TARGET =
           | _ ->
               assert false
           end
-            
+
     let print_literal64 oc (lbl, n) =
       fprintf oc "%a:	.quad	0x%Lx\n" label lbl n
     let print_literal32 oc (lbl, n) =
       fprintf oc "%a:	.long	0x%lx\n" label lbl n
-        
-    let print_jumptable oc jmptbl = 
+
+    let print_jumptable oc jmptbl =
       let print_jumptable oc (lbl, tbl) =
         fprintf oc "%a:" label lbl;
         List.iter
@@ -685,7 +685,7 @@ module Target(System: SYSTEM):TARGET =
         List.iter (print_jumptable oc) !jumptables;
         jumptables := []
       end
-          
+
     let print_init oc = function
       | Init_int8 n ->
           fprintf oc "	.byte	%ld\n" (camlint_of_coqint n)
@@ -707,7 +707,7 @@ module Target(System: SYSTEM):TARGET =
           if Z.gt n Z.zero then
             fprintf oc "	.space	%s\n" (Z.to_string n)
       | Init_addrof(symb, ofs) ->
-          fprintf oc "	.long	%a\n" 
+          fprintf oc "	.long	%a\n"
             symbol_offset (symb, camlint_of_coqint ofs)
 
     let print_align = print_align
@@ -738,7 +738,7 @@ module Target(System: SYSTEM):TARGET =
 
     let print_optional_fun_info _ = ()
 
-    let get_section_names name = 
+    let get_section_names name =
       match C2C.atom_sections name with
       | [t;l;j] -> (t, l, j)
       |    _    -> (Section_text, Section_literal, Section_jumptable)
@@ -746,10 +746,10 @@ module Target(System: SYSTEM):TARGET =
     let reset_constants = reset_constants
 
     let print_fun_info = print_fun_info
-        
+
     let print_var_info = print_var_info
 
-    let print_prologue oc = 
+    let print_prologue oc =
       need_masks := false;
       if !Clflags.option_g then begin
         section oc Section_text;
@@ -759,7 +759,7 @@ module Target(System: SYSTEM):TARGET =
         fprintf oc "	.cfi_sections	.debug_frame\n"
       end
 
-    let print_epilogue oc = 
+    let print_epilogue oc =
       if !need_masks then begin
         section oc (Section_const true);
         (* not Section_literal because not 8-bytes *)
@@ -781,13 +781,13 @@ module Target(System: SYSTEM):TARGET =
         section oc Section_text;
         fprintf oc "%a:\n" elf_label high_pc
       end
-      
+
     let comment = comment
 
     let default_falignment = 16
 
     let label = label
-       
+
     let new_label = new_label
 
 end
@@ -795,7 +795,7 @@ end
 let sel_target () =
  let module S = (val (match Configuration.system with
   | "macosx" -> (module MacOS_System:SYSTEM)
-  | "linux" 
+  | "linux"
   | "bsd" -> (module ELF_System:SYSTEM)
   | "cygwin" -> (module Cygwin_System:SYSTEM)
   | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported")  ):SYSTEM) in
diff --git a/ia32/ValueAOp.v b/ia32/ValueAOp.v
index 93fd8954..ad18c4f6 100644
--- a/ia32/ValueAOp.v
+++ b/ia32/ValueAOp.v
@@ -132,7 +132,7 @@ Proof.
   inv VM.
   destruct cond; auto with va.
   inv H0.
-  destruct cond; simpl; eauto with va.  
+  destruct cond; simpl; eauto with va.
   inv H2.
   destruct cond; simpl; eauto with va.
   destruct cond; auto with va.
@@ -149,7 +149,7 @@ Lemma symbol_address_sound_2:
   forall id ofs,
   vmatch bc (Genv.symbol_address ge id ofs) (Ifptr (Gl id ofs)).
 Proof.
-  intros. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:F. 
+  intros. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:F.
   constructor. constructor. apply GENV; auto.
   constructor.
 Qed.
@@ -173,7 +173,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:
@@ -187,7 +187,7 @@ Proof.
   destruct (propagate_float_constants tt); constructor.
   destruct (propagate_float_constants tt); constructor.
   eapply eval_static_addressing_sound; eauto.
-  apply of_optbool_sound. eapply eval_static_condition_sound; eauto. 
+  apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
 Qed.
 
 End SOUNDNESS.