Updated PR by removing whitespaces. Bug 17450.

16 files changed, 658 insertions, 658 deletions

diff --git a/arm/Asm.v b/arm/Asm.v
index 1fd792b8..b350b047 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -92,7 +92,7 @@ Notation "'RA'" := IR14 (only parsing).
   reference manuals for more details.  Some instructions,
   described below, are pseudo-instructions: they expand to
   canned instruction sequences during the printing of the assembly
-  code.  Most instructions are common to Thumb2 and ARM classic.  
+  code.  Most instructions are common to Thumb2 and ARM classic.
   We use a few Thumb2-specific instructions when available, and avoid
   to use ARM classic features that are not in Thumb2. *)
 
@@ -228,8 +228,8 @@ Inductive instruction : Type :=
   | Pstr_p: ireg -> ireg -> shift_op -> instruction   (**r int32 store with post increment *)
   | Pstrb_p: ireg -> ireg -> shift_op -> instruction  (**r unsigned int8 store with post increment *)
   | Pstrh_p: ireg -> ireg -> shift_op -> instruction. (**r unsigned int16 store with post increment *)
- 
- 
+
+
 
 (** The pseudo-instructions are the following:
 
@@ -290,7 +290,7 @@ Definition program := AST.program fundef unit.
   the convention that integer registers are mapped to values of
   type [Tint], float registers to values of type [Tfloat],
   and condition bits to either [Vzero] or [Vone]. *)
-  
+
 Definition regset := Pregmap.t val.
 Definition genv := Genv.t fundef unit.
 
@@ -405,7 +405,7 @@ Definition eval_shift_op (so: shift_op) (rs: regset) :=
 
 (** Auxiliaries for memory accesses *)
 
-Definition exec_load (chunk: memory_chunk) (addr: val) (r: preg) 
+Definition exec_load (chunk: memory_chunk) (addr: val) (r: preg)
                      (rs: regset) (m: mem) :=
   match Mem.loadv chunk m addr with
   | None => Stuck
@@ -549,74 +549,74 @@ Definition eval_testcond (c: testcond) (rs: regset) : option bool :=
 
 Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : outcome :=
   match i with
-  | Padd r1 r2 so => 
+  | Padd r1 r2 so =>
       Next (nextinstr_nf (rs#r1 <- (Val.add rs#r2 (eval_shift_op so rs)))) m
-  | Pand r1 r2 so => 
+  | Pand r1 r2 so =>
       Next (nextinstr_nf (rs#r1 <- (Val.and rs#r2 (eval_shift_op so rs)))) m
   | Pasr r1 r2 r3 =>
       Next (nextinstr_nf (rs#r1 <- (Val.shr rs#r2 rs#r3))) m
-  | Pb lbl =>                      
+  | Pb lbl =>
       goto_label f lbl rs m
-  | Pbc cond lbl =>            
+  | Pbc cond lbl =>
       match eval_testcond cond rs with
       | Some true => goto_label f lbl rs m
       | Some false => Next (nextinstr rs) m
       | None => Stuck
       end
-  | Pbsymb id sg =>                  
+  | Pbsymb id sg =>
       Next (rs#PC <- (Genv.symbol_address ge id Int.zero)) m
-  | Pbreg r sg =>                    
+  | Pbreg r sg =>
       Next (rs#PC <- (rs#r)) m
-  | Pblsymb id sg =>                 
+  | Pblsymb id sg =>
       Next (rs#IR14 <- (Val.add rs#PC Vone) #PC <- (Genv.symbol_address ge id Int.zero)) m
-  | Pblreg r sg =>                   
+  | Pblreg r sg =>
       Next (rs#IR14 <- (Val.add rs#PC Vone) #PC <- (rs#r)) m
-  | Pbic r1 r2 so => 
+  | Pbic r1 r2 so =>
       Next (nextinstr_nf (rs#r1 <- (Val.and rs#r2 (Val.notint (eval_shift_op so rs))))) m
-  | Pcmp r1 so => 
+  | Pcmp r1 so =>
       Next (nextinstr (compare_int rs rs#r1 (eval_shift_op so rs) m)) m
-  | Peor r1 r2 so => 
+  | Peor r1 r2 so =>
       Next (nextinstr_nf (rs#r1 <- (Val.xor rs#r2 (eval_shift_op so rs)))) m
-  | Pldr r1 r2 sa => 
+  | Pldr r1 r2 sa =>
       exec_load Mint32 (Val.add rs#r2 (eval_shift_op sa rs)) r1 rs m
-  | Pldr_a r1 r2 sa => 
+  | Pldr_a r1 r2 sa =>
       exec_load Many32 (Val.add rs#r2 (eval_shift_op sa rs)) r1 rs m
-  | Pldrb r1 r2 sa => 
+  | Pldrb r1 r2 sa =>
       exec_load Mint8unsigned (Val.add rs#r2 (eval_shift_op sa rs)) r1 rs m
-  | Pldrh r1 r2 sa => 
+  | Pldrh r1 r2 sa =>
       exec_load Mint16unsigned (Val.add rs#r2 (eval_shift_op sa rs)) r1 rs m
-  | Pldrsb r1 r2 sa => 
+  | Pldrsb r1 r2 sa =>
       exec_load Mint8signed (Val.add rs#r2 (eval_shift_op sa rs)) r1 rs m
-  | Pldrsh r1 r2 sa => 
+  | Pldrsh r1 r2 sa =>
       exec_load Mint16signed (Val.add rs#r2 (eval_shift_op sa rs)) r1 rs m
   | Plsl r1 r2 r3 =>
       Next (nextinstr_nf (rs#r1 <- (Val.shl rs#r2 rs#r3))) m
   | Plsr r1 r2 r3 =>
       Next (nextinstr_nf (rs#r1 <- (Val.shru rs#r2 rs#r3))) m
-  | Pmla r1 r2 r3 r4 =>      
+  | Pmla r1 r2 r3 r4 =>
       Next (nextinstr (rs#r1 <- (Val.add (Val.mul rs#r2 rs#r3) rs#r4))) m
-  | Pmov r1 so =>          
+  | Pmov r1 so =>
       Next (nextinstr_nf (rs#r1 <- (eval_shift_op so rs))) m
   | Pmovw r n =>
       Next (nextinstr (rs#r <- (Vint n))) m
   | Pmovt r n =>
       Next (nextinstr (rs#r <- (Val.or (Val.and rs#r (Vint (Int.repr 65535)))
                                        (Vint (Int.shl n (Int.repr 16)))))) m
-  | Pmul r1 r2 r3 =>      
+  | Pmul r1 r2 r3 =>
       Next (nextinstr (rs#r1 <- (Val.mul rs#r2 rs#r3))) m
-  | Pmvn r1 so =>          
+  | Pmvn r1 so =>
       Next (nextinstr_nf (rs#r1 <- (Val.notint (eval_shift_op so rs)))) m
-  | Porr r1 r2 so =>  
+  | Porr r1 r2 so =>
       Next (nextinstr_nf (rs#r1 <- (Val.or rs#r2 (eval_shift_op so rs)))) m
-  | Prsb r1 r2 so =>  
+  | Prsb r1 r2 so =>
       Next (nextinstr_nf (rs#r1 <- (Val.sub (eval_shift_op so rs) rs#r2))) m
-  | Pstr r1 r2 sa => 
+  | Pstr r1 r2 sa =>
       exec_store Mint32 (Val.add rs#r2 (eval_shift_op sa rs)) r1 rs m
-  | Pstr_a r1 r2 sa => 
+  | Pstr_a r1 r2 sa =>
       exec_store Many32 (Val.add rs#r2 (eval_shift_op sa rs)) r1 rs m
-  | Pstrb r1 r2 sa => 
+  | Pstrb r1 r2 sa =>
       exec_store Mint8unsigned (Val.add rs#r2 (eval_shift_op sa rs)) r1 rs m
-  | Pstrh r1 r2 sa => 
+  | Pstrh r1 r2 sa =>
       exec_store Mint16unsigned (Val.add rs#r2 (eval_shift_op sa rs)) r1 rs m
   | Psdiv =>
       match Val.divs rs#IR0 rs#IR1 with
@@ -630,7 +630,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Psmull rdl rdh r1 r2 =>
       Next (nextinstr (rs#rdl <- (Val.mul rs#r1 rs#r2)
                          #rdh <- (Val.mulhs rs#r1 rs#r2))) m
-  | Psub r1 r2 so =>  
+  | Psub r1 r2 so =>
       Next (nextinstr_nf (rs#r1 <- (Val.sub rs#r2 (eval_shift_op so rs)))) m
   | Pudiv =>
       match Val.divu rs#IR0 rs#IR1 with
@@ -645,23 +645,23 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   (* Floating-point coprocessor instructions *)
   | Pfcpyd r1 r2 =>
       Next (nextinstr (rs#r1 <- (rs#r2))) m
-  | Pfabsd r1 r2 => 
+  | Pfabsd r1 r2 =>
       Next (nextinstr (rs#r1 <- (Val.absf rs#r2))) m
-  | Pfnegd r1 r2 => 
+  | Pfnegd r1 r2 =>
       Next (nextinstr (rs#r1 <- (Val.negf rs#r2))) m
-  | Pfaddd r1 r2 r3 =>     
+  | Pfaddd r1 r2 r3 =>
       Next (nextinstr (rs#r1 <- (Val.addf rs#r2 rs#r3))) m
-  | Pfdivd r1 r2 r3 =>     
+  | Pfdivd r1 r2 r3 =>
       Next (nextinstr (rs#r1 <- (Val.divf rs#r2 rs#r3))) m
-  | Pfmuld r1 r2 r3 =>     
+  | Pfmuld r1 r2 r3 =>
       Next (nextinstr (rs#r1 <- (Val.mulf rs#r2 rs#r3))) m
-  | Pfsubd r1 r2 r3 =>     
+  | Pfsubd r1 r2 r3 =>
       Next (nextinstr (rs#r1 <- (Val.subf rs#r2 rs#r3))) m
-  | Pflid r1 f =>            
+  | Pflid r1 f =>
       Next (nextinstr (rs#r1 <- (Vfloat f))) m
-  | Pfcmpd r1 r2 =>              
+  | Pfcmpd r1 r2 =>
       Next (nextinstr (compare_float rs rs#r1 rs#r2)) m
-  | Pfcmpzd r1 =>              
+  | Pfcmpzd r1 =>
       Next (nextinstr (compare_float rs rs#r1 (Vfloat Float.zero))) m
   | Pfsitod r1 r2 =>
       Next (nextinstr (rs#r1 <- (Val.maketotal (Val.floatofint rs#r2)))) m
@@ -671,23 +671,23 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Next (nextinstr (rs #FR6 <- Vundef #r1 <- (Val.maketotal (Val.intoffloat rs#r2)))) m
   | Pftouizd r1 r2 =>
       Next (nextinstr (rs #FR6 <- Vundef #r1 <- (Val.maketotal (Val.intuoffloat rs#r2)))) m
-  | Pfabss r1 r2 => 
+  | Pfabss r1 r2 =>
       Next (nextinstr (rs#r1 <- (Val.absfs rs#r2))) m
-  | Pfnegs r1 r2 => 
+  | Pfnegs r1 r2 =>
       Next (nextinstr (rs#r1 <- (Val.negfs rs#r2))) m
-  | Pfadds r1 r2 r3 =>     
+  | Pfadds r1 r2 r3 =>
       Next (nextinstr (rs#r1 <- (Val.addfs rs#r2 rs#r3))) m
-  | Pfdivs r1 r2 r3 =>     
+  | Pfdivs r1 r2 r3 =>
       Next (nextinstr (rs#r1 <- (Val.divfs rs#r2 rs#r3))) m
-  | Pfmuls r1 r2 r3 =>     
+  | Pfmuls r1 r2 r3 =>
       Next (nextinstr (rs#r1 <- (Val.mulfs rs#r2 rs#r3))) m
-  | Pfsubs r1 r2 r3 =>     
+  | Pfsubs r1 r2 r3 =>
       Next (nextinstr (rs#r1 <- (Val.subfs rs#r2 rs#r3))) m
-  | Pflis r1 f =>            
+  | Pflis r1 f =>
       Next (nextinstr (rs#r1 <- (Vsingle f))) m
-  | Pfcmps r1 r2 =>              
+  | Pfcmps r1 r2 =>
       Next (nextinstr (compare_float32 rs rs#r1 rs#r2)) m
-  | Pfcmpzs r1 =>              
+  | Pfcmpzs r1 =>
       Next (nextinstr (compare_float32 rs rs#r1 (Vsingle Float32.zero))) m
   | Pfsitos r1 r2 =>
       Next (nextinstr (rs#r1 <- (Val.maketotal (Val.singleofint rs#r2)))) m
@@ -707,14 +707,14 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       exec_load Many64 (Val.add rs#r2 (Vint n)) r1 rs m
   | Pflds r1 r2 n =>
       exec_load Mfloat32 (Val.add rs#r2 (Vint n)) r1 rs m
-  | Pfstd r1 r2 n =>      
+  | Pfstd r1 r2 n =>
       exec_store Mfloat64 (Val.add rs#r2 (Vint n)) r1 rs m
-  | Pfstd_a r1 r2 n =>      
+  | Pfstd_a r1 r2 n =>
       exec_store Many64 (Val.add rs#r2 (Vint n)) r1 rs m
   | Pfsts r1 r2 n =>
       exec_store Mfloat32 (Val.add rs#r2 (Vint n)) r1 rs m
   (* Pseudo-instructions *)
-  | Pallocframe sz pos =>             
+  | Pallocframe sz pos =>
       let (m1, stk) := Mem.alloc m 0 sz in
       let sp := (Vptr stk Int.zero) in
       match Mem.storev Mint32 m1 (Val.add sp (Vint pos)) rs#IR13 with
@@ -748,7 +748,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Next (nextinstr (rs#r1 <- v)) m
   | Pbtbl r tbl =>
       match rs#r with
-      | Vint n => 
+      | Vint n =>
           match list_nth_z tbl (Int.unsigned n) with
           | None => Stuck
           | Some lbl => goto_label f lbl (rs#IR14 <- Vundef) m
@@ -873,7 +873,7 @@ Inductive final_state: state -> int -> Prop :=
       rs#PC = Vzero ->
       rs#IR0 = Vint r ->
       final_state (State rs m) r.
-      
+
 Definition semantics (p: program) :=
   Semantics step (initial_state p) final_state (Genv.globalenv p).
 
@@ -888,9 +888,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/arm/Asmexpand.ml b/arm/Asmexpand.ml
index fad13c9f..2b19cbe8 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -106,7 +106,7 @@ let memcpy_small_arg sz arg tmp =
       assert false
 
 let expand_builtin_memcpy_small sz al src dst =
-  let (tsrc, tdst) = 
+  let (tsrc, tdst) =
     if dst <> BA (IR IR2) then (IR2, IR3) else (IR3, IR2) in
   let (rsrc, osrc) = memcpy_small_arg sz src tsrc in
   let (rdst, odst) = memcpy_small_arg sz dst tdst in
@@ -142,7 +142,7 @@ let memcpy_big_arg arg tmp =
 let expand_builtin_memcpy_big sz al src dst =
   assert (sz >= al);
   assert (sz mod al = 0);
-  let (s, d) = 
+  let (s, d) =
     if dst <> BA (IR IR2) then (IR2, IR3) else (IR3, IR2) in
   memcpy_big_arg src s;
   memcpy_big_arg dst d;
diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index 2365d1d2..7b3f2fdc 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -198,7 +198,7 @@ Definition rsubimm (r1 r2: ireg) (n: int) (k: code) :=
   iterate_op (Prsb r1 r2) (Padd r1 r1) (decompose_int n) k.
 
 Definition andimm (r1 r2: ireg) (n: int) (k: code) :=
-  if is_immed_arith n 
+  if is_immed_arith n
   then Pand r1 r2 (SOimm n) :: k
   else iterate_op (Pbic r1 r2) (Pbic r1 r1) (decompose_int (Int.not n)) k.
 
@@ -402,7 +402,7 @@ Definition transl_op
       do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
       OK (Pmul r r1 r2 :: k)
   | Omla, a1 :: a2 :: a3 :: nil =>
-      do r <- ireg_of res; do r1 <- ireg_of a1; 
+      do r <- ireg_of res; do r1 <- ireg_of a1;
       do r2 <- ireg_of a2; do r3 <- ireg_of a3;
       OK (Pmla r r1 r2 r3 :: k)
   | Omulhs, a1 :: a2 :: nil =>
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index 93c50bfb..7a29e4a5 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -45,17 +45,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:
@@ -71,7 +71,7 @@ Lemma functions_transl:
   transf_function f = OK tf ->
   Genv.find_funct_ptr tge b = Some (Internal tf).
 Proof.
-  intros. 
+  intros.
   destruct (functions_translated _ _ H) as [tf' [A B]].
   rewrite A. monadInv B. f_equal. congruence.
 Qed.
@@ -79,9 +79,9 @@ 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 *)
@@ -102,7 +102,7 @@ Proof.
   intros. inv H.
   eapply exec_straight_steps_1; eauto.
   eapply transf_function_no_overflow; eauto.
-  eapply functions_transl; eauto. 
+  eapply functions_transl; eauto.
 Qed.
 
 Lemma exec_straight_at:
@@ -112,8 +112,8 @@ Lemma exec_straight_at:
   exec_straight tge tf tc rs m tc' rs' m' ->
   transl_code_at_pc ge (rs' PC) fb f c' ep' tf tc'.
 Proof.
-  intros. inv H. 
-  exploit exec_straight_steps_2; eauto. 
+  intros. inv H.
+  exploit exec_straight_steps_2; eauto.
   eapply transf_function_no_overflow; eauto.
   eapply functions_transl; eauto.
   intros [ofs' [PC' CT']].
@@ -134,22 +134,22 @@ Lemma label_pos_code_tail:
   forall lbl c pos c',
   find_label lbl c = Some c' ->
   exists pos',
-  label_pos lbl pos c = Some pos' 
+  label_pos lbl pos c = Some pos'
   /\ code_tail (pos' - pos) c c'
   /\ pos < pos' <= pos + list_length_z c.
 Proof.
-  induction c. 
+  induction c.
   simpl; intros. discriminate.
   simpl; intros until c'.
   case (is_label lbl a).
   intro EQ; injection EQ; intro; subst c'.
   exists (pos + 1). split. auto. split.
-  replace (pos + 1 - pos) with (0 + 1) by omega. constructor. constructor. 
-  rewrite list_length_z_cons. generalize (list_length_z_pos c). omega. 
+  replace (pos + 1 - pos) with (0 + 1) by omega. constructor. constructor.
+  rewrite list_length_z_cons. generalize (list_length_z_pos c). omega.
   intros. generalize (IHc (pos + 1) c' H). intros [pos' [A [B C]]].
   exists pos'. split. auto. split.
   replace (pos' - pos) with ((pos' - (pos + 1)) + 1) by omega.
-  constructor. auto. 
+  constructor. auto.
   rewrite list_length_z_cons. omega.
 Qed.
 
@@ -242,7 +242,7 @@ Remark indexed_memory_access_label:
   (forall r n, nolabel (mk_instr r n)) ->
   tail_nolabel k (indexed_memory_access mk_instr mk_immed base ofs k).
 Proof.
-  intros. unfold indexed_memory_access. 
+  intros. unfold indexed_memory_access.
   destruct (Int.eq ofs (mk_immed ofs)).
   TailNoLabel.
   eapply tail_nolabel_trans; TailNoLabel.
@@ -310,18 +310,18 @@ Proof.
   eapply loadind_label; eauto.
   eapply storeind_label; eauto.
   destruct ep. eapply loadind_label; eauto.
-    eapply tail_nolabel_trans. 2: eapply loadind_label; eauto. unfold loadind_int; TailNoLabel.  
+    eapply tail_nolabel_trans. 2: eapply loadind_label; eauto. unfold loadind_int; TailNoLabel.
   eapply transl_op_label; eauto.
-  unfold transl_load, transl_memory_access_int, transl_memory_access_float in H. 
-  destruct m; monadInv H; eapply transl_memory_access_label; eauto; simpl; auto. 
-  unfold transl_store, transl_memory_access_int, transl_memory_access_float in H. 
-  destruct m; monadInv H; eapply transl_memory_access_label; eauto; simpl; auto. 
+  unfold transl_load, transl_memory_access_int, transl_memory_access_float in H.
+  destruct m; monadInv H; eapply transl_memory_access_label; eauto; simpl; auto.
+  unfold transl_store, transl_memory_access_int, transl_memory_access_float in H.
+  destruct m; monadInv H; eapply transl_memory_access_label; eauto; simpl; auto.
   destruct s0; monadInv H; TailNoLabel.
   destruct s0; monadInv H; unfold loadind_int; eapply tail_nolabel_trans.
   eapply indexed_memory_access_label; auto with labels. TailNoLabel.
   eapply indexed_memory_access_label; auto with labels. TailNoLabel.
   eapply tail_nolabel_trans. eapply transl_cond_label; eauto. TailNoLabel.
-  eapply tail_nolabel_trans. unfold loadind_int. eapply indexed_memory_access_label; auto with labels. TailNoLabel. 
+  eapply tail_nolabel_trans. unfold loadind_int. eapply indexed_memory_access_label; auto with labels. TailNoLabel.
 Qed.
 
 Lemma transl_instr_label':
@@ -330,7 +330,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.
 
@@ -345,7 +345,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.
@@ -361,7 +361,7 @@ Lemma transl_find_label:
 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. 
+  eapply transl_code_label; eauto.
 Qed.
 
 End TRANSL_LABEL.
@@ -376,17 +376,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.
@@ -399,10 +399,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.
   exists x; exists true; split; auto. repeat constructor.
 - exact transf_function_no_overflow.
@@ -470,10 +470,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.
 
@@ -498,15 +498,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.
@@ -531,8 +531,8 @@ Definition measure (s: Mach.state) : nat :=
 
 Remark preg_of_not_R12: forall r, negb (mreg_eq r R12) = true -> IR IR12 <> preg_of r.
 Proof.
-  intros. change (IR IR12) with (preg_of R12). red; intros. 
-  exploit preg_of_injective; eauto. intros; subst r. 
+  intros. change (IR IR12) with (preg_of R12). red; intros.
+  exploit preg_of_injective; eauto. intros; subst r.
   unfold proj_sumbool in H; rewrite dec_eq_true in H; discriminate.
 Qed.
 
@@ -547,8 +547,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 *)
@@ -564,7 +564,7 @@ Proof.
 - (* Msetstack *)
   unfold store_stack in H.
   assert (Val.lessdef (rs src) (rs0 (preg_of src))). eapply preg_val; eauto.
-  exploit Mem.storev_extends; eauto. intros [m2' [A B]]. 
+  exploit Mem.storev_extends; eauto. intros [m2' [A B]].
   left; eapply exec_straight_steps; eauto.
   rewrite (sp_val _ _ _ AG) in A. intros. simpl in TR.
   exploit storeind_correct; eauto with asmgen. intros [rs' [P Q]].
@@ -574,11 +574,11 @@ Proof.
 
 - (* 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.
@@ -587,63 +587,63 @@ Opaque loadind.
   exploit loadind_correct. eexact EQ.
   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 with asmgen.
-  simpl; intros. rewrite R; auto with asmgen. 
+  simpl; intros. rewrite R; auto with asmgen.
   apply preg_of_not_R12; auto.
 (* GPR11 does not contain parent *)
   exploit loadind_int_correct. eexact A. instantiate (1 := IR12). intros [rs1 [P [Q R]]].
-  exploit loadind_correct. eexact EQ. instantiate (2 := rs1). rewrite Q. eauto. intros [rs2 [S [T U]]]. 
+  exploit loadind_correct. eexact EQ. instantiate (2 := rs1). rewrite Q. eauto. intros [rs2 [S [T U]]].
   exists rs2; split. eapply exec_straight_trans; eauto.
   split. eapply agree_set_mreg. eapply agree_set_mreg. eauto. eauto.
   instantiate (1 := rs1#IR12 <- (rs2#IR12)). intros.
   rewrite Pregmap.gso; auto with asmgen.
-  congruence. intros. unfold Pregmap.set. destruct (PregEq.eq r' IR12). congruence. auto with asmgen. 
-  simpl; intros. rewrite U; auto with asmgen. 
+  congruence. intros. unfold Pregmap.set. destruct (PregEq.eq r' IR12). congruence. auto with asmgen.
+  simpl; intros. rewrite U; auto with asmgen.
   apply preg_of_not_R12; 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]]].
   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 with asmgen.
-  simpl. destruct op; try congruence. destruct ep; simpl; try congruence. intros. 
+  simpl. destruct op; try congruence. destruct ep; simpl; try congruence. intros.
   rewrite R; auto. apply preg_of_not_R12; auto. exact I.
 
 - (* 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. 
+  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 (fn_code tf) <= Int.max_unsigned).
     eapply transf_function_no_overflow; eauto.
   destruct ros as [rf|fid]; simpl in H; monadInv H5.
@@ -659,23 +659,23 @@ 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. eauto.
-  econstructor; eauto. 
+  econstructor; eauto.
   econstructor; eauto.
   eapply agree_sp_def; eauto.
-  simpl. eapply agree_exten; eauto. intros. Simpl. 
+  simpl. eapply agree_exten; eauto. intros. Simpl.
   Simpl. rewrite <- H2. auto.
 + (* Direct call *)
   generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1.
   assert (TCA: transl_code_at_pc ge (Vptr fb (Int.add ofs Int.one)) fb f c false tf x).
-    econstructor; eauto. 
+    econstructor; eauto.
   exploit return_address_offset_correct; eauto. intros; subst ra.
   left; econstructor; split.
   apply plus_one. eapply exec_step_internal. eauto.
-  eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
+  eapply functions_transl; eauto. eapply find_instr_tail; eauto.
   simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. eauto.
-  econstructor; eauto. 
+  econstructor; eauto.
   econstructor; eauto.
   eapply agree_sp_def; eauto.
   simpl. eapply agree_exten; eauto. intros. Simpl.
@@ -692,7 +692,7 @@ Opaque loadind.
   unfold chunk_of_type. rewrite (sp_val _ _ _ AG). 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]].
   assert (X: forall k, exists rs2,
     exec_straight tge tf
        (loadind_int IR13 (fn_retaddr_ofs f) IR14
@@ -702,13 +702,13 @@ Opaque loadind.
     /\ rs2#RA = parent_ra s
     /\ forall r, if_preg r = true -> r <> SP -> r <> IR14 -> rs2#r = rs0#r).
   {
-    intros. 
-    exploit loadind_int_correct. eexact C. intros [rs1 [P [Q R]]]. 
+    intros.
+    exploit loadind_int_correct. eexact C. intros [rs1 [P [Q R]]].
     econstructor; split.
-    eapply exec_straight_trans. eexact P. apply exec_straight_one. 
-    simpl. rewrite R; auto with asmgen. unfold chunk_of_type in A. rewrite A. 
-    rewrite <- (sp_val _ _ _ AG). rewrite E. eauto. auto. 
-    split. Simpl. split. Simpl. intros. Simpl. 
+    eapply exec_straight_trans. eexact P. apply exec_straight_one.
+    simpl. rewrite R; auto with asmgen. unfold chunk_of_type in A. rewrite A.
+    rewrite <- (sp_val _ _ _ AG). rewrite E. eauto. auto.
+    split. Simpl. split. Simpl. intros. Simpl.
   }
   destruct ros as [rf|fid]; simpl in H; monadInv H7.
 + (* Indirect call *)
@@ -718,45 +718,45 @@ Opaque loadind.
   assert (rs0 x0 = Vptr f' Int.zero).
     exploit ireg_val; eauto. rewrite H7; intros LD; inv LD; auto.
   destruct (X (Pbreg x0 sig :: x)) as [rs2 [P [Q [R S]]]].
-  exploit exec_straight_steps_2. eexact P. eauto. eauto. eapply functions_transl; eauto. eauto. 
+  exploit exec_straight_steps_2. eexact P. eauto. eauto. eapply functions_transl; eauto. eauto.
   intros [ofs' [Y Z]].
   left; econstructor; split.
-  eapply plus_right'. eapply exec_straight_exec; eauto. 
-  econstructor. eauto. eapply functions_transl; eauto. 
-  eapply find_instr_tail; eauto. 
-  simpl. reflexivity. 
+  eapply plus_right'. eapply exec_straight_exec; eauto.
+  econstructor. eauto. eapply functions_transl; eauto.
+  eapply find_instr_tail; eauto.
+  simpl. reflexivity.
   traceEq.
-  econstructor; eauto. 
-  split. Simpl. eapply parent_sp_def; eauto. 
-  intros. Simpl. rewrite S; auto with asmgen. eapply preg_val; eauto. 
+  econstructor; eauto.
+  split. Simpl. eapply parent_sp_def; eauto.
+  intros. Simpl. rewrite S; auto with asmgen. eapply preg_val; eauto.
   Simpl. rewrite S; auto with asmgen.
   rewrite <- (ireg_of_eq _ _ EQ1); auto with asmgen.
   rewrite <- (ireg_of_eq _ _ EQ1); auto with asmgen.
 + (* Direct call *)
   destruct (X (Pbsymb fid sig :: x)) as [rs2 [P [Q [R S]]]].
-  exploit exec_straight_steps_2. eexact P. eauto. eauto. eapply functions_transl; eauto. eauto. 
+  exploit exec_straight_steps_2. eexact P. eauto. eauto. eapply functions_transl; eauto. eauto.
   intros [ofs' [Y Z]].
   left; econstructor; split.
-  eapply plus_right'. eapply exec_straight_exec; eauto. 
-  econstructor. eauto. eapply functions_transl; eauto. 
-  eapply find_instr_tail; eauto. 
-  simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. reflexivity. 
+  eapply plus_right'. eapply exec_straight_exec; eauto.
+  econstructor. eauto. eapply functions_transl; eauto.
+  eapply find_instr_tail; eauto.
+  simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. reflexivity.
   traceEq.
   econstructor; eauto.
-  split. Simpl. eapply parent_sp_def; eauto. 
-  intros. Simpl. rewrite S; auto with asmgen. eapply preg_val; eauto. 
+  split. Simpl. eapply parent_sp_def; eauto.
+  intros. Simpl. rewrite S; auto with asmgen. eapply preg_val; eauto.
 
 - (* 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.
@@ -770,12 +770,12 @@ Opaque loadind.
   rewrite preg_notin_charact. intros. auto with asmgen.
   auto with asmgen.
   apply agree_nextinstr. eapply agree_set_res; auto.
-  eapply agree_undef_regs; eauto. intros; apply undef_regs_other_2; auto. 
+  eapply agree_undef_regs; eauto. intros; apply undef_regs_other_2; auto.
   congruence.
 
 - (* Mgoto *)
   assert (f0 = f) by congruence. subst f0.
-  inv AT. monadInv H4. 
+  inv AT. monadInv H4.
   exploit find_label_goto_label; eauto. intros [tc' [rs' [GOTO [AT2 INV]]]].
   left; exists (State rs' m'); split.
   apply plus_one. econstructor; eauto.
@@ -793,9 +793,9 @@ Opaque loadind.
   intros. simpl in TR.
   destruct (transl_cond_correct tge tf cond args _ rs0 m' _ TR) as [rs' [A [B C]]].
   rewrite EC in B. destruct B as [Bpos Bneg].
-  econstructor; econstructor; econstructor; split. eexact A. 
+  econstructor; econstructor; econstructor; split. eexact A.
   split. eapply agree_undef_regs; eauto with asmgen.
-  simpl. rewrite Bpos. reflexivity. 
+  simpl. rewrite Bpos. reflexivity.
 
 - (* Mcond false *)
   exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
@@ -803,7 +803,7 @@ Opaque loadind.
   destruct (transl_cond_correct tge tf cond args _ rs0 m' _ TR) as [rs' [A [B C]]].
   rewrite EC in B. destruct B as [Bpos Bneg].
   econstructor; split.
-  eapply exec_straight_trans. eexact A. 
+  eapply exec_straight_trans. eexact A.
   apply exec_straight_one. simpl. rewrite Bpos. reflexivity. auto.
   split. eapply agree_undef_regs; eauto with asmgen.
   intros; Simpl.
@@ -811,32 +811,32 @@ 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. eauto.
-  instantiate (2 := rs0#IR14 <- Vundef). 
+  instantiate (2 := rs0#IR14 <- Vundef).
   Simpl. eauto.
-  eauto. 
+  eauto.
   intros [tc' [rs' [A [B C]]]].
   exploit ireg_val; eauto. rewrite H. intros LD; inv LD.
   left; econstructor; split.
-  apply plus_one. econstructor; eauto. 
-  eapply find_instr_tail; eauto. 
+  apply plus_one. econstructor; eauto.
+  eapply find_instr_tail; eauto.
   simpl. rewrite <- H9. unfold Mach.label in H0; unfold label; rewrite H0. eexact A.
-  econstructor; eauto. 
-  eapply agree_undef_regs; eauto. intros. rewrite C; auto with asmgen. Simpl. 
+  econstructor; eauto.
+  eapply agree_undef_regs; eauto. intros. rewrite C; auto with asmgen. Simpl.
   congruence.
 
 - (* Mreturn *)
   assert (f0 = f) by congruence. subst f0.
-  inversion AT; subst. 
+  inversion AT; subst.
   assert (NOOV: list_length_z (fn_code tf) <= 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.
@@ -849,40 +849,40 @@ Opaque loadind.
     /\ rs2#RA = parent_ra s
     /\ forall r, if_preg r = true -> r <> SP -> r <> IR14 -> rs2#r = rs0#r).
   {
-    intros. 
-    exploit loadind_int_correct. eexact C. intros [rs1 [P [Q R]]]. 
+    intros.
+    exploit loadind_int_correct. eexact C. intros [rs1 [P [Q R]]].
     econstructor; split.
-    eapply exec_straight_trans. eexact P. apply exec_straight_one. 
-    simpl. rewrite R; auto with asmgen. rewrite A. 
-    rewrite <- (sp_val _ _ _ AG). rewrite E. eauto. auto. 
+    eapply exec_straight_trans. eexact P. apply exec_straight_one.
+    simpl. rewrite R; auto with asmgen. rewrite A.
+    rewrite <- (sp_val _ _ _ AG). rewrite E. eauto. auto.
     split. Simpl.
     split. Simpl.
-    intros. Simpl. 
+    intros. Simpl.
   }
   destruct (X (Pbreg IR14 (Mach.fn_sig f) :: x)) as [rs2 [P [Q [R S]]]].
-  exploit exec_straight_steps_2. eexact P. eauto. eauto. eapply functions_transl; eauto. eauto. 
+  exploit exec_straight_steps_2. eexact P. eauto. eauto. eapply functions_transl; eauto. eauto.
   intros [ofs' [Y Z]].
   left; econstructor; split.
-  eapply plus_right'. eapply exec_straight_exec; eauto. 
-  econstructor. eauto. eapply functions_transl; eauto. 
-  eapply find_instr_tail; eauto. 
+  eapply plus_right'. eapply exec_straight_exec; eauto.
+  econstructor. eauto. eapply functions_transl; eauto.
+  eapply find_instr_tail; eauto.
   simpl. reflexivity.
   traceEq.
-  econstructor; eauto. 
+  econstructor; eauto.
   split. Simpl. eapply parent_sp_def; eauto.
   intros. Simpl. rewrite S; auto with asmgen. eapply preg_val; eauto.
 
 - (* internal function *)
   exploit functions_translated; eauto. intros [tf [A B]]. monadInv B.
-  generalize EQ; intros EQ'. monadInv EQ'. 
+  generalize EQ; intros EQ'. monadInv EQ'.
   destruct (zlt Int.max_unsigned (list_length_z (fn_code x0))); inversion EQ1. clear EQ1.
-  monadInv EQ0. 
-  unfold store_stack in *. 
-  exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. 
+  monadInv EQ0.
+  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]].
   (* Execution of function prologue *)
   set (rs2 := nextinstr (rs0#IR12 <- (parent_sp s) #IR13 <- (Vptr stk Int.zero))).
@@ -894,34 +894,34 @@ Opaque loadind.
   rewrite <- H5 at 2; unfold fn_code.
   apply exec_straight_two with rs2 m2'.
   unfold exec_instr. rewrite C. fold sp.
-  rewrite <- (sp_val _ _ _ AG). unfold chunk_of_type in F. rewrite F. auto. 
+  rewrite <- (sp_val _ _ _ AG). unfold chunk_of_type in F. rewrite F. auto.
   simpl. auto.
-  simpl. unfold exec_store. change (rs2 IR14) with (rs0 IR14). 
+  simpl. unfold exec_store. change (rs2 IR14) with (rs0 IR14).
   rewrite Int.add_zero_l. simpl. unfold chunk_of_type in P. simpl in P.
-  rewrite Int.add_zero_l in P. rewrite ATLR. rewrite P. auto. auto. auto. 
+  rewrite Int.add_zero_l in P. rewrite ATLR. rewrite P. auto. auto. auto.
   left; exists (State rs3 m3'); split.
-  eapply exec_straight_steps_1; eauto. omega. constructor. 
-  econstructor; eauto. 
+  eapply exec_straight_steps_1; eauto. omega. constructor.
+  econstructor; eauto.
   change (rs3 PC) with (Val.add (Val.add (rs0 PC) Vone) Vone).
   rewrite ATPC. simpl. constructor; eauto.
-  subst x. eapply code_tail_next_int. omega. 
-  eapply code_tail_next_int. omega. constructor. 
+  subst x. eapply code_tail_next_int. omega.
+  eapply code_tail_next_int. omega. constructor.
   unfold rs3, rs2.
   apply agree_nextinstr. apply agree_nextinstr.
-  eapply agree_change_sp. 
+  eapply agree_change_sp.
   apply agree_undef_regs with rs0; eauto.
   intros. Simpl. congruence.
 
 - (* 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.
   apply agree_set_other; auto with asmgen.
@@ -946,20 +946,20 @@ Proof.
   econstructor; eauto.
   constructor.
   apply Mem.extends_refl.
-  split. auto. simpl. unfold Vzero; congruence. intros. rewrite Regmap.gi. auto. 
-  unfold Genv.symbol_address. 
+  split. auto. simpl. unfold Vzero; congruence. intros. rewrite Regmap.gi. auto.
+  unfold Genv.symbol_address.
   rewrite (transform_partial_program_main _ _ TRANSF).
-  rewrite symbols_preserved. 
+  rewrite symbols_preserved.
   unfold ge; rewrite H1. auto.
 Qed.
 
 Lemma transf_final_states:
-  forall st1 st2 r, 
+  forall st1 st2 r,
   match_states st1 st2 -> Mach.final_state st1 r -> Asm.final_state st2 r.
 Proof.
   intros. inv H0. inv H. inv STACKS. constructor.
-  auto. 
-  compute in H1. inv H1. 
+  auto.
+  compute in H1. inv H1.
   generalize (preg_val _ _ _ R0 AG). rewrite H2. intros LD; inv LD. auto.
 Qed.
 
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index f0a698eb..3e222ba4 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -51,7 +51,7 @@ Hint Resolve ireg_of_not_R14': asmgen.
 Lemma nextinstr_nf_pc:
   forall rs, (nextinstr_nf rs)#PC = Val.add rs#PC Vone.
 Proof.
-  intros. reflexivity. 
+  intros. reflexivity.
 Qed.
 
 Definition if_preg (r: preg) : bool :=
@@ -83,7 +83,7 @@ Qed.
 Lemma nextinstr_nf_inv1:
   forall r rs, data_preg r = true -> (nextinstr_nf rs)#r = rs#r.
 Proof.
-  intros. destruct r; reflexivity || discriminate. 
+  intros. destruct r; reflexivity || discriminate.
 Qed.
 
 (** Useful simplification tactic *)
@@ -143,14 +143,14 @@ Proof.
   auto.
   predSpec Int.eq Int.eq_spec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero.
   auto.
-  simpl. rewrite IHN. rewrite Int.add_assoc. decEq. rewrite Int.add_and. 
+  simpl. rewrite IHN. rewrite Int.add_assoc. decEq. rewrite Int.add_and.
   rewrite Int.or_not_self. apply Int.and_mone. apply Int.and_not_self.
 Qed.
 
 Remark decompose_int_arm_nil:
   forall N n p, decompose_int_arm N n p = nil -> n = Int.zero.
 Proof.
-  intros. generalize (decompose_int_arm_or N n p Int.zero). rewrite H. simpl. 
+  intros. generalize (decompose_int_arm_or N n p Int.zero). rewrite H. simpl.
   rewrite Int.or_commut; rewrite Int.or_zero; auto.
 Qed.
 
@@ -189,14 +189,14 @@ Proof.
   auto.
   predSpec Int.eq Int.eq_spec (Int.and n (Int.shl Int.one p)) Int.zero.
   auto.
-  simpl. rewrite IHN. rewrite Int.add_assoc. decEq. rewrite Int.add_and. 
+  simpl. rewrite IHN. rewrite Int.add_assoc. decEq. rewrite Int.add_and.
   rewrite Int.or_not_self. apply Int.and_mone. apply Int.and_not_self.
 Qed.
 
 Remark decompose_int_thumb_nil:
   forall N n p, decompose_int_thumb N n p = nil -> n = Int.zero.
 Proof.
-  intros. generalize (decompose_int_thumb_or N n p Int.zero). rewrite H. simpl. 
+  intros. generalize (decompose_int_thumb_or N n p Int.zero). rewrite H. simpl.
   rewrite Int.or_commut; rewrite Int.or_zero; auto.
 Qed.
 
@@ -219,16 +219,16 @@ Proof.
     rewrite IHl. rewrite DISTR. decEq. decEq. auto.
   intros. unfold decompose_int, decompose_int_base.
   destruct (thumb tt); [destruct (is_immed_arith_thumb_special n)|].
-- reflexivity. 
+- reflexivity.
 - destruct (decompose_int_thumb 24%nat n Int.zero) eqn:DB.
   + simpl. exploit decompose_int_thumb_nil; eauto. congruence.
   + simpl. rewrite B. decEq.
-    generalize (DECOMP2 24%nat n Int.zero Int.zero). 
+    generalize (DECOMP2 24%nat n Int.zero Int.zero).
     rewrite DB; simpl. rewrite ! ZERO. auto.
 - destruct (decompose_int_arm 12%nat n Int.zero) eqn:DB.
   + simpl. exploit decompose_int_arm_nil; eauto. congruence.
   + simpl. rewrite B. decEq.
-    generalize (DECOMP1 12%nat n Int.zero Int.zero). 
+    generalize (DECOMP1 12%nat n Int.zero Int.zero).
     rewrite DB; simpl. rewrite ! ZERO. auto.
 Qed.
 
@@ -240,7 +240,7 @@ Proof.
   intros. rewrite Val.or_assoc. auto.
   apply Int.or_assoc.
   intros. rewrite Int.or_commut. apply Int.or_zero.
-  apply decompose_int_arm_or. apply decompose_int_thumb_or. 
+  apply decompose_int_arm_or. apply decompose_int_thumb_or.
 Qed.
 
 Lemma decompose_int_bic:
@@ -259,7 +259,7 @@ Lemma decompose_int_xor:
   List.fold_left (fun v i => Val.xor v (Vint i)) (decompose_int n) v = Val.xor v (Vint n).
 Proof.
   intros. apply decompose_int_general with (f := fun v n => Val.xor v (Vint n)) (g := Int.xor).
-  intros. rewrite Val.xor_assoc. auto. 
+  intros. rewrite Val.xor_assoc. auto.
   apply Int.xor_assoc.
   intros. rewrite Int.xor_commut. apply Int.xor_zero.
   apply decompose_int_arm_xor. apply decompose_int_thumb_xor.
@@ -270,10 +270,10 @@ Lemma decompose_int_add:
   List.fold_left (fun v i => Val.add v (Vint i)) (decompose_int n) v = Val.add v (Vint n).
 Proof.
   intros. apply decompose_int_general with (f := fun v n => Val.add v (Vint n)) (g := Int.add).
-  intros. rewrite Val.add_assoc. auto. 
+  intros. rewrite Val.add_assoc. auto.
   apply Int.add_assoc.
   intros. rewrite Int.add_commut. apply Int.add_zero.
-  apply decompose_int_arm_add. apply decompose_int_thumb_add. 
+  apply decompose_int_arm_add. apply decompose_int_thumb_add.
 Qed.
 
 Lemma decompose_int_sub:
@@ -281,11 +281,11 @@ Lemma decompose_int_sub:
   List.fold_left (fun v i => Val.sub v (Vint i)) (decompose_int n) v = Val.sub v (Vint n).
 Proof.
   intros. apply decompose_int_general with (f := fun v n => Val.sub v (Vint n)) (g := Int.add).
-  intros. repeat rewrite Val.sub_add_opp. rewrite Val.add_assoc. decEq. simpl. decEq. 
+  intros. repeat rewrite Val.sub_add_opp. rewrite Val.add_assoc. decEq. simpl. decEq.
   rewrite Int.neg_add_distr; auto.
   apply Int.add_assoc.
   intros. rewrite Int.add_commut. apply Int.add_zero.
-  apply decompose_int_arm_add. apply decompose_int_thumb_add. 
+  apply decompose_int_arm_add. apply decompose_int_thumb_add.
 Qed.
 
 Lemma iterate_op_correct:
@@ -311,16 +311,16 @@ Proof.
   split. apply exec_straight_one. rewrite SEM1. reflexivity. reflexivity.
   intuition Simpl.
   (* inductive case *)
-  intros. 
-  rewrite List.map_app. simpl. rewrite app_ass. simpl. 
+  intros.
+  rewrite List.map_app. simpl. rewrite app_ass. simpl.
   destruct (H (op2 (SOimm x) :: k)) as [rs' [A [B C]]].
   econstructor.
   split. eapply exec_straight_trans. eexact A. apply exec_straight_one.
   rewrite SEM2. reflexivity. reflexivity.
-  split. rewrite fold_left_app; simpl. Simpl. rewrite B. auto. 
+  split. rewrite fold_left_app; simpl. Simpl. rewrite B. auto.
   intros; Simpl.
 Qed.
-  
+
 (** Loading a constant. *)
 
 Lemma loadimm_correct:
@@ -335,28 +335,28 @@ Proof.
   set (l2 := length (decompose_int (Int.not n))).
   destruct (NPeano.leb l1 1%nat).
 { (* single mov *)
-  econstructor; split. apply exec_straight_one. simpl; reflexivity. auto. 
+  econstructor; split. apply exec_straight_one. simpl; reflexivity. auto.
   split; intros; Simpl. }
   destruct (NPeano.leb l2 1%nat).
 { (* single movn *)
   econstructor; split. apply exec_straight_one.
-  simpl. rewrite Int.not_involutive. reflexivity. auto. 
+  simpl. rewrite Int.not_involutive. reflexivity. auto.
   split; intros; Simpl. }
   destruct (thumb tt).
 { (* movw / movt *)
   unfold loadimm_thumb. destruct (Int.eq (Int.shru n (Int.repr 16)) Int.zero).
   econstructor; split.
-  apply exec_straight_one. simpl; eauto. auto. split; intros; Simpl. 
+  apply exec_straight_one. simpl; eauto. auto. split; intros; Simpl.
   econstructor; split.
   eapply exec_straight_two. simpl; reflexivity. simpl; reflexivity. auto. auto.
-  split; intros; Simpl. simpl. f_equal. rewrite Int.zero_ext_and by omega. 
+  split; intros; Simpl. simpl. f_equal. rewrite Int.zero_ext_and by omega.
   rewrite Int.and_assoc. change 65535 with (two_p 16 - 1). rewrite Int.and_idem.
-  apply Int.same_bits_eq; intros. 
+  apply Int.same_bits_eq; intros.
   rewrite Int.bits_or, Int.bits_and, Int.bits_shl, Int.testbit_repr by auto.
   rewrite Int.Ztestbit_two_p_m1 by omega. change (Int.unsigned (Int.repr 16)) with 16.
   destruct (zlt i 16).
   rewrite andb_true_r, orb_false_r; auto.
-  rewrite andb_false_r; simpl. rewrite Int.bits_shru by omega. 
+  rewrite andb_false_r; simpl. rewrite Int.bits_shru by omega.
   change (Int.unsigned (Int.repr 16)) with 16. rewrite zlt_true by omega. f_equal; omega.
 }
   destruct (NPeano.leb l1 l2).
@@ -388,8 +388,8 @@ Proof.
   intros. unfold addimm.
   destruct (Int.ltu (Int.repr (-256)) n).
   (* sub *)
-  econstructor; split. apply exec_straight_one; simpl; auto. 
-  split; intros; Simpl. apply Val.sub_opp_add. 
+  econstructor; split. apply exec_straight_one; simpl; auto.
+  split; intros; Simpl. apply Val.sub_opp_add.
   destruct (NPeano.leb (length (decompose_int n)) (length (decompose_int (Int.neg n)))).
   (* add - add* *)
   replace (Val.add (rs r2) (Vint n))
@@ -445,7 +445,7 @@ Proof.
   auto.
   intros. simpl. destruct (rs r2); auto. simpl. rewrite Int.sub_add_opp.
   rewrite Int.add_commut; auto.
-  rewrite decompose_int_add. 
+  rewrite decompose_int_add.
   destruct (rs r2); simpl; auto. rewrite Int.sub_add_opp. rewrite Int.add_commut; auto.
 Qed.
 
@@ -497,14 +497,14 @@ Lemma indexed_memory_access_correct:
     (forall (r: preg), if_preg r = true -> r <> IR14 -> rs1 r = rs r) ->
     exists rs',
     exec_straight ge fn (mk_instr r1 n1 :: k) rs1 m k rs' m' /\ P rs') ->
-  exists rs', 
+  exists rs',
      exec_straight ge fn
         (indexed_memory_access mk_instr mk_immed base n k) rs m
         k rs' m'
   /\ P rs'.
 Proof.
   intros until m'; intros SEM.
-  unfold indexed_memory_access. 
+  unfold indexed_memory_access.
   destruct (Int.eq n (mk_immed n)).
 - apply SEM; auto.
 - destruct (addimm_correct IR14 base (Int.sub n (mk_immed n)) (mk_instr IR14 (mk_immed n) :: k) rs m)
@@ -512,10 +512,10 @@ Proof.
   destruct (SEM IR14 rs1 (mk_immed n) k) as (rs2 & D & E).
   rewrite B. rewrite Val.add_assoc. f_equal. simpl.
   rewrite Int.sub_add_opp. rewrite Int.add_assoc.
-  rewrite (Int.add_commut (Int.neg (mk_immed n))). 
+  rewrite (Int.add_commut (Int.neg (mk_immed n))).
   rewrite Int.add_neg_zero. rewrite Int.add_zero. auto.
-  auto with asmgen. 
-  exists rs2; split; auto. eapply exec_straight_trans; eauto. 
+  auto with asmgen.
+  exists rs2; split; auto. eapply exec_straight_trans; eauto.
 Qed.
 
 Lemma loadind_int_correct:
@@ -527,7 +527,7 @@ Lemma loadind_int_correct:
   /\ forall r, if_preg r = true -> r <> IR14 -> r <> dst -> rs'#r = rs#r.
 Proof.
   intros; unfold loadind_int. apply indexed_memory_access_correct; intros.
-  econstructor; split. 
+  econstructor; split.
   apply exec_straight_one. simpl. unfold exec_load. rewrite H0; rewrite H; eauto. auto.
   split; intros; Simpl.
 Qed.
@@ -543,26 +543,26 @@ Lemma loadind_correct:
 Proof.
   unfold loadind; intros. destruct ty; destruct (preg_of dst); inv H; simpl in H0.
 - (* int *)
-  apply loadind_int_correct; auto. 
+  apply loadind_int_correct; auto.
 - (* float *)
   apply indexed_memory_access_correct; intros.
-  econstructor; split. 
-  apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto. 
+  econstructor; split.
+  apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto.
   split; intros; Simpl.
 - (* single *)
   apply indexed_memory_access_correct; intros.
-  econstructor; split. 
-  apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto. 
+  econstructor; split.
+  apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto.
   split; intros; Simpl.
 - (* any32 *)
   apply indexed_memory_access_correct; intros.
-  econstructor; split. 
-  apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto. 
+  econstructor; split.
+  apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto.
   split; intros; Simpl.
 - (* any64 *)
   apply indexed_memory_access_correct; intros.
-  econstructor; split. 
-  apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto. 
+  econstructor; split.
+  apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto.
   split; intros; Simpl.
 Qed.
 
@@ -581,32 +581,32 @@ Proof.
   destruct ty; destruct (preg_of src); inv H; simpl in H0.
 - (* int *)
   apply indexed_memory_access_correct; intros.
-  econstructor; split. 
-  apply exec_straight_one. simpl. unfold exec_store. 
+  econstructor; split.
+  apply exec_straight_one. simpl. unfold exec_store.
   rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. auto.
   intros; Simpl.
 - (* float *)
   apply indexed_memory_access_correct; intros.
-  econstructor; split. 
-  apply exec_straight_one. simpl. unfold exec_store. 
+  econstructor; split.
+  apply exec_straight_one. simpl. unfold exec_store.
   rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. auto.
   intros; Simpl.
 - (* single *)
   apply indexed_memory_access_correct; intros.
-  econstructor; split. 
-  apply exec_straight_one. simpl. unfold exec_store. 
+  econstructor; split.
+  apply exec_straight_one. simpl. unfold exec_store.
   rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. auto.
   intros; Simpl.
 - (* any32 *)
   apply indexed_memory_access_correct; intros.
-  econstructor; split. 
-  apply exec_straight_one. simpl. unfold exec_store. 
+  econstructor; split.
+  apply exec_straight_one. simpl. unfold exec_store.
   rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. auto.
   intros; Simpl.
 - (* any64 *)
   apply indexed_memory_access_correct; intros.
-  econstructor; split. 
-  apply exec_straight_one. simpl. unfold exec_store. 
+  econstructor; split.
+  apply exec_straight_one. simpl. unfold exec_store.
   rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. auto.
   intros; Simpl.
 Qed.
@@ -639,19 +639,19 @@ Lemma compare_int_inv:
   forall r', data_preg r' = true -> rs1#r' = rs#r'.
 Proof.
   intros. unfold rs1, compare_int.
-  repeat Simplif. 
+  repeat Simplif.
 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:
@@ -660,8 +660,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.
 
@@ -677,8 +677,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.
 
@@ -733,16 +733,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).
@@ -780,7 +780,7 @@ Proof.
   assert (nextinstr (rs#CN <- Vundef #CZ <- Vundef #CC <- Vundef #CV <- Vundef) r' = rs r').
   { repeat Simplif. }
   destruct v1; destruct v2; auto.
-  repeat Simplif. 
+  repeat Simplif.
 Qed.
 
 Lemma compare_float_nextpc:
@@ -797,7 +797,7 @@ Lemma cond_for_float_cmp_correct:
   Some(Float.cmp c n1 n2).
 Proof.
   intros.
-  generalize (compare_float_spec rs n1 n2). 
+  generalize (compare_float_spec rs n1 n2).
   set (rs' := nextinstr (compare_float rs (Vfloat n1) (Vfloat n2))).
   intros [A [B [C D]]].
   unfold eval_testcond. rewrite A; rewrite B; rewrite C; rewrite D.
@@ -809,7 +809,7 @@ Proof.
 (* lt *)
   destruct (Float.cmp Clt n1 n2); auto.
 (* le *)
-  rewrite Float.cmp_le_lt_eq. 
+  rewrite Float.cmp_le_lt_eq.
   destruct (Float.cmp Clt n1 n2); destruct (Float.cmp Ceq n1 n2); auto.
 (* gt *)
   destruct (Float.cmp Ceq n1 n2) eqn:EQ;
@@ -819,7 +819,7 @@ Proof.
   exfalso; eapply Float.cmp_gt_eq_false; eauto.
   exfalso; eapply Float.cmp_lt_gt_false; eauto.
 (* ge *)
-  rewrite Float.cmp_ge_gt_eq. 
+  rewrite Float.cmp_ge_gt_eq.
   destruct (Float.cmp Ceq n1 n2) eqn:EQ;
   destruct (Float.cmp Clt n1 n2) eqn:LT;
   destruct (Float.cmp Cgt n1 n2) eqn:GT; auto.
@@ -847,7 +847,7 @@ Proof.
 (* lt *)
   destruct (Float.cmp Clt n1 n2); auto.
 (* le *)
-  rewrite Float.cmp_le_lt_eq. 
+  rewrite Float.cmp_le_lt_eq.
   destruct (Float.cmp Clt n1 n2) eqn:LT; destruct (Float.cmp Ceq n1 n2) eqn:EQ; auto.
 (* gt *)
   destruct (Float.cmp Ceq n1 n2) eqn:EQ;
@@ -857,7 +857,7 @@ Proof.
   exfalso; eapply Float.cmp_gt_eq_false; eauto.
   exfalso; eapply Float.cmp_lt_gt_false; eauto.
 (* ge *)
-  rewrite Float.cmp_ge_gt_eq. 
+  rewrite Float.cmp_ge_gt_eq.
   destruct (Float.cmp Ceq n1 n2) eqn:EQ;
   destruct (Float.cmp Clt n1 n2) eqn:LT;
   destruct (Float.cmp Cgt n1 n2) eqn:GT; auto.
@@ -886,7 +886,7 @@ Proof.
   assert (nextinstr (rs#CN <- Vundef #CZ <- Vundef #CC <- Vundef #CV <- Vundef) r' = rs r').
   { repeat Simplif. }
   destruct v1; destruct v2; auto.
-  repeat Simplif. 
+  repeat Simplif.
 Qed.
 
 Lemma compare_float32_nextpc:
@@ -903,7 +903,7 @@ Lemma cond_for_float32_cmp_correct:
   Some(Float32.cmp c n1 n2).
 Proof.
   intros.
-  generalize (compare_float32_spec rs n1 n2). 
+  generalize (compare_float32_spec rs n1 n2).
   set (rs' := nextinstr (compare_float32 rs (Vsingle n1) (Vsingle n2))).
   intros [A [B [C D]]].
   unfold eval_testcond. rewrite A; rewrite B; rewrite C; rewrite D.
@@ -915,7 +915,7 @@ Proof.
 (* lt *)
   destruct (Float32.cmp Clt n1 n2); auto.
 (* le *)
-  rewrite Float32.cmp_le_lt_eq. 
+  rewrite Float32.cmp_le_lt_eq.
   destruct (Float32.cmp Clt n1 n2); destruct (Float32.cmp Ceq n1 n2); auto.
 (* gt *)
   destruct (Float32.cmp Ceq n1 n2) eqn:EQ;
@@ -925,7 +925,7 @@ Proof.
   exfalso; eapply Float32.cmp_gt_eq_false; eauto.
   exfalso; eapply Float32.cmp_lt_gt_false; eauto.
 (* ge *)
-  rewrite Float32.cmp_ge_gt_eq. 
+  rewrite Float32.cmp_ge_gt_eq.
   destruct (Float32.cmp Ceq n1 n2) eqn:EQ;
   destruct (Float32.cmp Clt n1 n2) eqn:LT;
   destruct (Float32.cmp Cgt n1 n2) eqn:GT; auto.
@@ -953,7 +953,7 @@ Proof.
 (* lt *)
   destruct (Float32.cmp Clt n1 n2); auto.
 (* le *)
-  rewrite Float32.cmp_le_lt_eq. 
+  rewrite Float32.cmp_le_lt_eq.
   destruct (Float32.cmp Clt n1 n2) eqn:LT; destruct (Float32.cmp Ceq n1 n2) eqn:EQ; auto.
 (* gt *)
   destruct (Float32.cmp Ceq n1 n2) eqn:EQ;
@@ -963,7 +963,7 @@ Proof.
   exfalso; eapply Float32.cmp_gt_eq_false; eauto.
   exfalso; eapply Float32.cmp_lt_gt_false; eauto.
 (* ge *)
-  rewrite Float32.cmp_ge_gt_eq. 
+  rewrite Float32.cmp_ge_gt_eq.
   destruct (Float32.cmp Ceq n1 n2) eqn:EQ;
   destruct (Float32.cmp Clt n1 n2) eqn:LT;
   destruct (Float32.cmp Cgt n1 n2) eqn:GT; auto.
@@ -998,14 +998,14 @@ Lemma transl_cond_correct:
      end
   /\ forall r, data_preg r = true -> rs'#r = rs r.
 Proof.
-  intros until c; intros TR. 
+  intros until c; intros TR.
   unfold transl_cond in TR; destruct cond; ArgsInv.
 - (* Ccomp *)
   econstructor.
   split. apply exec_straight_one. simpl. eauto. auto.
   split. destruct (Val.cmp_bool c0 (rs x) (rs x0)) eqn:CMP; auto.
   split; apply cond_for_signed_cmp_correct; auto. rewrite Val.negate_cmp_bool, CMP; auto.
-  apply compare_int_inv. 
+  apply compare_int_inv.
 - (* Ccompu *)
   econstructor.
   split. apply exec_straight_one. simpl. eauto. auto.
@@ -1030,17 +1030,17 @@ Proof.
   destruct (is_immed_arith i).
   econstructor.
   split. apply exec_straight_one. simpl. eauto. auto.
-  split. destruct (Val.cmp_bool c0 (rs x) (Vint i)) eqn:CMP; auto. 
+  split. destruct (Val.cmp_bool c0 (rs x) (Vint i)) eqn:CMP; auto.
   split; apply cond_for_signed_cmp_correct; auto. rewrite Val.negate_cmp_bool, CMP; auto.
   apply compare_int_inv.
   exploit (loadimm_correct IR14). intros [rs' [P [Q R]]].
   econstructor.
   split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl.
   rewrite Q. rewrite R; eauto with asmgen. auto.
-  split. rewrite <- R by (eauto with asmgen). 
+  split. rewrite <- R by (eauto with asmgen).
   destruct (Val.cmp_bool c0 (rs' x) (Vint i)) eqn:CMP; auto.
   split; apply cond_for_signed_cmp_correct; auto. rewrite Val.negate_cmp_bool, CMP; auto.
-  intros. rewrite compare_int_inv by auto. auto with asmgen. 
+  intros. rewrite compare_int_inv by auto. auto with asmgen.
 - (* Ccompuimm *)
   destruct (is_immed_arith i).
   econstructor.
@@ -1052,17 +1052,17 @@ Proof.
   econstructor.
   split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl.
   rewrite Q. rewrite R; eauto with asmgen. auto.
-  split. rewrite <- R by (eauto with asmgen). 
+  split. rewrite <- R by (eauto with asmgen).
   destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs' x) (Vint i)) eqn:CMP; auto.
   split; apply cond_for_unsigned_cmp_correct; auto. rewrite Val.negate_cmpu_bool, CMP; auto.
-  intros. rewrite compare_int_inv by auto. auto with asmgen. 
+  intros. rewrite compare_int_inv by auto. auto with asmgen.
 - (* Ccompf *)
   econstructor.
   split. apply exec_straight_one. simpl. eauto. apply compare_float_nextpc.
   split. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) eqn:CMP; auto.
   destruct (rs x); try discriminate. destruct (rs x0); try discriminate.
   simpl in CMP. inv CMP.
-  split. apply cond_for_float_cmp_correct. apply cond_for_float_not_cmp_correct. 
+  split. apply cond_for_float_cmp_correct. apply cond_for_float_not_cmp_correct.
   apply compare_float_inv.
 - (* Cnotcompf *)
   econstructor.
@@ -1080,7 +1080,7 @@ Local Opaque compare_float. simpl.
   split. destruct (Val.cmpf_bool c0 (rs x) (Vfloat Float.zero)) eqn:CMP; auto.
   destruct (rs x); try discriminate.
   simpl in CMP. inv CMP.
-  split. apply cond_for_float_cmp_correct. apply cond_for_float_not_cmp_correct. 
+  split. apply cond_for_float_cmp_correct. apply cond_for_float_not_cmp_correct.
   apply compare_float_inv.
 - (* Cnotcompfzero *)
   econstructor.
@@ -1096,7 +1096,7 @@ Local Opaque compare_float. simpl.
   split. apply exec_straight_one. simpl. eauto. apply compare_float32_nextpc.
   split. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) eqn:CMP; auto.
   destruct (rs x); try discriminate. destruct (rs x0); try discriminate.
-  simpl in CMP. inv CMP. 
+  simpl in CMP. inv CMP.
   split. apply cond_for_float32_cmp_correct. apply cond_for_float32_not_cmp_correct.
   apply compare_float32_inv.
 - (* Cnotcompfs *)
@@ -1144,7 +1144,7 @@ Lemma transl_op_correct_same:
   /\ rs'#(preg_of res) = v
   /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs'#r = rs#r.
 Proof.
-  intros until v; intros TR EV NOCMP. 
+  intros until v; intros TR EV NOCMP.
   unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; inv EV; try (TranslOpSimpl; fail).
   (* Omove *)
   destruct (preg_of res) eqn:RES; try discriminate;
@@ -1152,12 +1152,12 @@ Proof.
   econstructor; split. apply exec_straight_one; simpl; eauto. intuition Simpl.
   econstructor; split. apply exec_straight_one; simpl; eauto. intuition Simpl.
   (* Ointconst *)
-  generalize (loadimm_correct x i k rs m). intros [rs' [A [B C]]]. 
-  exists rs'; auto with asmgen. 
+  generalize (loadimm_correct x i k rs m). intros [rs' [A [B C]]].
+  exists rs'; auto with asmgen.
   (* Oaddrstack *)
-  generalize (addimm_correct x IR13 i k rs m). 
+  generalize (addimm_correct x IR13 i k rs m).
   intros [rs' [EX [RES OTH]]].
-  exists rs'; auto with asmgen. 
+  exists rs'; auto with asmgen.
   (* Ocast8signed *)
   destruct (thumb tt).
   econstructor; split. apply exec_straight_one; simpl; eauto. intuition Simpl.
@@ -1165,12 +1165,12 @@ Proof.
   set (rs1 := nextinstr_nf (rs#x <- (Val.shl rs#x0 (Vint (Int.repr 24))))).
   set (rs2 := nextinstr_nf (rs1#x <- (Val.shr rs1#x (Vint (Int.repr 24))))).
   exists rs2.
-  split. apply exec_straight_two with rs1 m; auto. 
+  split. apply exec_straight_two with rs1 m; auto.
   split. unfold rs2; Simpl. unfold rs1; Simpl.
-  unfold Val.shr, Val.shl; destruct (rs x0); auto. 
+  unfold Val.shr, Val.shl; destruct (rs x0); auto.
   change (Int.ltu (Int.repr 24) Int.iwordsize) with true; simpl.
   f_equal. symmetry. apply (Int.sign_ext_shr_shl 8). compute; auto.
-  intros. unfold rs2, rs1; Simpl. 
+  intros. unfold rs2, rs1; Simpl.
   (* Ocast16signed *)
   destruct (thumb tt).
   econstructor; split. apply exec_straight_one; simpl; eauto. intuition Simpl.
@@ -1178,15 +1178,15 @@ Proof.
   set (rs1 := nextinstr_nf (rs#x <- (Val.shl rs#x0 (Vint (Int.repr 16))))).
   set (rs2 := nextinstr_nf (rs1#x <- (Val.shr rs1#x (Vint (Int.repr 16))))).
   exists rs2.
-  split. apply exec_straight_two with rs1 m; auto. 
+  split. apply exec_straight_two with rs1 m; auto.
   split. unfold rs2; Simpl. unfold rs1; Simpl.
-  unfold Val.shr, Val.shl; destruct (rs x0); auto. 
+  unfold Val.shr, Val.shl; destruct (rs x0); auto.
   change (Int.ltu (Int.repr 16) Int.iwordsize) with true; simpl.
   f_equal. symmetry. apply (Int.sign_ext_shr_shl 16). compute; auto.
-  intros. unfold rs2, rs1; Simpl. 
+  intros. unfold rs2, rs1; Simpl.
   (* Oaddimm *)
   generalize (addimm_correct x x0 i k rs m).
-  intros [rs' [A [B C]]]. 
+  intros [rs' [A [B C]]].
   exists rs'; auto with asmgen.
   (* Orsbimm *)
   generalize (rsubimm_correct x x0 i k rs m).
@@ -1195,44 +1195,44 @@ Proof.
   (* divs *)
 Local Transparent destroyed_by_op.
   econstructor. split. apply exec_straight_one. simpl. rewrite H0. reflexivity. auto.
-  split. Simpl. simpl; intros. intuition Simpl. 
+  split. Simpl. simpl; intros. intuition Simpl.
   (* divu *)
   econstructor. split. apply exec_straight_one. simpl. rewrite H0. reflexivity. auto.
-  split. Simpl. simpl; intros. intuition Simpl. 
+  split. Simpl. simpl; intros. intuition Simpl.
   (* Oandimm *)
-  generalize (andimm_correct x x0 i k rs m). 
-  intros [rs' [A [B C]]]. 
+  generalize (andimm_correct x x0 i k rs m).
+  intros [rs' [A [B C]]].
   exists rs'; auto with asmgen.
   (* Oorimm *)
   generalize (orimm_correct x x0 i k rs m).
-  intros [rs' [A [B C]]]. 
+  intros [rs' [A [B C]]].
   exists rs'; auto with asmgen.
   (* Oxorimm *)
   generalize (xorimm_correct x x0 i k rs m).
-  intros [rs' [A [B C]]]. 
+  intros [rs' [A [B C]]].
   exists rs'; auto with asmgen.
   (* Oshrximm *)
-  destruct (rs x0) eqn: X0; simpl in H0; try discriminate. 
-  destruct (Int.ltu i (Int.repr 31)) eqn: LTU; inv H0. 
-  revert EQ2. predSpec Int.eq Int.eq_spec i Int.zero; intros EQ2. 
+  destruct (rs x0) eqn: X0; simpl in H0; try discriminate.
+  destruct (Int.ltu i (Int.repr 31)) eqn: LTU; inv H0.
+  revert EQ2. predSpec Int.eq Int.eq_spec i Int.zero; intros EQ2.
   (* i = 0 *)
-  inv EQ2. econstructor. 
-  split. apply exec_straight_one. simpl. reflexivity. auto. 
-  split. Simpl. unfold Int.shrx. rewrite Int.shl_zero. unfold Int.divs. 
+  inv EQ2. econstructor.
+  split. apply exec_straight_one. simpl. reflexivity. auto.
+  split. Simpl. unfold Int.shrx. rewrite Int.shl_zero. unfold Int.divs.
   change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed. auto.
-  intros. Simpl. 
+  intros. Simpl.
   (* i <> 0 *)
   inv EQ2.
   assert (LTU': Int.ltu (Int.sub Int.iwordsize i) Int.iwordsize = true).
   {
     generalize (Int.ltu_inv _ _ LTU). intros.
-    unfold Int.sub, Int.ltu. rewrite Int.unsigned_repr_wordsize. 
+    unfold Int.sub, Int.ltu. rewrite Int.unsigned_repr_wordsize.
     rewrite Int.unsigned_repr. apply zlt_true.
-    assert (Int.unsigned i <> 0). 
+    assert (Int.unsigned i <> 0).
     { red; intros; elim H. rewrite <- (Int.repr_unsigned i). rewrite H1; reflexivity. }
-    omega. 
+    omega.
     change (Int.unsigned (Int.repr 31)) with (Int.zwordsize - 1) in H0.
-    generalize Int.wordsize_max_unsigned; omega. 
+    generalize Int.wordsize_max_unsigned; omega.
   }
   assert (LTU'': Int.ltu i Int.iwordsize = true).
   {
@@ -1250,16 +1250,16 @@ Local Transparent destroyed_by_op.
   simpl. rewrite X0; reflexivity.
   simpl. f_equal. Simpl. replace (rs1 x0) with (rs x0). rewrite X0; reflexivity.
   unfold rs1; Simpl.
-  reflexivity. 
+  reflexivity.
   auto. auto. auto.
-  split. unfold rs3; Simpl. unfold rs2; Simpl. unfold rs1; Simpl. 
-  simpl. change (Int.ltu (Int.repr 31) Int.iwordsize) with true. simpl. 
-  rewrite LTU'; simpl. rewrite LTU''; simpl. 
-  f_equal. symmetry. apply Int.shrx_shr_2. assumption. 
-  intros. unfold rs3; Simpl. unfold rs2; Simpl. unfold rs1; Simpl. 
+  split. unfold rs3; Simpl. unfold rs2; Simpl. unfold rs1; Simpl.
+  simpl. change (Int.ltu (Int.repr 31) Int.iwordsize) with true. simpl.
+  rewrite LTU'; simpl. rewrite LTU''; simpl.
+  f_equal. symmetry. apply Int.shrx_shr_2. assumption.
+  intros. unfold rs3; Simpl. unfold rs2; Simpl. unfold rs1; Simpl.
   (* intoffloat *)
   econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto.
-Transparent destroyed_by_op. 
+Transparent destroyed_by_op.
   simpl. intuition Simpl.
   (* intuoffloat *)
   econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto.
@@ -1295,21 +1295,21 @@ Lemma transl_op_correct:
   /\ Val.lessdef v rs'#(preg_of res)
   /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs'#r = rs#r.
 Proof.
-  intros. 
+  intros.
   assert (EITHER: match op with Ocmp _ => False | _ => True end \/ exists cmp, op = Ocmp cmp).
     destruct op; auto. right; exists c0; auto.
-  destruct EITHER as [A | [cmp A]]. 
+  destruct EITHER as [A | [cmp A]].
   exploit transl_op_correct_same; eauto. intros [rs' [P [Q R]]].
-  subst v. exists rs'; eauto. 
+  subst v. exists rs'; eauto.
   (* Ocmp *)
-  subst op. simpl in H. monadInv H. simpl in H0. inv H0. 
+  subst op. simpl in H. monadInv H. simpl in H0. inv H0.
   rewrite (ireg_of_eq _ _ EQ).
   exploit transl_cond_correct; eauto. instantiate (1 := rs). instantiate (1 := m). intros [rs1 [A [B C]]].
   econstructor; split.
   eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto.
   split; intros; Simpl.
   destruct (eval_condition cmp rs ## (preg_of ## args) m) as [b|]; simpl; auto.
-  destruct B as [B1 B2]; rewrite B1. destruct b; auto. 
+  destruct B as [B1 B2]; rewrite B1. destruct b; auto.
 Qed.
 
 (** Translation of loads and stores. *)
@@ -1352,7 +1352,7 @@ Proof.
   simpl. erewrite ! ireg_of_eq; eauto.
   (* Aindexed2shift *)
   destruct mk_instr_gen as [mk | ]; monadInv TR. apply MK2.
-  erewrite ! ireg_of_eq; eauto. rewrite transl_shift_correct. auto. 
+  erewrite ! ireg_of_eq; eauto. rewrite transl_shift_correct. auto.
   (* Ainstack *)
   inv TR. apply indexed_memory_access_correct. exact MK1.
 Qed.
@@ -1370,13 +1370,13 @@ Lemma transl_load_int_correct:
    /\ rs'#(preg_of dst) = v
    /\ forall r, data_preg r = true -> r <> preg_of dst -> rs'#r = rs#r.
 Proof.
-  intros. monadInv H. erewrite ireg_of_eq by eauto.  
+  intros. monadInv H. erewrite ireg_of_eq by eauto.
   eapply transl_memory_access_correct; eauto.
-  intros; simpl. econstructor; split. apply exec_straight_one. 
+  intros; simpl. econstructor; split. apply exec_straight_one.
   rewrite H2. unfold exec_load. simpl eval_shift_op. rewrite H. rewrite H1. eauto. auto.
-  split. Simpl. intros; Simpl. 
-  simpl; intros. 
-  econstructor; split. apply exec_straight_one. 
+  split. Simpl. intros; Simpl.
+  simpl; intros.
+  econstructor; split. apply exec_straight_one.
   rewrite H2. unfold exec_load. rewrite H. rewrite H1. eauto. auto.
   split. Simpl. intros; Simpl.
 Qed.
@@ -1394,9 +1394,9 @@ Lemma transl_load_float_correct:
    /\ rs'#(preg_of dst) = v
    /\ forall r, data_preg r = true -> r <> preg_of dst -> rs'#r = rs#r.
 Proof.
-  intros. monadInv H. erewrite freg_of_eq by eauto.  
+  intros. monadInv H. erewrite freg_of_eq by eauto.
   eapply transl_memory_access_correct; eauto.
-  intros; simpl. econstructor; split. apply exec_straight_one. 
+  intros; simpl. econstructor; split. apply exec_straight_one.
   rewrite H2. unfold exec_load. rewrite H. rewrite H1. eauto. auto.
   split. Simpl. intros; Simpl.
   simpl; auto.
@@ -1415,14 +1415,14 @@ Lemma transl_store_int_correct:
    /\ forall r, data_preg r = true -> preg_notin r mr -> rs'#r = rs#r.
 Proof.
   intros. assert (DR: data_preg (preg_of src) = true) by eauto with asmgen.
-  monadInv H. erewrite ireg_of_eq in * by eauto.  
+  monadInv H. erewrite ireg_of_eq in * by eauto.
   eapply transl_memory_access_correct; eauto.
-  intros; simpl. econstructor; split. apply exec_straight_one. 
-  rewrite H2. unfold exec_store. simpl eval_shift_op. rewrite H. rewrite H3; eauto with asmgen. 
+  intros; simpl. econstructor; split. apply exec_straight_one.
+  rewrite H2. unfold exec_store. simpl eval_shift_op. rewrite H. rewrite H3; eauto with asmgen.
   rewrite H1. eauto. auto.
   intros; Simpl.
-  simpl; intros. 
-  econstructor; split. apply exec_straight_one. 
+  simpl; intros.
+  econstructor; split. apply exec_straight_one.
   rewrite H2. unfold exec_store. rewrite H. rewrite H1. eauto. auto.
   intros; Simpl.
 Qed.
@@ -1440,9 +1440,9 @@ Lemma transl_store_float_correct:
    /\ forall r, data_preg r = true -> preg_notin r mr -> rs'#r = rs#r.
 Proof.
   intros. assert (DR: data_preg (preg_of src) = true) by eauto with asmgen.
-  monadInv H. erewrite freg_of_eq in * by eauto.  
+  monadInv H. erewrite freg_of_eq in * by eauto.
   eapply transl_memory_access_correct; eauto.
-  intros; simpl. econstructor; split. apply exec_straight_one. 
+  intros; simpl. econstructor; split. apply exec_straight_one.
   rewrite H2. unfold exec_store. rewrite H. rewrite H3; auto with asmgen. rewrite H1. eauto. auto.
   intros; Simpl.
   simpl; auto.
diff --git a/arm/CombineOp.v b/arm/CombineOp.v
index 8da6e3a2..1bcdba22 100644
--- a/arm/CombineOp.v
+++ b/arm/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.
@@ -98,7 +98,7 @@ Function combine_op (op: operation) (args: list valnum) : option(operation * lis
       end
   | Oandimm n, x :: nil =>
       match get x with
-      | Some(Op (Oandimm m) ys) => 
+      | Some(Op (Oandimm m) ys) =>
           Some(let p := Int.and m n in
                if Int.eq p m then (Omove, x :: nil) else (Oandimm p, ys))
       | _ => None
diff --git a/arm/CombineOpproof.v b/arm/CombineOpproof.v
index 485857b9..cb30e956 100644
--- a/arm/CombineOpproof.v
+++ b/arm/CombineOpproof.v
@@ -10,7 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Recognition of combined operations, addressing modes and conditions 
+(** Recognition of combined operations, addressing modes and conditions
   during the [CSE] phase. *)
 
 Require Import Coqlib.
@@ -36,7 +36,7 @@ Hypothesis get_sound: forall v rhs, get v = Some rhs -> rhs_eval_to valu ge sp m
 Lemma get_op_sound:
   forall v op vl, get v = Some (Op op vl) -> eval_operation ge sp op (map valu vl) m = Some (valu v).
 Proof.
-  intros. exploit get_sound; eauto. intros REV; inv REV; auto. 
+  intros. exploit get_sound; eauto. intros REV; inv REV; auto.
 Qed.
 
 Ltac UseGetSound :=
@@ -44,7 +44,7 @@ Ltac UseGetSound :=
   | [ H: get _ = Some _ |- _ ] =>
       let x := fresh "EQ" in (generalize (get_op_sound _ _ _ H); intros x; simpl in x; FuncInv)
   end.
-  
+
 Lemma combine_compimm_ne_0_sound:
   forall x cond args,
   combine_compimm_ne_0 get x = Some(cond, args) ->
@@ -53,7 +53,7 @@ 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.
 Qed.
 
@@ -65,8 +65,8 @@ Lemma combine_compimm_eq_0_sound:
 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. 
+  UseGetSound. rewrite <- H.
+  rewrite eval_negate_condition.
   destruct (eval_condition c (map valu args) m); simpl; auto. destruct b; auto.
 Qed.
 
@@ -78,7 +78,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.
 
@@ -90,7 +90,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.
@@ -126,7 +126,7 @@ Theorem combine_addr_sound:
 Proof.
   intros. functional inversion H; subst.
   (* indexed - addimm *)
-  UseGetSound. simpl. rewrite <- H0. rewrite Val.add_assoc. auto. 
+  UseGetSound. simpl. rewrite <- H0. rewrite Val.add_assoc. auto.
 Qed.
 
 Theorem combine_op_sound:
@@ -149,10 +149,10 @@ Transparent Val.sub.
   destruct v; simpl; auto. repeat rewrite Int.sub_add_opp. rewrite Int.add_assoc.
   rewrite Int.neg_add_distr. decEq. decEq. decEq. apply Int.add_commut.
 (* andimm - andimm *)
-  UseGetSound; simpl. 
-  generalize (Int.eq_spec p m0); rewrite H7; intros. 
+  UseGetSound; simpl.
+  generalize (Int.eq_spec p m0); rewrite H7; intros.
   rewrite <- H0. rewrite Val.and_assoc. simpl. fold p. rewrite H1. auto.
-  UseGetSound; simpl. 
+  UseGetSound; simpl.
   rewrite <- H0. rewrite Val.and_assoc. auto.
 (* orimm - orimm *)
   UseGetSound. simpl. rewrite <- H0. rewrite Val.or_assoc. auto.
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index fa20d17e..6f6afa8a 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -51,7 +51,7 @@ Lemma match_G:
   forall r id ofs,
   AE.get r ae = Ptr(Gl id ofs) -> Val.lessdef rs#r (Genv.symbol_address ge id ofs).
 Proof.
-  intros. apply vmatch_ptr_gl with bc; auto. rewrite <- H. apply MATCH. 
+  intros. apply vmatch_ptr_gl with bc; auto. rewrite <- H. apply MATCH.
 Qed.
 
 Lemma match_S:
@@ -63,9 +63,9 @@ Qed.
 
 Ltac InvApproxRegs :=
   match goal with
-  | [ H: _ :: _ = _ :: _ |- _ ] => 
+  | [ H: _ :: _ = _ :: _ |- _ ] =>
         injection H; clear H; intros; InvApproxRegs
-  | [ H: ?v = AE.get ?r ae |- _ ] => 
+  | [ H: ?v = AE.get ?r ae |- _ ] =>
         generalize (MATCH r); rewrite <- H; clear H; intro; InvApproxRegs
   | _ => idtac
   end.
@@ -86,11 +86,11 @@ Ltac SimplVM :=
       rewrite E in *; clear H; SimplVM
   | [ H: vmatch _ ?v (Ptr(Gl ?id ?ofs)) |- _ ] =>
       let E := fresh in
-      assert (E: Val.lessdef v (Genv.symbol_address ge id ofs)) by (eapply vmatch_ptr_gl; eauto); 
+      assert (E: Val.lessdef v (Genv.symbol_address ge id ofs)) by (eapply vmatch_ptr_gl; eauto);
       clear H; SimplVM
   | [ H: vmatch _ ?v (Ptr(Stk ?ofs)) |- _ ] =>
       let E := fresh in
-      assert (E: Val.lessdef v (Vptr sp ofs)) by (eapply vmatch_ptr_stk; eauto); 
+      assert (E: Val.lessdef v (Vptr sp ofs)) by (eapply vmatch_ptr_stk; eauto);
       clear H; SimplVM
   | _ => idtac
   end.
@@ -114,31 +114,31 @@ Proof.
 - apply Val.swap_cmpu_bool.
 - auto.
 - rewrite eval_static_shift_correct. auto.
-- rewrite eval_static_shift_correct. auto. 
+- rewrite eval_static_shift_correct. auto.
 - destruct (Float.eq_dec n1 Float.zero).
   subst n1. simpl. destruct (rs#r2); simpl; auto. rewrite Float.cmp_swap. auto.
-  simpl. rewrite H1; auto. 
+  simpl. rewrite H1; auto.
 - destruct (Float.eq_dec n2 Float.zero).
   subst n2. simpl. auto.
   simpl. rewrite H1; auto.
 - destruct (Float.eq_dec n1 Float.zero).
   subst n1. simpl. destruct (rs#r2); simpl; auto. rewrite Float.cmp_swap. auto.
-  simpl. rewrite H1; auto. 
+  simpl. rewrite H1; auto.
 - destruct (Float.eq_dec n2 Float.zero); simpl; auto.
   subst n2; auto.
-  rewrite H1; auto. 
+  rewrite H1; auto.
 - destruct (Float32.eq_dec n1 Float32.zero).
   subst n1. simpl. destruct (rs#r2); simpl; auto. rewrite Float32.cmp_swap. auto.
-  simpl. rewrite H1; auto. 
+  simpl. rewrite H1; auto.
 - destruct (Float32.eq_dec n2 Float32.zero).
   subst n2. simpl. auto.
   simpl. rewrite H1; auto.
 - destruct (Float32.eq_dec n1 Float32.zero).
   subst n1. simpl. destruct (rs#r2); simpl; auto. rewrite Float32.cmp_swap. auto.
-  simpl. rewrite H1; auto. 
+  simpl. rewrite H1; auto.
 - destruct (Float32.eq_dec n2 Float32.zero); simpl; auto.
   subst n2; auto.
-  rewrite H1; auto. 
+  rewrite H1; auto.
 - auto.
 Qed.
 
@@ -146,20 +146,20 @@ Lemma make_cmp_base_correct:
   forall c args vl,
   vl = map (fun r => AE.get r ae) args ->
   let (op', args') := make_cmp_base c args vl in
-  exists v, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some v 
+  exists v, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some v
          /\ Val.lessdef (Val.of_optbool (eval_condition c rs##args m)) v.
 Proof.
-  intros. unfold make_cmp_base. 
-  generalize (cond_strength_reduction_correct c args vl H). 
+  intros. unfold make_cmp_base.
+  generalize (cond_strength_reduction_correct c args vl H).
   destruct (cond_strength_reduction c args vl) as [c' args']. intros EQ.
-  econstructor; split. simpl; eauto. rewrite EQ. auto. 
+  econstructor; split. simpl; eauto. rewrite EQ. auto.
 Qed.
 
 Lemma make_cmp_correct:
   forall c args vl,
   vl = map (fun r => AE.get r ae) args ->
   let (op', args') := make_cmp c args vl in
-  exists v, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some v 
+  exists v, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some v
          /\ Val.lessdef (Val.of_optbool (eval_condition c rs##args m)) v.
 Proof.
   intros c args vl.
@@ -168,20 +168,20 @@ Proof.
   { intros. apply vmatch_Uns_1 with bc Ptop. eapply vmatch_ge. eapply vincl_ge; eauto. apply MATCH. }
   unfold make_cmp. case (make_cmp_match c args vl); intros.
 - destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
-  simpl in H; inv H. InvBooleans. subst n. 
+  simpl in H; inv H. InvBooleans. subst n.
   exists (rs#r1); split; auto. simpl.
   exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
   destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
-  simpl in H; inv H. InvBooleans. subst n. 
+  simpl in H; inv H. InvBooleans. subst n.
   exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl.
   exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
   apply make_cmp_base_correct; auto.
 - destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
-  simpl in H; inv H. InvBooleans. subst n. 
+  simpl in H; inv H. InvBooleans. subst n.
   exists (rs#r1); split; auto. simpl.
   exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
   destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
-  simpl in H; inv H. InvBooleans. subst n. 
+  simpl in H; inv H. InvBooleans. subst n.
   exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl.
   exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
   apply make_cmp_base_correct; auto.
@@ -194,7 +194,7 @@ Lemma make_addimm_correct:
   exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.add rs#r (Vint n)) v.
 Proof.
   intros. unfold make_addimm.
-  predSpec Int.eq Int.eq_spec n Int.zero; intros. 
+  predSpec Int.eq Int.eq_spec n Int.zero; intros.
   subst. exists (rs#r); split; auto. destruct (rs#r); simpl; auto; rewrite Int.add_zero; auto.
   exists (Val.add rs#r (Vint n)); auto.
 Qed.
@@ -210,7 +210,7 @@ Proof.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
   exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.shl_zero. auto.
   destruct (Int.ltu n Int.iwordsize) eqn:?; intros.
-  econstructor; split. simpl; eauto.  rewrite mk_shift_amount_eq; auto. 
+  econstructor; split. simpl; eauto.  rewrite mk_shift_amount_eq; auto.
   econstructor; split; eauto. simpl. congruence.
 Qed.
 
@@ -224,7 +224,7 @@ Proof.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
   exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.shr_zero. auto.
   destruct (Int.ltu n Int.iwordsize) eqn:?; intros.
-  econstructor; split. simpl; eauto.  rewrite mk_shift_amount_eq; auto. 
+  econstructor; split. simpl; eauto.  rewrite mk_shift_amount_eq; auto.
   econstructor; split; eauto. simpl. congruence.
 Qed.
 
@@ -238,7 +238,7 @@ Proof.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
   exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.shru_zero. auto.
   destruct (Int.ltu n Int.iwordsize) eqn:?; intros.
-  econstructor; split. simpl; eauto.  rewrite mk_shift_amount_eq; auto. 
+  econstructor; split. simpl; eauto.  rewrite mk_shift_amount_eq; auto.
   econstructor; split; eauto. simpl. congruence.
 Qed.
 
@@ -255,7 +255,7 @@ Proof.
   exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.mul_one; auto.
   destruct (Int.is_power2 n) eqn:?; intros.
   exploit Int.is_power2_range; eauto. intros R.
-  econstructor; split. simpl; eauto. rewrite mk_shift_amount_eq; auto.  
+  econstructor; split. simpl; eauto. rewrite mk_shift_amount_eq; auto.
   rewrite (Val.mul_pow2 rs#r1 _ _ Heqo). auto.
   econstructor; split; eauto. simpl. congruence.
 Qed.
@@ -270,7 +270,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.
@@ -284,8 +284,8 @@ Lemma make_divuimm_correct:
 Proof.
   intros; unfold make_divuimm.
   destruct (Int.is_power2 n) eqn:?.
-  replace v with (Val.shru rs#r1 (Vint i)). 
-  econstructor; split. simpl. rewrite mk_shift_amount_eq. eauto. 
+  replace v with (Val.shru rs#r1 (Vint i)).
+  econstructor; split. simpl. rewrite mk_shift_amount_eq. eauto.
   eapply Int.is_power2_range; eauto. auto.
   eapply Val.divu_pow2; eauto. congruence.
   exists v; auto.
@@ -304,17 +304,17 @@ Proof.
   subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.and_mone; auto.
   destruct (match x with Uns _ k => Int.eq (Int.zero_ext k (Int.not n)) Int.zero
                        | _ => false end) eqn:UNS.
-  destruct x; try congruence. 
+  destruct x; try congruence.
   exists (rs#r); split; auto.
   inv H; auto. simpl. replace (Int.and i n) with i; auto.
   generalize (Int.eq_spec (Int.zero_ext n0 (Int.not n)) Int.zero); rewrite UNS; intro EQ.
   Int.bit_solve. destruct (zlt i0 n0).
   replace (Int.testbit n i0) with (negb (Int.testbit Int.zero i0)).
-  rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto. 
-  rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto. 
-  rewrite Int.bits_not by auto. apply negb_involutive. 
-  rewrite H6 by auto. auto. 
-  econstructor; split; eauto. auto. 
+  rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto.
+  rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto.
+  rewrite Int.bits_not by auto. apply negb_involutive.
+  rewrite H6 by auto. auto.
+  econstructor; split; eauto. auto.
 Qed.
 
 Lemma make_orimm_correct:
@@ -327,7 +327,7 @@ Proof.
   subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.or_zero; auto.
   predSpec Int.eq Int.eq_spec n Int.mone; intros.
   subst n. exists (Vint Int.mone); split; auto. destruct (rs#r); simpl; auto. rewrite Int.or_mone; auto.
-  econstructor; split; eauto. auto. 
+  econstructor; split; eauto. auto.
 Qed.
 
 Lemma make_xorimm_correct:
@@ -340,8 +340,8 @@ Proof.
   subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.xor_zero; auto.
   predSpec Int.eq Int.eq_spec n Int.mone; intros.
   subst n. exists (Val.notint (rs#r)); split. auto.
-  destruct (rs#r); simpl; auto. 
-  econstructor; split; eauto. auto. 
+  destruct (rs#r); simpl; auto.
+  econstructor; split; eauto. auto.
 Qed.
 
 Lemma make_mulfimm_correct:
@@ -350,11 +350,11 @@ Lemma make_mulfimm_correct:
   let (op, args) := make_mulfimm n r1 r1 r2 in
   exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v.
 Proof.
-  intros; unfold make_mulfimm. 
-  destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros. 
+  intros; unfold make_mulfimm.
+  destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros.
   simpl. econstructor; split. eauto. rewrite H; subst n.
-  destruct (rs#r1); simpl; auto. rewrite Float.mul2_add; auto. 
-  simpl. econstructor; split; eauto. 
+  destruct (rs#r1); simpl; auto. rewrite Float.mul2_add; auto.
+  simpl. econstructor; split; eauto.
 Qed.
 
 Lemma make_mulfimm_correct_2:
@@ -363,12 +363,12 @@ Lemma make_mulfimm_correct_2:
   let (op, args) := make_mulfimm n r2 r1 r2 in
   exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v.
 Proof.
-  intros; unfold make_mulfimm. 
-  destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros. 
+  intros; unfold make_mulfimm.
+  destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros.
   simpl. econstructor; split. eauto. rewrite H; subst n.
-  destruct (rs#r2); simpl; auto. rewrite Float.mul2_add; auto. 
-  rewrite Float.mul_commut; auto. 
-  simpl. econstructor; split; eauto. 
+  destruct (rs#r2); simpl; auto. rewrite Float.mul2_add; auto.
+  rewrite Float.mul_commut; auto.
+  simpl. econstructor; split; eauto.
 Qed.
 
 Lemma make_mulfsimm_correct:
@@ -377,11 +377,11 @@ Lemma make_mulfsimm_correct:
   let (op, args) := make_mulfsimm n r1 r1 r2 in
   exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulfs rs#r1 rs#r2) v.
 Proof.
-  intros; unfold make_mulfsimm. 
-  destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros. 
+  intros; unfold make_mulfsimm.
+  destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros.
   simpl. econstructor; split. eauto. rewrite H; subst n.
-  destruct (rs#r1); simpl; auto. rewrite Float32.mul2_add; auto. 
-  simpl. econstructor; split; eauto. 
+  destruct (rs#r1); simpl; auto. rewrite Float32.mul2_add; auto.
+  simpl. econstructor; split; eauto.
 Qed.
 
 Lemma make_mulfsimm_correct_2:
@@ -390,12 +390,12 @@ Lemma make_mulfsimm_correct_2:
   let (op, args) := make_mulfsimm n r2 r1 r2 in
   exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulfs rs#r1 rs#r2) v.
 Proof.
-  intros; unfold make_mulfsimm. 
-  destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros. 
+  intros; unfold make_mulfsimm.
+  destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros.
   simpl. econstructor; split. eauto. rewrite H; subst n.
-  destruct (rs#r2); simpl; auto. rewrite Float32.mul2_add; auto. 
-  rewrite Float32.mul_commut; auto. 
-  simpl. econstructor; split; eauto. 
+  destruct (rs#r2); simpl; auto. rewrite Float32.mul2_add; auto.
+  rewrite Float32.mul_commut; auto.
+  simpl. econstructor; split; eauto.
 Qed.
 
 Lemma make_cast8signed_correct:
@@ -404,8 +404,8 @@ Lemma make_cast8signed_correct:
   let (op, args) := make_cast8signed r x in
   exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 8 rs#r) v.
 Proof.
-  intros; unfold make_cast8signed. destruct (vincl x (Sgn Ptop 8)) eqn:INCL. 
-  exists rs#r; split; auto. 
+  intros; unfold make_cast8signed. destruct (vincl x (Sgn Ptop 8)) eqn:INCL.
+  exists rs#r; split; auto.
   assert (V: vmatch bc rs#r (Sgn Ptop 8)).
   { eapply vmatch_ge; eauto. apply vincl_ge; auto. }
   inv V; simpl; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto.
@@ -418,8 +418,8 @@ Lemma make_cast16signed_correct:
   let (op, args) := make_cast16signed r x in
   exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 16 rs#r) v.
 Proof.
-  intros; unfold make_cast16signed. destruct (vincl x (Sgn Ptop 16)) eqn:INCL. 
-  exists rs#r; split; auto. 
+  intros; unfold make_cast16signed. destruct (vincl x (Sgn Ptop 16)) eqn:INCL.
+  exists rs#r; split; auto.
   assert (V: vmatch bc rs#r (Sgn Ptop 16)).
   { eapply vmatch_ge; eauto. apply vincl_ge; auto. }
   inv V; simpl; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto.
@@ -440,13 +440,13 @@ Proof.
 (* cast8signed *)
   InvApproxRegs; SimplVM; inv H0. apply make_cast16signed_correct; auto.
 (* add *)
-  InvApproxRegs; SimplVM. inv H0. 
+  InvApproxRegs; SimplVM. inv H0.
   fold (Val.add (Vint n1) rs#r2). rewrite Val.add_commut. apply make_addimm_correct.
   InvApproxRegs; SimplVM. inv H0. apply make_addimm_correct.
 (* addshift *)
   InvApproxRegs; SimplVM. inv H0. rewrite eval_static_shift_correct. apply make_addimm_correct.
 (* sub *)
-  InvApproxRegs; SimplVM. inv H0. econstructor; split; eauto. 
+  InvApproxRegs; SimplVM. inv H0. econstructor; split; eauto.
   InvApproxRegs; SimplVM. inv H0. rewrite Val.sub_add_opp. apply make_addimm_correct.
 (* subshift *)
   InvApproxRegs; SimplVM. inv H0. rewrite eval_static_shift_correct. rewrite Val.sub_add_opp. apply make_addimm_correct.
@@ -511,7 +511,7 @@ Proof.
   intros until res. unfold addr_strength_reduction.
   destruct (addr_strength_reduction_match addr args vl); simpl;
   intros VL EA; InvApproxRegs; SimplVM; try (inv EA).
-- rewrite Int.add_zero_l. 
+- rewrite Int.add_zero_l.
   change (Vptr sp (Int.add n1 n2)) with (Val.add (Vptr sp n1) (Vint n2)).
   econstructor; split; eauto. apply Val.add_lessdef; auto.
 - fold (Val.add (Vint n1) rs#r2).  rewrite Int.add_zero_l. rewrite Int.add_commut.
@@ -520,12 +520,12 @@ Proof.
 - fold (Val.add (Vint n1) rs#r2).
   rewrite Val.add_commut. econstructor; split; eauto.
 - econstructor; split; eauto.
-- rewrite eval_static_shift_correct. rewrite Int.add_zero_l. 
+- rewrite eval_static_shift_correct. rewrite Int.add_zero_l.
   change (Vptr sp (Int.add n1 (eval_static_shift s n2)))
     with (Val.add (Vptr sp n1) (Vint (eval_static_shift s n2))).
   econstructor; split; eauto. apply Val.add_lessdef; auto.
-- rewrite eval_static_shift_correct. econstructor; split; eauto. 
-- rewrite Int.add_zero_l. change (Vptr sp (Int.add n1 n)) with (Val.add (Vptr sp n1) (Vint n)). 
+- rewrite eval_static_shift_correct. econstructor; split; eauto.
+- rewrite Int.add_zero_l. change (Vptr sp (Int.add n1 n)) with (Val.add (Vptr sp n1) (Vint n)).
   econstructor; split; eauto. apply Val.add_lessdef; auto.
 - exists res; auto.
 Qed.
diff --git a/arm/Conventions1.v b/arm/Conventions1.v
index ffa441bc..e27a9293 100644
--- a/arm/Conventions1.v
+++ b/arm/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.
@@ -121,25 +121,25 @@ Proof.
 Qed.
 
 Lemma index_int_callee_save_inj:
-  forall r1 r2, 
+  forall r1 r2,
   In r1 int_callee_save_regs ->
   In r2 int_callee_save_regs ->
   r1 <> r2 ->
   index_int_callee_save r1 <> index_int_callee_save r2.
 Proof.
-  intros r1 r2. 
+  intros r1 r2.
   simpl; ElimOrEq; ElimOrEq; unfold index_int_callee_save;
   intros; congruence.
 Qed.
 
 Lemma index_float_callee_save_inj:
-  forall r1 r2, 
+  forall r1 r2,
   In r1 float_callee_save_regs ->
   In r2 float_callee_save_regs ->
   r1 <> r2 ->
   index_float_callee_save r1 <> index_float_callee_save r2.
 Proof.
-  intros r1 r2. 
+  intros r1 r2.
   simpl; ElimOrEq; ElimOrEq; unfold index_float_callee_save;
   intros; congruence.
 Qed.
@@ -155,10 +155,10 @@ 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).
@@ -166,14 +166,14 @@ 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.
@@ -216,9 +216,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.
 
@@ -259,7 +259,7 @@ Qed.
 (** The result locations are caller-save registers *)
 
 Lemma loc_result_caller_save:
-  forall (s: signature) (r: mreg), 
+  forall (s: signature) (r: mreg),
   In r (loc_result s) -> In r destroyed_at_call.
 Proof.
   intros.
@@ -420,7 +420,7 @@ Definition size_arguments (s: signature) : Z :=
       else size_arguments_hf s.(sig_args) 0 0 0
   end.
 
-(** Argument locations are either non-temporary registers or [Outgoing] 
+(** Argument locations are either non-temporary registers or [Outgoing]
   stack slots at nonnegative offsets. *)
 
 Definition loc_argument_acceptable (l: loc) : Prop :=
@@ -432,17 +432,17 @@ Definition loc_argument_acceptable (l: loc) : Prop :=
 
 Remark ireg_param_in_params: forall n, In (ireg_param n) int_param_regs.
 Proof.
-  unfold ireg_param; intros. 
+  unfold ireg_param; intros.
   destruct (list_nth_z int_param_regs n) as [r|] eqn:NTH.
-  eapply list_nth_z_in; eauto. 
+  eapply list_nth_z_in; eauto.
   simpl; auto.
 Qed.
 
 Remark freg_param_in_params: forall n, In (freg_param n) float_param_regs.
 Proof.
-  unfold freg_param; intros. 
+  unfold freg_param; intros.
   destruct (list_nth_z float_param_regs n) as [r|] eqn:NTH.
-  eapply list_nth_z_in; eauto. 
+  eapply list_nth_z_in; eauto.
   simpl; auto.
 Qed.
 
@@ -488,7 +488,7 @@ Proof.
   apply Zle_trans with (align ofs 2). apply align_le; omega. omega.
 - (* long *)
   set (ir' := align ir 2) in *.
-  assert (ofs <= align ofs 2) by (apply align_le; omega). 
+  assert (ofs <= align ofs 2) by (apply align_le; omega).
   destruct (zlt ir' 4).
   destruct H. subst l; left; apply ireg_param_in_params.
   destruct H. subst l; left; apply ireg_param_in_params.
@@ -545,8 +545,8 @@ Proof.
   elim H.
   destruct a.
 - (* int *)
-  destruct H. 
-  destruct (zlt ofs 0); subst l. 
+  destruct H.
+  destruct (zlt ofs 0); subst l.
   left; apply ireg_param_in_params.
   split. xomega. congruence.
   eapply INCR. eapply IHtyl; eauto. omega.
@@ -571,14 +571,14 @@ Proof.
   split. xomega. congruence.
   eapply INCR. eapply IHtyl; eauto. omega.
 - (* single *)
-  destruct H. 
-  destruct (zlt ofs 0); subst l. 
+  destruct H.
+  destruct (zlt ofs 0); subst l.
   right; apply freg_param_in_params.
   split. xomega. congruence.
   eapply INCR. eapply IHtyl; eauto. omega.
 - (* any32 *)
-  destruct H. 
-  destruct (zlt ofs 0); subst l. 
+  destruct H.
+  destruct (zlt ofs 0); subst l.
   left; apply ireg_param_in_params.
   split. xomega. congruence.
   eapply INCR. eapply IHtyl; eauto. omega.
@@ -624,7 +624,7 @@ Proof.
   apply Zle_trans with (align ofs0 2). apply align_le; omega.
   apply Zle_trans with (align ofs0 2 + 2); auto; omega.
   set (ir' := align ir 2).
-  destruct (zlt ir' 4); eauto. 
+  destruct (zlt ir' 4); eauto.
   apply Zle_trans with (align ofs0 2). apply align_le; omega.
   apply Zle_trans with (align ofs0 2 + 2); auto; omega.
   destruct (zlt fr 8); eauto.
@@ -641,7 +641,7 @@ Remark size_arguments_sf_above:
 Proof.
   induction tyl; simpl; intros.
   omega.
-  destruct a; (eapply Zle_trans; [idtac|eauto]). 
+  destruct a; (eapply Zle_trans; [idtac|eauto]).
   xomega.
   assert (ofs0 <= align ofs0 2) by (apply align_le; omega). xomega.
   assert (ofs0 <= align ofs0 2) by (apply align_le; omega). xomega.
@@ -673,17 +673,17 @@ Proof.
   destruct (zlt ir 4); destruct H.
   discriminate.
   eauto.
-  inv H. apply size_arguments_hf_above. 
+  inv H. apply size_arguments_hf_above.
   eauto.
 - (* float *)
   destruct (zlt fr 8); destruct H.
   discriminate.
-  eauto. 
-  inv H. apply size_arguments_hf_above. 
+  eauto.
+  inv H. apply size_arguments_hf_above.
   eauto.
 - (* long *)
   destruct (zlt (align ir 2) 4).
-  destruct H. discriminate. destruct H. discriminate. eauto. 
+  destruct H. discriminate. destruct H. discriminate. eauto.
   destruct H. inv H.
   rewrite <- Zplus_assoc. simpl. apply size_arguments_hf_above.
   destruct H. inv H.
@@ -699,13 +699,13 @@ Proof.
   destruct (zlt ir 4); destruct H.
   discriminate.
   eauto.
-  inv H. apply size_arguments_hf_above. 
+  inv H. apply size_arguments_hf_above.
   eauto.
 - (* any64 *)
   destruct (zlt fr 8); destruct H.
   discriminate.
-  eauto. 
-  inv H. apply size_arguments_hf_above. 
+  eauto.
+  inv H. apply size_arguments_hf_above.
   eauto.
 Qed.
 
@@ -718,28 +718,28 @@ Proof.
   elim H.
   destruct a.
 - (* int *)
-  destruct H. 
-  destruct (zlt ofs0 0); inv H. apply size_arguments_sf_above. 
+  destruct H.
+  destruct (zlt ofs0 0); inv H. apply size_arguments_sf_above.
   eauto.
 - (* float *)
   destruct H.
   destruct (zlt (align ofs0 2) 0); inv H. apply size_arguments_sf_above.
   eauto.
 - (* long *)
-  destruct H. 
+  destruct H.
   destruct (zlt (align ofs0 2) 0); inv H.
   rewrite <- Zplus_assoc. simpl. apply size_arguments_sf_above.
-  destruct H. 
+  destruct H.
   destruct (zlt (align ofs0 2) 0); inv H.
   eapply Zle_trans. 2: apply size_arguments_sf_above. simpl; xomega.
   eauto.
 - (* float *)
-  destruct H. 
-  destruct (zlt ofs0 0); inv H. apply size_arguments_sf_above. 
+  destruct H.
+  destruct (zlt ofs0 0); inv H. apply size_arguments_sf_above.
   eauto.
 - (* any32 *)
-  destruct H. 
-  destruct (zlt ofs0 0); inv H. apply size_arguments_sf_above. 
+  destruct H.
+  destruct (zlt ofs0 0); inv H. apply size_arguments_sf_above.
   eauto.
 - (* any64 *)
   destruct H.
@@ -765,6 +765,6 @@ Qed.
 Lemma loc_arguments_main:
   loc_arguments signature_main = nil.
 Proof.
-  unfold loc_arguments. 
+  unfold loc_arguments.
   destruct Archi.abi; reflexivity.
 Qed.
diff --git a/arm/Machregs.v b/arm/Machregs.v
index f4bd4613..211d2791 100644
--- a/arm/Machregs.v
+++ b/arm/Machregs.v
@@ -21,7 +21,7 @@ Require Import Op.
 (** The following type defines the machine registers that can be referenced
   as locations.  These include:
 - Integer registers that can be allocated to RTL pseudo-registers ([Rxx]).
-- Floating-point registers that can be allocated to RTL pseudo-registers 
+- Floating-point registers that can be allocated to RTL pseudo-registers
   ([Fxx]).
 
   The type [mreg] does not include reserved machine registers
@@ -45,9 +45,9 @@ Global Opaque mreg_eq.
 
 Definition mreg_type (r: mreg): typ :=
   match r with
-  | R0  | R1  | R2  | R3   | R4  | R5  | R6  | R7 
+  | R0  | R1  | R2  | R3   | R4  | R5  | R6  | R7
   | R8  | R9  | R10 | R11  | R12 => Tany32
-  | F0  | F1  | F2  | F3   | F4 | F5   | F6  | F7 
+  | F0  | F1  | F2  | F3   | F4 | F5   | F6  | F7
   | F8  | F9  | F10  | F11 | F12  | F13  | F14  | F15 => Tany64
   end.
 
diff --git a/arm/NeedOp.v b/arm/NeedOp.v
index e91ea64d..41b80941 100644
--- a/arm/NeedOp.v
+++ b/arm/NeedOp.v
@@ -120,7 +120,7 @@ Lemma needs_of_condition_sound:
   vagree_list args args' (needs_of_condition cond) ->
   eval_condition cond args' m' = Some b.
 Proof.
-  intros. unfold needs_of_condition in H0. 
+  intros. unfold needs_of_condition in H0.
   eapply default_needs_of_condition_sound; eauto.
 Qed.
 
@@ -129,10 +129,10 @@ Lemma needs_of_shift_sound:
   vagree v v' (needs_of_shift s nv) ->
   vagree (eval_shift s v) (eval_shift s v') nv.
 Proof.
-  intros. destruct s; simpl in *. 
+  intros. destruct s; simpl in *.
   apply shlimm_sound; auto.
   apply shruimm_sound; auto.
-  apply shrimm_sound; auto. 
+  apply shrimm_sound; auto.
   apply ror_sound; auto.
 Qed.
 
@@ -157,32 +157,32 @@ Proof.
 - apply sign_ext_sound; auto. compute; auto.
 - apply sign_ext_sound; auto. compute; auto.
 - apply add_sound; auto.
-- apply add_sound; auto. apply needs_of_shift_sound; auto. 
+- apply add_sound; auto. apply needs_of_shift_sound; auto.
 - apply add_sound; auto with na.
-- replace (default nv) with All in *. 
-  apply vagree_lessdef. apply val_sub_lessdef; auto with na. 
+- replace (default nv) with All in *.
+  apply vagree_lessdef. apply val_sub_lessdef; auto with na.
   apply lessdef_vagree. apply needs_of_shift_sound; auto with na.
   destruct nv; simpl; congruence.
-- replace (default nv) with All in *. 
-  apply vagree_lessdef. apply val_sub_lessdef; auto with na. 
+- replace (default nv) with All in *.
+  apply vagree_lessdef. apply val_sub_lessdef; auto with na.
   apply lessdef_vagree. apply needs_of_shift_sound; auto with na.
   destruct nv; simpl; congruence.
-- apply mul_sound; auto. 
-- apply add_sound; auto. apply mul_sound; auto. 
+- apply mul_sound; auto.
+- apply add_sound; auto. apply mul_sound; auto.
 - apply and_sound; auto.
-- apply and_sound; auto. apply needs_of_shift_sound; auto. 
+- apply and_sound; auto. apply needs_of_shift_sound; auto.
 - apply andimm_sound; auto.
 - apply or_sound; auto.
-- apply or_sound; auto. apply needs_of_shift_sound; auto. 
+- apply or_sound; auto. apply needs_of_shift_sound; auto.
 - apply orimm_sound; auto.
 - apply xor_sound; auto.
-- apply xor_sound; auto. apply needs_of_shift_sound; auto. 
+- apply xor_sound; auto. apply needs_of_shift_sound; auto.
 - apply xor_sound; auto with na.
-- apply and_sound; auto. apply notint_sound; auto. 
-- apply and_sound; auto. apply notint_sound. apply needs_of_shift_sound; auto. 
-- apply notint_sound; auto. 
+- apply and_sound; auto. apply notint_sound; auto.
+- apply and_sound; auto. apply notint_sound. apply needs_of_shift_sound; auto.
+- apply notint_sound; auto.
 - apply notint_sound. apply needs_of_shift_sound; auto.
-- apply needs_of_shift_sound; auto. 
+- apply needs_of_shift_sound; auto.
 Qed.
 
 Lemma operation_is_redundant_sound:
@@ -195,7 +195,7 @@ Proof.
   intros. destruct op; simpl in *; try discriminate; inv H1; FuncInv; subst.
 - apply sign_ext_redundant_sound; auto. omega.
 - apply sign_ext_redundant_sound; auto. omega.
-- apply andimm_redundant_sound; auto. 
+- apply andimm_redundant_sound; auto.
 - apply orimm_redundant_sound; auto.
 Qed.
 
diff --git a/arm/Op.v b/arm/Op.v
index df39b26a..bc717d7b 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -17,7 +17,7 @@
 - [operation]: arithmetic and logical operations;
 - [addressing]: addressing modes for load and store operations.
 
-  These types are processor-specific and correspond roughly to what the 
+  These types are processor-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
@@ -36,7 +36,7 @@ Require Import Events.
 
 Set Implicit Arguments.
 
-Record shift_amount: Type := 
+Record shift_amount: Type :=
   { s_amount: int;
     s_range: Int.ltu s_amount Int.iwordsize = true }.
 
@@ -141,7 +141,7 @@ Inductive operation : Type :=
 (*c Boolean tests: *)
   | Ocmp: condition -> operation.       (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
 
-(** Addressing modes.  [r1], [r2], etc, are the arguments to the 
+(** Addressing modes.  [r1], [r2], etc, are the arguments to the
   addressing. *)
 
 Inductive addressing: Type :=
@@ -510,15 +510,15 @@ Program Definition mk_shift_amount (n: int) : shift_amount :=
   {| s_amount := Int.modu n Int.iwordsize; s_range := _ |}.
 Next Obligation.
   assert (0 <= Zmod (Int.unsigned n) 32 < 32). apply Z_mod_lt. omega.
-  unfold Int.ltu, Int.modu. change (Int.unsigned Int.iwordsize) with 32. 
-  rewrite Int.unsigned_repr. apply zlt_true. omega. 
+  unfold Int.ltu, Int.modu. change (Int.unsigned Int.iwordsize) with 32.
+  rewrite Int.unsigned_repr. apply zlt_true. omega.
   assert (32 < Int.max_unsigned). compute; auto. omega.
 Qed.
 
 Lemma mk_shift_amount_eq:
   forall n, Int.ltu n Int.iwordsize = true -> s_amount (mk_shift_amount n) = n.
 Proof.
-  intros; simpl. unfold Int.modu. transitivity (Int.repr (Int.unsigned n)). 
+  intros; simpl. unfold Int.modu. transitivity (Int.repr (Int.unsigned n)).
   decEq. apply Zmod_small. apply Int.ltu_inv; auto.
   apply Int.repr_unsigned.
 Qed.
@@ -540,7 +540,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.
 
@@ -576,13 +576,13 @@ Proof.
   repeat (destruct vl; auto). apply Val.negate_cmpu_bool.
   repeat (destruct vl; auto). apply Val.negate_cmp_bool.
   repeat (destruct vl; auto). apply Val.negate_cmpu_bool.
-  repeat (destruct vl; auto). 
+  repeat (destruct vl; auto).
   repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0); auto. destruct b; auto.
-  repeat (destruct vl; auto). 
+  repeat (destruct vl; auto).
   repeat (destruct vl; auto). destruct (Val.cmpf_bool c v (Vfloat Float.zero)); auto. destruct b; auto.
-  repeat (destruct vl; auto). 
+  repeat (destruct vl; auto).
   repeat (destruct vl; auto). destruct (Val.cmpfs_bool c v v0); auto. destruct b; auto.
-  repeat (destruct vl; auto). 
+  repeat (destruct vl; auto).
   repeat (destruct vl; auto). destruct (Val.cmpfs_bool c v (Vsingle Float32.zero)); auto. destruct b; auto.
 Qed.
 
@@ -603,7 +603,7 @@ Definition shift_stack_operation (delta: int) (op: operation) :=
 Lemma type_shift_stack_addressing:
   forall delta addr, type_of_addressing (shift_stack_addressing delta addr) = type_of_addressing addr.
 Proof.
-  intros. destruct addr; auto. 
+  intros. destruct addr; auto.
 Qed.
 
 Lemma type_shift_stack_operation:
@@ -650,7 +650,7 @@ Lemma eval_offset_addressing:
 Proof.
   intros. destruct addr; simpl in H; inv H; simpl in *; FuncInv; subst.
   rewrite Val.add_assoc; auto.
-  rewrite Val.add_assoc. auto. 
+  rewrite Val.add_assoc. auto.
 Qed.
 
 (** Transformation of addressing modes with two operands or more
@@ -750,7 +750,7 @@ Lemma eval_operation_preserved:
   eval_operation ge2 sp op vl m = eval_operation ge1 sp op vl m.
 Proof.
   intros.
-  unfold eval_operation; destruct op; auto. 
+  unfold eval_operation; destruct op; auto.
   unfold Genv.symbol_address. rewrite agree_on_symbols; auto.
 Qed.
 
@@ -826,7 +826,7 @@ Ltac InvInject :=
 Remark eval_shift_inj:
   forall s v v', Val.inject f v v' -> Val.inject f (eval_shift s v) (eval_shift s v').
 Proof.
-  intros. inv H; destruct s; simpl; auto; rewrite s_range; auto. 
+  intros. inv H; destruct s; simpl; auto; rewrite s_range; auto.
 Qed.
 
 Lemma eval_condition_inj:
@@ -887,9 +887,9 @@ Proof.
   apply Values.Val.add_inject; auto. inv H4; inv H2; simpl; auto.
   inv H4; inv H2; simpl; auto.
   inv H4; inv H2; simpl; auto.
-  inv H4; inv H3; simpl in H1; inv H1. simpl. 
+  inv H4; inv H3; simpl in H1; inv H1. simpl.
     destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2. TrivialExists.
-  inv H4; inv H3; simpl in H1; inv H1. simpl. 
+  inv H4; inv H3; simpl in H1; inv H1. simpl.
     destruct (Int.eq i0 Int.zero); inv H2. TrivialExists.
 
   inv H4; inv H2; simpl; auto.
@@ -987,7 +987,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:
@@ -1055,8 +1055,8 @@ Proof.
   apply valid_different_pointers_extends; auto.
   intros. rewrite <- val_inject_lessdef; auto.
   rewrite <- val_inject_lessdef; auto.
-  eauto. auto. 
-  destruct H2 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. 
+  eauto. auto.
+  destruct H2 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto.
 Qed.
 
 Lemma eval_addressing_lessdef:
@@ -1070,10 +1070,10 @@ Proof.
           eval_addressing genv sp addr vl2 = Some v2
           /\ Val.inject (fun b => Some(b, 0)) v1 v2).
   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. 
+  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.
 Qed.
 
 End EVAL_LESSDEF.
@@ -1095,7 +1095,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.
 
@@ -1117,11 +1117,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.
@@ -1136,7 +1136,7 @@ Lemma eval_operation_inject:
      eval_operation genv (Vptr sp2 Int.zero) (shift_stack_operation (Int.repr delta) op) vl2 m2 = Some v2
   /\ Val.inject f v1 v2.
 Proof.
-  intros. 
+  intros.
   rewrite eval_shift_stack_operation. simpl.
   eapply eval_operation_inj with (sp1 := Vptr sp1 Int.zero) (m1 := m1); eauto.
   intros; eapply Mem.valid_pointer_inject_val; eauto.
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index 5f41e754..297e1f64 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -31,7 +31,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.
 
@@ -116,8 +116,8 @@ Theorem eval_addrsymbol:
   forall le id ofs,
   exists v, eval_expr ge sp e m le (addrsymbol id ofs) v /\ Val.lessdef (Genv.symbol_address ge id ofs) v.
 Proof.
-  intros. unfold addrsymbol. econstructor; split. 
-  EvalOp. simpl; eauto. 
+  intros. unfold addrsymbol. econstructor; split.
+  EvalOp. simpl; eauto.
   auto.
 Qed.
 
@@ -126,7 +126,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.
 
@@ -146,14 +146,14 @@ 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.
   unfold Genv.symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. rewrite Int.add_commut; auto.
   rewrite Val.add_assoc. rewrite Int.add_commut. auto.
   subst x. rewrite Val.add_assoc. rewrite Int.add_commut. auto.
-Qed. 
+Qed.
 
 Theorem eval_add: binary_constructor_sound add Val.add.
 Proof.
@@ -161,12 +161,12 @@ Proof.
   unfold add; case (add_match a b); intros; InvEval.
   rewrite Val.add_commut. apply eval_addimm; auto.
   apply eval_addimm; auto.
-  subst. 
+  subst.
   replace (Val.add (Val.add v1 (Vint n1)) (Val.add v0 (Vint n2)))
      with (Val.add (Val.add v1 v0) (Val.add (Vint n1) (Vint n2))).
   apply eval_addimm. EvalOp.
   repeat rewrite Val.add_assoc. decEq. apply Val.add_permut.
-  subst. 
+  subst.
   replace (Val.add (Val.add v1 (Vint n1)) y)
      with (Val.add (Val.add v1 y) (Vint n1)).
   apply eval_addimm. EvalOp.
@@ -174,7 +174,7 @@ Proof.
   subst. rewrite <- Val.add_assoc. apply eval_addimm. EvalOp.
   subst. rewrite Val.add_commut. TrivialExists.
   subst. TrivialExists.
-  subst. TrivialExists. 
+  subst. TrivialExists.
   subst. rewrite Val.add_commut. TrivialExists.
   TrivialExists.
 Qed.
@@ -184,7 +184,7 @@ Proof.
   red; intros until x. unfold rsubimm; case (rsubimm_match a); intros.
   InvEval. TrivialExists.
   InvEval. subst x. econstructor; split. EvalOp. unfold eval_operation; eauto.
-  destruct v1; simpl; auto. rewrite Int.sub_add_r. rewrite <- Int.sub_add_opp. 
+  destruct v1; simpl; auto. rewrite Int.sub_add_r. rewrite <- Int.sub_add_opp.
   auto.
   InvEval. subst x. econstructor; split. EvalOp. simpl; eauto.
   fold (Val.sub (Vint m0) v1). destruct v1; simpl; auto.
@@ -198,7 +198,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.
@@ -211,7 +211,7 @@ Qed.
 
 Theorem eval_negint: unary_constructor_sound negint (fun v => Val.sub Vzero v).
 Proof.
-  red; intros. unfold negint. apply eval_rsubimm; auto. 
+  red; intros. unfold negint. apply eval_rsubimm; auto.
 Qed.
 
 Theorem eval_shlimm:
@@ -227,11 +227,11 @@ Opaque mk_shift_amount.
   InvEval. simpl; rewrite Heqb. TrivialExists.
   destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?.
   InvEval. subst x. exists (Val.shl v1 (Vint (Int.add n n1))); split. EvalOp.
-  simpl. rewrite mk_shift_amount_eq; auto. 
+  simpl. rewrite mk_shift_amount_eq; auto.
   destruct v1; simpl; auto. rewrite s_range. simpl. rewrite Heqb. rewrite Heqb0.
   rewrite Int.add_commut. rewrite Int.shl_shl; auto. apply s_range. rewrite Int.add_commut; auto.
-  TrivialExists. simpl. rewrite mk_shift_amount_eq; auto. 
-  TrivialExists. simpl. rewrite mk_shift_amount_eq; auto. 
+  TrivialExists. simpl. rewrite mk_shift_amount_eq; auto.
+  TrivialExists. simpl. rewrite mk_shift_amount_eq; auto.
   intros; TrivialExists. simpl. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. auto.
 Qed.
 
@@ -247,11 +247,11 @@ Proof.
   InvEval. simpl; rewrite Heqb. TrivialExists.
   destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?.
   InvEval. subst x. exists (Val.shr v1 (Vint (Int.add n n1))); split. EvalOp.
-  simpl. rewrite mk_shift_amount_eq; auto. 
+  simpl. rewrite mk_shift_amount_eq; auto.
   destruct v1; simpl; auto. rewrite s_range. simpl. rewrite Heqb. rewrite Heqb0.
   rewrite Int.add_commut. rewrite Int.shr_shr; auto. apply s_range. rewrite Int.add_commut; auto.
-  TrivialExists. simpl. rewrite mk_shift_amount_eq; auto.  
-  TrivialExists. simpl. rewrite mk_shift_amount_eq; auto. 
+  TrivialExists. simpl. rewrite mk_shift_amount_eq; auto.
+  TrivialExists. simpl. rewrite mk_shift_amount_eq; auto.
   intros; TrivialExists. simpl. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. auto.
 Qed.
 
@@ -267,11 +267,11 @@ Proof.
   InvEval. simpl; rewrite Heqb. TrivialExists.
   destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?.
   InvEval. subst x. exists (Val.shru v1 (Vint (Int.add n n1))); split. EvalOp.
-  simpl. rewrite mk_shift_amount_eq; auto. 
+  simpl. rewrite mk_shift_amount_eq; auto.
   destruct v1; simpl; auto. destruct (Int.ltu n1 Int.iwordsize) eqn:?; simpl; auto.
   rewrite Heqb; rewrite Heqb0. rewrite Int.add_commut. rewrite Int.shru_shru; auto. rewrite Int.add_commut; auto.
-  TrivialExists. simpl. rewrite mk_shift_amount_eq; auto. 
-  TrivialExists. simpl. rewrite mk_shift_amount_eq; auto. 
+  TrivialExists. simpl. rewrite mk_shift_amount_eq; auto.
+  TrivialExists. simpl. rewrite mk_shift_amount_eq; auto.
   intros; TrivialExists. simpl. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. auto.
 Qed.
 
@@ -282,12 +282,12 @@ Proof.
   assert (DFL: exists v, eval_expr ge sp e m le (Eop Omul (Eop (Ointconst n) Enil ::: a ::: Enil)) v /\ Val.lessdef (Val.mul x (Vint n)) v).
   TrivialExists. econstructor. EvalOp. simpl; eauto. econstructor. eauto. constructor.
   rewrite Val.mul_commut. auto.
-  generalize (Int.one_bits_decomp n). 
+  generalize (Int.one_bits_decomp n).
   generalize (Int.one_bits_range n).
   destruct (Int.one_bits n).
   intros. auto.
   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.
@@ -296,13 +296,13 @@ 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 (x :: le)). eexact A1. eexact A2. intros [v [A B]].
-  exists v; split. econstructor; eauto. 
+  exists v; 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. eapply Val.lessdef_trans. 2: eauto. apply Val.add_lessdef; auto.
-  simpl. repeat rewrite H0; auto with coqlib. 
+  simpl. repeat rewrite H0; auto with coqlib.
   intros. auto.
 Qed.
 
@@ -311,18 +311,18 @@ 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.
@@ -331,7 +331,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.
@@ -340,15 +340,15 @@ 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. 
+  intros. exists x; split; auto.
   subst. destruct x; simpl; auto. rewrite Int.and_mone; auto.
   case (andimm_match a); intros.
   InvEval. TrivialExists. simpl. rewrite Int.and_commut; auto.
-  InvEval. subst. rewrite Val.and_assoc. simpl. rewrite Int.and_commut. TrivialExists. 
+  InvEval. subst. rewrite Val.and_assoc. simpl. rewrite Int.and_commut. TrivialExists.
   TrivialExists.
 Qed.
 
@@ -374,11 +374,11 @@ Proof.
   intros. subst. exists x; split; auto.
   destruct x; simpl; auto. rewrite Int.or_zero; auto.
   predSpec Int.eq Int.eq_spec n Int.mone.
-  intros. exists (Vint Int.mone); split. EvalOp. 
+  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.
 
@@ -390,10 +390,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.
 
@@ -406,9 +406,9 @@ Proof.
   destruct (Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2) eqn:?.
   destruct (andb_prop _ _ Heqb0).
   generalize (Int.eq_spec (Int.add n1 n2) Int.iwordsize); rewrite H1; intros.
-  exploit eval_same_expr; eauto. intros [EQ1 EQ2]. subst. 
+  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.
@@ -419,9 +419,9 @@ Proof.
   destruct (Int.eq (Int.add n2 n1) Int.iwordsize && same_expr_pure t1 t2) eqn:?.
   destruct (andb_prop _ _ Heqb0).
   generalize (Int.eq_spec (Int.add n2 n1) Int.iwordsize); rewrite H1; intros.
-  exploit eval_same_expr; eauto. intros [EQ1 EQ2]. subst. 
+  exploit eval_same_expr; eauto. intros [EQ1 EQ2]. subst.
   exists (Val.ror v0 (Vint n1)); 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_commut. rewrite <- Int.or_ror; auto.
@@ -439,15 +439,15 @@ 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.
   predSpec Int.eq Int.eq_spec n Int.mone.
   intros. subst n. rewrite <- Val.not_xor. apply eval_notint; auto.
   intros. destruct (xorimm_match a); intros; InvEval.
   TrivialExists. simpl. rewrite Int.xor_commut; auto.
   subst. rewrite Val.xor_assoc. simpl. rewrite Int.xor_commut. TrivialExists.
-  subst x. rewrite Val.not_xor. rewrite Val.xor_assoc. 
+  subst x. rewrite Val.not_xor. rewrite Val.xor_assoc.
   rewrite (Val.xor_commut (Vint Int.mone)). TrivialExists.
   TrivialExists.
 Qed.
@@ -472,19 +472,19 @@ Lemma eval_mod_aux:
   eval_expr ge sp e m le (mod_aux divop a b) (Val.sub x (Val.mul z y)).
 Proof.
   intros; unfold mod_aux.
-  eapply eval_Elet. eexact H0. eapply eval_Elet. 
+  eapply eval_Elet. eexact H0. eapply eval_Elet.
   apply eval_lift. eexact H1.
-  eapply eval_Eop. eapply eval_Econs. 
+  eapply eval_Eop. eapply eval_Econs.
   eapply eval_Eletvar. simpl; reflexivity.
-  eapply eval_Econs. eapply eval_Eop. 
+  eapply eval_Econs. eapply eval_Eop.
   eapply eval_Econs. eapply eval_Eop.
   eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity.
   eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity.
-  apply eval_Enil.  
+  apply eval_Enil.
   rewrite H. eauto.
   eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity.
-  apply eval_Enil.  
-  simpl; reflexivity. apply eval_Enil. 
+  apply eval_Enil.
+  simpl; reflexivity. apply eval_Enil.
   reflexivity.
 Qed.
 
@@ -505,7 +505,7 @@ Theorem eval_mods_base:
   Val.mods x y = Some z ->
   exists v, eval_expr ge sp e m le (mods_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros; unfold mods_base. 
+  intros; unfold mods_base.
   exploit Val.mods_divs; eauto. intros [v [A B]].
   subst. econstructor; split; eauto.
   apply eval_mod_aux with (semdivop := Val.divs); auto.
@@ -528,7 +528,7 @@ Theorem eval_modu_base:
   Val.modu x y = Some z ->
   exists v, eval_expr ge sp e m le (modu_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros; unfold modu_base. 
+  intros; unfold modu_base.
   exploit Val.modu_divu; eauto. intros [v [A B]].
   subst. econstructor; split; eauto.
   apply eval_mod_aux with (semdivop := Val.divu); auto.
@@ -540,13 +540,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.
@@ -555,39 +555,39 @@ 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.
@@ -600,19 +600,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.
@@ -646,8 +646,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.
@@ -656,13 +656,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.
@@ -670,7 +670,7 @@ 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.
@@ -687,7 +687,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.
@@ -696,9 +696,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.
 
@@ -706,9 +706,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.
 
@@ -766,7 +766,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:
@@ -776,8 +776,8 @@ Theorem eval_floatofint:
   exists v, eval_expr ge sp e m le (floatofint a) v /\ Val.lessdef y v.
 Proof.
   intros until y; unfold floatofint. case (floatofint_match a); intros.
-  InvEval. simpl in H0. TrivialExists. 
-  TrivialExists. 
+  InvEval. simpl in H0. TrivialExists.
+  TrivialExists.
 Qed.
 
 Theorem eval_intuoffloat:
@@ -786,7 +786,7 @@ Theorem eval_intuoffloat:
   Val.intuoffloat x = Some y ->
   exists v, eval_expr ge sp e m le (intuoffloat a) v /\ Val.lessdef y v.
 Proof.
-  intros; unfold intuoffloat. TrivialExists. 
+  intros; unfold intuoffloat. TrivialExists.
 Qed.
 
 Theorem eval_floatofintu:
@@ -796,7 +796,7 @@ Theorem eval_floatofintu:
   exists v, eval_expr ge sp e m le (floatofintu a) v /\ Val.lessdef y v.
 Proof.
   intros until y; unfold floatofintu. case (floatofintu_match a); intros.
-  InvEval. simpl in H0. TrivialExists. 
+  InvEval. simpl in H0. TrivialExists.
   TrivialExists.
 Qed.
 
@@ -806,7 +806,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:
@@ -816,8 +816,8 @@ Theorem eval_singleofint:
   exists v, eval_expr ge sp e m le (singleofint a) v /\ Val.lessdef y v.
 Proof.
   intros until y; unfold singleofint. case (singleofint_match a); intros.
-  InvEval. simpl in H0. TrivialExists. 
-  TrivialExists. 
+  InvEval. simpl in H0. TrivialExists.
+  TrivialExists.
 Qed.
 
 Theorem eval_intuofsingle:
@@ -826,7 +826,7 @@ Theorem eval_intuofsingle:
   Val.intuofsingle x = Some y ->
   exists v, eval_expr ge sp e m le (intuofsingle a) v /\ Val.lessdef y v.
 Proof.
-  intros; unfold intuofsingle. TrivialExists. 
+  intros; unfold intuofsingle. TrivialExists.
 Qed.
 
 Theorem eval_singleofintu:
@@ -836,7 +836,7 @@ Theorem eval_singleofintu:
   exists v, eval_expr ge sp e m le (singleofintu a) v /\ Val.lessdef y v.
 Proof.
   intros until y; unfold singleofintu. case (singleofintu_match a); intros.
-  InvEval. simpl in H0. TrivialExists. 
+  InvEval. simpl in H0. TrivialExists.
   TrivialExists.
 Qed.
 
@@ -846,7 +846,7 @@ Theorem eval_addressing:
   v = Vptr b ofs ->
   match addressing chunk a with (mode, args) =>
     exists vl,
-    eval_exprlist ge sp e m le args vl /\ 
+    eval_exprlist ge sp e m le args vl /\
     eval_addressing ge sp mode vl = Some v
   end.
 Proof.
@@ -872,12 +872,12 @@ 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.
 - inv H. InvEval. simpl in H6. rewrite <- Genv.shift_symbol_address in H6.
-  inv H6. constructor; auto.  
+  inv H6. constructor; auto.
 - constructor; auto.
 Qed.
 
diff --git a/arm/Stacklayout.v b/arm/Stacklayout.v
index 7694dcfe..82d11727 100644
--- a/arm/Stacklayout.v
+++ b/arm/Stacklayout.v
@@ -112,7 +112,7 @@ Proof.
   set (x1 := 4 * bound_outgoing b).
   assert (4 | x1). unfold x1; exists (bound_outgoing b); ring.
   set (x2 := align x1 8).
-  assert (8 | x2). apply align_divides. omega. 
+  assert (8 | x2). apply align_divides. omega.
   set (x3 := x2 + 4 * bound_local b).
   assert (4 | x3). apply Zdivide_plus_r. apply Zdivides_trans with 8; auto. exists 2; auto.
   exists (bound_local b); ring.
@@ -121,10 +121,10 @@ Proof.
   set (x5 := x4 + 8 * bound_float_callee_save b).
   assert (8 | x5). apply Zdivide_plus_r; auto. exists (bound_float_callee_save b); ring.
   assert (4 | x5). apply Zdivides_trans with 8; auto. exists 2; auto.
-  set (x6 := x5 + 4). 
+  set (x6 := x5 + 4).
   assert (4 | x6). apply Zdivide_plus_r; auto. exists 1; auto.
   set (x7 := x6 + 4).
-  assert (8 | x7). unfold x7, x6. replace (x5 + 4 + 4) with (x5 + 8) by omega. 
+  assert (8 | x7). unfold x7, x6. replace (x5 + 4 + 4) with (x5 + 8) by omega.
   apply Zdivide_plus_r; auto. exists 1; auto.
   set (x8 := align (x7 + bound_stack_data b) 8).
   assert (8 | x8). apply align_divides. omega.
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index 04226900..a938725a 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -40,13 +40,13 @@ module type PRINTER_OPTIONS =
 module Target (Opt: PRINTER_OPTIONS) : TARGET =
   struct
 (* Code generation options. *)
-    
+
     let literals_in_code = ref true     (* to be turned into a proper option *)
-    
+
 (* Basic printing functions *)
-        
+
     let print_label oc lbl = elf_label oc (transl_label lbl)
-        
+
     let comment = "@"
 
     let symbol = elf_symbol
@@ -61,34 +61,34 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
       | IR4 -> "r4" | IR5 -> "r5" | IR6 -> "r6" | IR7 -> "r7"
       | IR8 -> "r8" | IR9 -> "r9" | IR10 -> "r10" | IR11 -> "r11"
       | IR12 -> "r12" | IR13 -> "sp" | IR14 -> "lr"
-            
+
     let float_reg_name = function
       | FR0 -> "d0"  | FR1 -> "d1"  | FR2 -> "d2"  | FR3 -> "d3"
       | FR4 -> "d4"  | FR5 -> "d5"  | FR6 -> "d6"  | FR7 -> "d7"
       | FR8 -> "d8"  | FR9 -> "d9"  | FR10 -> "d10"  | FR11 -> "d11"
       | FR12 -> "d12"  | FR13 -> "d13"  | FR14 -> "d14"  | FR15 -> "d15"
-            
+
     let single_float_reg_index = function
       | FR0 -> 0  | FR1 -> 2  | FR2 -> 4  | FR3 -> 6
       | FR4 -> 8  | FR5 -> 10  | FR6 -> 12  | FR7 -> 14
       | FR8 -> 16  | FR9 -> 18  | FR10 -> 20  | FR11 -> 22
       | FR12 -> 24  | FR13 -> 26  | FR14 -> 28  | FR15 -> 30
-            
+
     let single_float_reg_name = function
       | FR0 -> "s0"  | FR1 -> "s2"  | FR2 -> "s4"  | FR3 -> "s6"
       | FR4 -> "s8"  | FR5 -> "s10"  | FR6 -> "s12"  | FR7 -> "s14"
       | FR8 -> "s16"  | FR9 -> "s18"  | FR10 -> "s20"  | FR11 -> "s22"
       | FR12 -> "s24"  | FR13 -> "s26"  | FR14 -> "s28"  | FR15 -> "s30"
-            
+
     let ireg oc r = output_string oc (int_reg_name r)
     let freg oc r = output_string oc (float_reg_name r)
     let freg_single oc r = output_string oc (single_float_reg_name r)
-        
+
     let preg oc = function
       | IR r -> ireg oc r
       | FR r -> freg oc r
       | _    -> assert false
-            
+
     let condition_name = function
       | TCeq -> "eq"
       | TCne -> "ne"
@@ -102,7 +102,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
       | TClt -> "lt"
       | TCgt -> "gt"
       | TCle -> "le"
-            
+
     let neg_condition_name = function
       | TCeq -> "ne"
       | TCne -> "eq"
@@ -116,7 +116,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
       | TClt -> "ge"
       | TCgt -> "le"
       | TCle -> "gt"
-            
+
 (* In Thumb2 mode, some arithmetic instructions have shorter encodings
    if they carry the "S" flag (update condition flags):
        add   (but not sp + imm)
@@ -158,27 +158,27 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
       | Section_debug_abbrev -> ".section	.debug_abbrev,\"\",%progbits"
       | Section_debug_line _ -> ".section	.debug_line,\"\",%progbits"
 
-            
+
     let section oc sec =
       fprintf oc "	%s\n" (name_of_section sec)
-        
+
 (* Record current code position and latest position at which to
    emit float and symbol constants. *)
-        
+
     let currpos = ref 0
     let size_constants = ref 0
     let max_pos_constants = ref max_int
-        
+
     let distance_to_emit_constants () =
       if !literals_in_code
       then !max_pos_constants - (!currpos + !size_constants)
       else max_int
-          
+
 (* Associate labels to floating-point constants and to symbols *)
-          
+
     let float_labels = (Hashtbl.create 39 : (int64, int) Hashtbl.t)
     let float32_labels = (Hashtbl.create 39 : (int32, int) Hashtbl.t)
-        
+
     let label_float bf =
       try
         Hashtbl.find float_labels bf
@@ -188,7 +188,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
         size_constants := !size_constants + 8;
         max_pos_constants := min !max_pos_constants (!currpos + 1024);
         lbl'
-          
+
     let label_float32 bf =
       try
         Hashtbl.find float32_labels bf
@@ -198,10 +198,10 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
         size_constants := !size_constants + 4;
         max_pos_constants := min !max_pos_constants (!currpos + 1024);
         lbl'
-          
+
     let symbol_labels =
       (Hashtbl.create 39 : (ident * Integers.Int.int, int) Hashtbl.t)
-        
+
     let label_symbol id ofs =
       try
         Hashtbl.find symbol_labels (id, ofs)
@@ -211,14 +211,14 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
         size_constants := !size_constants + 4;
         max_pos_constants := min !max_pos_constants (!currpos + 4096);
         lbl'
-          
+
     let reset_constants () =
       Hashtbl.clear float_labels;
       Hashtbl.clear float32_labels;
       Hashtbl.clear symbol_labels;
       size_constants := 0;
       max_pos_constants := max_int
-          
+
     let emit_constants oc =
       fprintf oc "	.balign	4\n";
       Hashtbl.iter
@@ -238,9 +238,9 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
             lbl symbol_offset (id, ofs))
         symbol_labels;
       reset_constants ()
-        
+
 (* Generate code to load the address of id + ofs in register r *)
-        
+
     let loadsymbol oc r id ofs =
       if !Clflags.option_mthumb then begin
         fprintf oc "	movw	%a, #:lower16:%a\n"
@@ -249,13 +249,13 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
           ireg r symbol_offset (id, ofs); 2
       end else begin
         let lbl = label_symbol id ofs in
-        fprintf oc "	ldr	%a, .L%d @ %a\n" 
+        fprintf oc "	ldr	%a, .L%d @ %a\n"
           ireg r lbl symbol_offset (id, ofs); 1
       end
-          
+
 (* Emit instruction sequences that set or offset a register by a constant. *)
 (* No S suffix because they are applied to SP most of the time. *)
-          
+
     let movimm oc dst n =
       match Asmgen.decompose_int n with
       | [] -> assert false
@@ -265,7 +265,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
             (fun n -> fprintf oc "	orr	%s, %s, #%a\n" dst dst coqint n)
             tl;
           List.length l
-            
+
     let addimm oc dst src n =
       match Asmgen.decompose_int n with
       | [] -> assert false
@@ -275,7 +275,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
             (fun n -> fprintf oc "	add	%s, %s, #%a\n" dst dst coqint n)
             tl;
           List.length l
-            
+
     let subimm oc dst src n =
       match Asmgen.decompose_int n with
       | [] -> assert false
@@ -285,27 +285,27 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
             (fun n -> fprintf oc "	sub	%s, %s, #%a\n" dst dst coqint n)
             tl;
           List.length l
-            
+
 (* Recognition of float constants appropriate for VMOV.
    a normalized binary floating point encoding with 1 sign bit, 4
    bits of fraction and a 3-bit exponent *)
-   
+
     let is_immediate_float64 bits =
       let exp = (Int64.(to_int (shift_right_logical bits 52)) land 0x7FF) - 1023 in
       let mant = Int64.logand bits 0xF_FFFF_FFFF_FFFFL in
       exp >= -3 && exp <= 4 && Int64.logand mant 0xF_0000_0000_0000L = mant
-        
+
    let is_immediate_float32 bits =
      let exp = (Int32.(to_int (shift_right_logical bits 23)) land 0xFF) - 127 in
      let mant = Int32.logand bits 0x7F_FFFFl in
      exp >= -3 && exp <= 4 && Int32.logand mant 0x78_0000l = mant
-       
+
 
 (* Emit .file / .loc debugging directives *)
-       
+
     let print_file_line oc file line =
       print_file_line oc comment file line
-        
+
     let print_location oc loc =
       if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc)
 
@@ -456,7 +456,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
       match Opt.float_abi with
       | Soft -> (FixupEABI.fixup_arguments, FixupEABI.fixup_result)
       | Hard -> (FixupHF.fixup_arguments, FixupHF.fixup_result)
-            
+
 (* Printing of instructions *)
 
     let shift_op oc = function
@@ -494,7 +494,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
           fprintf oc "	b	%a\n" symbol id;
           n + 1
       | Pbreg(r, sg) ->
-          let n = 
+          let n =
             if r = IR14
             then fixup_result oc Outgoing sg
             else fixup_arguments oc Outgoing sg in
@@ -886,7 +886,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
             fprintf oc "	.space	%s\n" (Z.to_string n)
       | Init_addrof(symb, ofs) ->
           fprintf oc "	.word	%a\n" symbol_offset (symb, ofs)
-            
+
     let print_prologue oc =
       fprintf oc "	.syntax	unified\n";
       fprintf oc "	.arch	%s\n"
@@ -908,7 +908,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
       end
 
 
-    let print_epilogue oc = 
+    let print_epilogue oc =
       if !Clflags.option_g then begin
         let high_pc = new_label () in
         Debug.add_compilation_section_end ".text" high_pc;
@@ -919,22 +919,22 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
 
 
     let default_falignment = 4
-    
+
     let label = elf_label
-       
+
     let new_label = new_label
   end
 
-let sel_target () = 
+let sel_target () =
   let module S : PRINTER_OPTIONS = struct
-   
+
    let vfpv3 = Configuration.model >= "armv7"
-   
+
    let float_abi = match Configuration.abi with
    | "eabi"      -> Soft
    | "hardfloat" -> Hard
    | _ -> assert false
-   
+
    let hardware_idiv  =
    match  Configuration.model with
    | "armv7r" | "armv7m" -> !Clflags.option_mthumb
diff --git a/arm/ValueAOp.v b/arm/ValueAOp.v
index b388bf12..64a34329 100644
--- a/arm/ValueAOp.v
+++ b/arm/ValueAOp.v
@@ -189,7 +189,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:
@@ -204,7 +204,7 @@ Proof.
   destruct (propagate_float_constants tt); constructor.
   rewrite Int.add_zero_l; eauto with va.
   fold (Val.sub (Vint i) a1). auto with va.
-  apply of_optbool_sound. eapply eval_static_condition_sound; eauto. 
+  apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
 Qed.
 
 End SOUNDNESS.