Updated PR by removing whitespaces. Bug 17450.

1 files changed, 152 insertions, 152 deletions

diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 147132dd..b40ad21b 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -32,7 +32,7 @@ Open Local Scope cminorsel_scope.
 
 (** The following are trivial lemmas and custom tactics that help
   perform backward (inversion) and forward reasoning over the evaluation
-  of operator applications. *)  
+  of operator applications. *)
 
 Ltac EvalOp := eapply eval_Eop; eauto with evalexpr.
 
@@ -117,8 +117,8 @@ Theorem eval_addrsymbol:
   forall le id ofs,
   exists v, eval_expr ge sp e m le (addrsymbol id ofs) v /\ Val.lessdef (Genv.symbol_address ge id ofs) v.
 Proof.
-  intros. unfold addrsymbol. econstructor; split. 
-  EvalOp. simpl; eauto. 
+  intros. unfold addrsymbol. econstructor; split.
+  EvalOp. simpl; eauto.
   auto.
 Qed.
 
@@ -127,7 +127,7 @@ Theorem eval_addrstack:
   exists v, eval_expr ge sp e m le (addrstack ofs) v /\ Val.lessdef (Val.add sp (Vint ofs)) v.
 Proof.
   intros. unfold addrstack. econstructor; split.
-  EvalOp. simpl; eauto. 
+  EvalOp. simpl; eauto.
   auto.
 Qed.
 
@@ -138,20 +138,20 @@ Proof.
   unfold notint; red; intros until x; case (notint_match a); intros; InvEval.
   TrivialExists.
   subst. exists v1; split; auto.
-  subst. TrivialExists. 
+  subst. TrivialExists.
   subst. TrivialExists.
   subst. TrivialExists.
   subst. exists (Val.and v1 v0); split; auto. EvalOp.
   subst. exists (Val.or v1 v0); split; auto. EvalOp.
   subst. exists (Val.xor v1 v0); split; auto. EvalOp.
-  subst. exists (Val.or v0 (Val.notint v1)); split. EvalOp. 
+  subst. exists (Val.or v0 (Val.notint v1)); split. EvalOp.
     destruct v0; destruct v1; simpl; auto. rewrite Int.not_and_or_not. rewrite Int.not_involutive.
     rewrite Int.or_commut. auto.
-  subst. exists (Val.and v0 (Val.notint v1)); split. EvalOp. 
+  subst. exists (Val.and v0 (Val.notint v1)); split. EvalOp.
     destruct v0; destruct v1; simpl; auto. rewrite Int.not_or_and_not. rewrite Int.not_involutive.
     rewrite Int.and_commut. auto.
   subst x. TrivialExists. simpl. rewrite Val.not_xor. rewrite Val.xor_assoc. auto.
-  TrivialExists. 
+  TrivialExists.
 Qed.
 
 Theorem eval_addimm:
@@ -159,7 +159,7 @@ Theorem eval_addimm:
 Proof.
   red; unfold addimm; intros until x.
   predSpec Int.eq Int.eq_spec n Int.zero.
-  subst n. intros. exists x; split; auto. 
+  subst n. intros. exists x; split; auto.
   destruct x; simpl; auto. rewrite Int.add_zero. auto. rewrite Int.add_zero. auto.
   case (addimm_match a); intros; InvEval; simpl; TrivialExists; simpl.
   rewrite Int.add_commut. auto.
@@ -167,15 +167,15 @@ Proof.
   rewrite Val.add_assoc. rewrite Int.add_commut. auto.
   subst. rewrite Val.add_assoc. rewrite Int.add_commut. auto.
   subst. rewrite Int.add_commut. rewrite Genv.shift_symbol_address. rewrite ! Val.add_assoc. f_equal. f_equal. apply Val.add_commut.
-Qed. 
+Qed.
 
 Theorem eval_addsymbol:
   forall s ofs, unary_constructor_sound (addsymbol s ofs) (Val.add (Genv.symbol_address ge s ofs)).
 Proof.
   red; unfold addsymbol; intros until x.
   case (addsymbol_match a); intros; InvEval; simpl; TrivialExists; simpl.
-  rewrite Genv.shift_symbol_address. auto. 
-  rewrite Genv.shift_symbol_address. subst x. rewrite Val.add_assoc. f_equal. f_equal. 
+  rewrite Genv.shift_symbol_address. auto.
+  rewrite Genv.shift_symbol_address. subst x. rewrite Val.add_assoc. f_equal. f_equal.
   apply Val.add_commut.
 Qed.
 
@@ -187,36 +187,36 @@ Proof.
 - apply eval_addimm; auto.
 - apply eval_addsymbol; auto.
 - rewrite Val.add_commut. apply eval_addsymbol; auto.
-- subst. 
+- subst.
   replace (Val.add (Val.add v1 (Vint n1)) (Val.add v0 (Vint n2)))
      with (Val.add (Val.add v1 v0) (Val.add (Vint n1) (Vint n2))).
   apply eval_addimm. EvalOp.
   repeat rewrite Val.add_assoc. decEq. apply Val.add_permut.
-- subst. 
+- subst.
   replace (Val.add (Val.add v1 (Vint n1)) y)
      with (Val.add (Val.add v1 y) (Vint n1)).
   apply eval_addimm. EvalOp.
   repeat rewrite Val.add_assoc. decEq. apply Val.add_commut.
-- subst. TrivialExists. 
+- subst. TrivialExists.
     econstructor. EvalOp. simpl. reflexivity. econstructor. eauto. constructor.
     simpl. repeat rewrite Val.add_assoc. decEq; decEq.
     rewrite Val.add_commut. rewrite Val.add_permut. auto.
 - replace (Val.add x y) with
     (Val.add (Genv.symbol_address ge s (Int.add ofs n)) (Val.add v1 v0)).
-  apply eval_addsymbol; auto. EvalOp. 
-  subst. rewrite Genv.shift_symbol_address. rewrite ! Val.add_assoc. f_equal. 
+  apply eval_addsymbol; auto. EvalOp.
+  subst. rewrite Genv.shift_symbol_address. rewrite ! Val.add_assoc. f_equal.
   rewrite Val.add_permut. f_equal. apply Val.add_commut.
-- subst. rewrite Val.add_assoc. apply eval_addsymbol. EvalOp. 
+- subst. rewrite Val.add_assoc. apply eval_addsymbol. EvalOp.
 - subst. rewrite <- Val.add_assoc. apply eval_addimm. EvalOp.
-- subst. rewrite Val.add_permut. apply eval_addsymbol. EvalOp. 
-- TrivialExists. 
+- subst. rewrite Val.add_permut. apply eval_addsymbol. EvalOp.
+- TrivialExists.
 Qed.
 
 Theorem eval_subimm:
   forall n, unary_constructor_sound (subimm n) (fun v => Val.sub (Vint n) v).
 Proof.
   intros; red; intros until x. unfold subimm. destruct (subimm_match a); intros.
-  InvEval. TrivialExists. 
+  InvEval. TrivialExists.
   InvEval. subst x. TrivialExists. unfold eval_operation. destruct v1; simpl; auto.
   rewrite ! Int.sub_add_opp. rewrite Int.add_assoc. f_equal. f_equal. f_equal.
   rewrite Int.neg_add_distr.  apply Int.add_commut.
@@ -229,7 +229,7 @@ Proof.
   unfold sub; case (sub_match a b); intros; InvEval.
   rewrite Val.sub_add_opp. apply eval_addimm; auto.
   apply eval_subimm; auto.
-  subst. rewrite Val.sub_add_l. rewrite Val.sub_add_r. 
+  subst. rewrite Val.sub_add_l. rewrite Val.sub_add_r.
     rewrite Val.add_assoc. simpl. rewrite Int.add_commut. rewrite <- Int.sub_add_opp.
     apply eval_addimm; EvalOp.
   subst. rewrite Val.sub_add_l. apply eval_addimm; EvalOp.
@@ -239,7 +239,7 @@ Qed.
 
 Theorem eval_negint: unary_constructor_sound negint (fun v => Val.sub Vzero v).
 Proof.
-  red; intros. unfold negint. apply eval_subimm; auto. 
+  red; intros. unfold negint. apply eval_subimm; auto.
 Qed.
 
 Lemma eval_rolm:
@@ -248,7 +248,7 @@ Lemma eval_rolm:
                           (fun x => Val.rolm x amount mask).
 Proof.
   red; intros until x. unfold rolm; case (rolm_match a); intros; InvEval.
-  TrivialExists. 
+  TrivialExists.
   subst. rewrite Val.rolm_rolm. TrivialExists.
   subst. rewrite <- Val.rolm_zero. rewrite Val.rolm_rolm.
   rewrite (Int.add_commut Int.zero). rewrite Int.add_zero. TrivialExists.
@@ -262,8 +262,8 @@ Proof.
   red; intros.  unfold shlimm.
   predSpec Int.eq Int.eq_spec n Int.zero.
   subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shl_zero; auto.
-  destruct (Int.ltu n Int.iwordsize) eqn:?. 
-  rewrite Val.shl_rolm; auto. apply eval_rolm; auto. 
+  destruct (Int.ltu n Int.iwordsize) eqn:?.
+  rewrite Val.shl_rolm; auto. apply eval_rolm; auto.
   TrivialExists. econstructor. eauto. econstructor. EvalOp. simpl; eauto. constructor. auto.
 Qed.
 
@@ -274,8 +274,8 @@ Proof.
   red; intros.  unfold shruimm.
   predSpec Int.eq Int.eq_spec n Int.zero.
   subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shru_zero; auto.
-  destruct (Int.ltu n Int.iwordsize) eqn:?. 
-  rewrite Val.shru_rolm; auto. apply eval_rolm; auto. 
+  destruct (Int.ltu n Int.iwordsize) eqn:?.
+  rewrite Val.shru_rolm; auto. apply eval_rolm; auto.
   TrivialExists. econstructor. eauto. econstructor. EvalOp. simpl; eauto. constructor. auto.
 Qed.
 
@@ -283,18 +283,18 @@ Theorem eval_shrimm:
   forall n, unary_constructor_sound (fun a => shrimm a n)
                                     (fun x => Val.shr x (Vint n)).
 Proof.
-  red; intros until x. unfold shrimm. 
+  red; intros until x. unfold shrimm.
   predSpec Int.eq Int.eq_spec n Int.zero.
   intros. subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shr_zero; auto.
   destruct (Int.ltu n Int.iwordsize) eqn:WS.
   case (shrimm_match a); intros.
   InvEval. exists (Vint (Int.shr n1 n)); split. EvalOp. simpl; rewrite WS; auto.
-  simpl; destruct (Int.lt mask1 Int.zero) eqn:?. 
+  simpl; destruct (Int.lt mask1 Int.zero) eqn:?.
   TrivialExists.
-  replace (Val.shr x (Vint n)) with (Val.shru x (Vint n)). 
+  replace (Val.shr x (Vint n)) with (Val.shru x (Vint n)).
   apply eval_shruimm; auto.
   destruct x; simpl; auto. rewrite WS.
-  decEq. symmetry. InvEval. destruct v1; simpl in H0; inv H0. 
+  decEq. symmetry. InvEval. destruct v1; simpl in H0; inv H0.
   apply Int.shr_and_is_shru_and; auto.
   simpl. TrivialExists.
   intros. simpl. TrivialExists.
@@ -304,13 +304,13 @@ Qed.
 Lemma eval_mulimm_base:
   forall n, unary_constructor_sound (mulimm_base n) (fun x => Val.mul x (Vint n)).
 Proof.
-  intros; red; intros; unfold mulimm_base. 
-  generalize (Int.one_bits_decomp n). 
+  intros; red; intros; unfold mulimm_base.
+  generalize (Int.one_bits_decomp n).
   generalize (Int.one_bits_range n).
   destruct (Int.one_bits n).
-  intros. TrivialExists. 
+  intros. TrivialExists.
   destruct l.
-  intros. rewrite H1. simpl. 
+  intros. rewrite H1. simpl.
   rewrite Int.add_zero.
   replace (Vint (Int.shl Int.one i)) with (Val.shl Vone (Vint i)). rewrite Val.shl_mul.
   apply eval_shlimm. auto. simpl. rewrite H0; auto with coqlib.
@@ -325,27 +325,27 @@ Proof.
   replace (Vint (Int.add (Int.shl Int.one i) (Int.shl Int.one i0)))
      with (Val.add (Val.shl Vone (Vint i)) (Val.shl Vone (Vint i0))).
   rewrite Val.mul_add_distr_r.
-  repeat rewrite Val.shl_mul. apply Val.add_lessdef; auto. 
-  simpl. repeat rewrite H0; auto with coqlib. 
-  intros. TrivialExists. 
+  repeat rewrite Val.shl_mul. apply Val.add_lessdef; auto.
+  simpl. repeat rewrite H0; auto with coqlib.
+  intros. TrivialExists.
 Qed.
 
 Theorem eval_mulimm:
   forall n, unary_constructor_sound (mulimm n) (fun x => Val.mul x (Vint n)).
 Proof.
   intros; red; intros until x; unfold mulimm.
-  predSpec Int.eq Int.eq_spec n Int.zero. 
-  intros. exists (Vint Int.zero); split. EvalOp. 
+  predSpec Int.eq Int.eq_spec n Int.zero.
+  intros. exists (Vint Int.zero); split. EvalOp.
   destruct x; simpl; auto. subst n. rewrite Int.mul_zero. auto.
   predSpec Int.eq Int.eq_spec n Int.one.
   intros. exists x; split; auto.
   destruct x; simpl; auto. subst n. rewrite Int.mul_one. auto.
   case (mulimm_match a); intros; InvEval.
   TrivialExists. simpl. rewrite Int.mul_commut; auto.
-  subst. rewrite Val.mul_add_distr_l. 
+  subst. rewrite Val.mul_add_distr_l.
   exploit eval_mulimm_base; eauto. instantiate (1 := n). intros [v' [A1 B1]].
   exploit (eval_addimm (Int.mul n n2) le (mulimm_base n t2) v'). auto. intros [v'' [A2 B2]].
-  exists v''; split; auto. eapply Val.lessdef_trans. eapply Val.add_lessdef; eauto. 
+  exists v''; split; auto. eapply Val.lessdef_trans. eapply Val.add_lessdef; eauto.
   rewrite Val.mul_commut; auto.
   apply eval_mulimm_base; auto.
 Qed.
@@ -354,7 +354,7 @@ Theorem eval_mul: binary_constructor_sound mul Val.mul.
 Proof.
   red; intros until y.
   unfold mul; case (mul_match a b); intros; InvEval.
-  rewrite Val.mul_commut. apply eval_mulimm. auto. 
+  rewrite Val.mul_commut. apply eval_mulimm. auto.
   apply eval_mulimm. auto.
   TrivialExists.
 Qed.
@@ -362,9 +362,9 @@ Qed.
 Theorem eval_andimm:
   forall n, unary_constructor_sound (andimm n) (fun x => Val.and x (Vint n)).
 Proof.
-  intros; red; intros until x. unfold andimm. 
+  intros; red; intros until x. unfold andimm.
   predSpec Int.eq Int.eq_spec n Int.zero.
-  intros. subst. exists (Vint Int.zero); split. EvalOp. 
+  intros. subst. exists (Vint Int.zero); split. EvalOp.
   destruct x; simpl; auto. rewrite Int.and_zero; auto.
   predSpec Int.eq Int.eq_spec n Int.mone.
   intros. subst. exists x; split. auto.
@@ -372,10 +372,10 @@ Proof.
   clear H H0.
   case (andimm_match a); intros.
   InvEval. TrivialExists. simpl. rewrite Int.and_commut; auto.
-  set (n' := Int.and n n2). 
+  set (n' := Int.and n n2).
   destruct (Int.eq (Int.shru (Int.shl n' amount) amount) n' &&
             Int.ltu amount Int.iwordsize) eqn:?.
-  InvEval. destruct (andb_prop _ _ Heqb). 
+  InvEval. destruct (andb_prop _ _ Heqb).
   generalize (Int.eq_spec (Int.shru (Int.shl n' amount) amount) n'). rewrite H1; intros.
   replace (Val.and x (Vint n))
      with (Val.rolm v0 (Int.sub Int.iwordsize amount) (Int.and (Int.shru Int.mone amount) n')).
@@ -383,26 +383,26 @@ Proof.
   subst. destruct v0; simpl; auto. rewrite H3. simpl. decEq. rewrite Int.and_assoc.
   rewrite (Int.and_commut n2 n).
   transitivity (Int.and (Int.shru i amount) (Int.and n n2)).
-  rewrite (Int.shru_rolm i); auto. unfold Int.rolm. rewrite Int.and_assoc; auto. 
+  rewrite (Int.shru_rolm i); auto. unfold Int.rolm. rewrite Int.and_assoc; auto.
   symmetry. apply Int.shr_and_shru_and. auto.
   set (e2 := Eop (Oshrimm amount) (t2 ::: Enil)) in *.
-  InvEval. subst. rewrite Val.and_assoc. simpl. rewrite Int.and_commut. TrivialExists.  
-  InvEval. subst. rewrite Val.and_assoc. simpl. rewrite Int.and_commut. TrivialExists. 
-  InvEval. subst. TrivialExists. simpl. 
-  destruct v1; auto. simpl. unfold Int.rolm. rewrite Int.and_assoc. 
+  InvEval. subst. rewrite Val.and_assoc. simpl. rewrite Int.and_commut. TrivialExists.
+  InvEval. subst. rewrite Val.and_assoc. simpl. rewrite Int.and_commut. TrivialExists.
+  InvEval. subst. TrivialExists. simpl.
+  destruct v1; auto. simpl. unfold Int.rolm. rewrite Int.and_assoc.
   decEq. decEq. decEq. apply Int.and_commut.
   destruct (Int.eq (Int.shru (Int.shl n amount) amount) n &&
             Int.ltu amount Int.iwordsize) eqn:?.
-  InvEval. destruct (andb_prop _ _ Heqb). 
+  InvEval. destruct (andb_prop _ _ Heqb).
   generalize (Int.eq_spec (Int.shru (Int.shl n amount) amount) n). rewrite H0; intros.
   replace (Val.and x (Vint n))
      with (Val.rolm v1 (Int.sub Int.iwordsize amount) (Int.and (Int.shru Int.mone amount) n)).
   apply eval_rolm; auto.
-  subst x. destruct v1; simpl; auto. rewrite H1; simpl. decEq. 
+  subst x. destruct v1; simpl; auto. rewrite H1; simpl. decEq.
   transitivity (Int.and (Int.shru i amount) n).
-  rewrite (Int.shru_rolm i); auto. unfold Int.rolm. rewrite Int.and_assoc; auto. 
+  rewrite (Int.shru_rolm i); auto. unfold Int.rolm. rewrite Int.and_assoc; auto.
   symmetry. apply Int.shr_and_shru_and. auto.
-  TrivialExists. 
+  TrivialExists.
   TrivialExists.
 Qed.
 
@@ -426,7 +426,7 @@ Proof.
   intros. subst. exists (Vint Int.mone); split. EvalOp. destruct x; simpl; auto. rewrite Int.or_mone; auto.
   clear H H0. destruct (orimm_match a); intros; InvEval.
   TrivialExists. simpl. rewrite Int.or_commut; auto.
-  subst. rewrite Val.or_assoc. simpl. rewrite Int.or_commut. TrivialExists. 
+  subst. rewrite Val.or_assoc. simpl. rewrite Int.or_commut. TrivialExists.
   TrivialExists.
 Qed.
 
@@ -438,10 +438,10 @@ Remark eval_same_expr:
   a1 = a2 /\ v1 = v2.
 Proof.
   intros until v2.
-  destruct a1; simpl; try (intros; discriminate). 
+  destruct a1; simpl; try (intros; discriminate).
   destruct a2; simpl; try (intros; discriminate).
   case (ident_eq i i0); intros.
-  subst i0. inversion H0. inversion H1. split. auto. congruence. 
+  subst i0. inversion H0. inversion H1. split. auto. congruence.
   discriminate.
 Qed.
 
@@ -452,29 +452,29 @@ Proof.
   destruct (Int.eq amount1 amount2 && same_expr_pure t1 t2) eqn:?.
   destruct (andb_prop _ _ Heqb0).
   generalize (Int.eq_spec amount1 amount2). rewrite H1. intro. subst amount2.
-  InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]. subst. 
+  InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]. subst.
   rewrite Val.or_rolm. TrivialExists.
   TrivialExists.
 (* andimm - rolm *)
   destruct (Int.eq mask1 (Int.not mask2) && is_rlw_mask mask2) eqn:?.
-  destruct (andb_prop _ _ Heqb0). 
+  destruct (andb_prop _ _ Heqb0).
   generalize (Int.eq_spec mask1 (Int.not mask2)); rewrite H1; intros.
-  InvEval. subst. TrivialExists. 
+  InvEval. subst. TrivialExists.
   TrivialExists.
 (* rolm - andimm *)
   destruct (Int.eq mask2 (Int.not mask1) && is_rlw_mask mask1) eqn:?.
-  destruct (andb_prop _ _ Heqb0). 
+  destruct (andb_prop _ _ Heqb0).
   generalize (Int.eq_spec mask2 (Int.not mask1)); rewrite H1; intros.
   InvEval. subst. rewrite Val.or_commut. TrivialExists.
   TrivialExists.
 (* intconst *)
-  InvEval. rewrite Val.or_commut. apply eval_orimm; auto. 
+  InvEval. rewrite Val.or_commut. apply eval_orimm; auto.
   InvEval. apply eval_orimm; auto.
 (* orc *)
   InvEval. subst. rewrite Val.or_commut. TrivialExists.
   InvEval. subst. TrivialExists.
 (* default *)
-  TrivialExists. 
+  TrivialExists.
 Qed.
 
 Theorem eval_xorimm:
@@ -484,11 +484,11 @@ Proof.
   predSpec Int.eq Int.eq_spec n Int.zero.
   intros. subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.xor_zero; auto.
   predSpec Int.eq Int.eq_spec n Int.mone.
-  intros. subst. rewrite <- Val.not_xor. apply eval_notint; auto. 
+  intros. subst. rewrite <- Val.not_xor. apply eval_notint; auto.
   clear H H0. destruct (xorimm_match a); intros; InvEval.
   TrivialExists. simpl. rewrite Int.xor_commut; auto.
   subst. rewrite Val.xor_assoc. simpl. rewrite Int.xor_commut. TrivialExists.
-  subst x. TrivialExists. simpl. rewrite Val.not_xor. rewrite Val.xor_assoc. 
+  subst x. TrivialExists. simpl. rewrite Val.not_xor. rewrite Val.xor_assoc.
   simpl. rewrite Int.xor_commut; auto.
   TrivialExists.
 Qed.
@@ -498,7 +498,7 @@ Proof.
   red; intros until y; unfold xor; case (xor_match a b); intros; InvEval.
   rewrite Val.xor_commut. apply eval_xorimm; auto.
   apply eval_xorimm; auto.
-  subst. rewrite Val.xor_commut. rewrite Val.not_xor. rewrite <- Val.xor_assoc. 
+  subst. rewrite Val.xor_commut. rewrite Val.not_xor. rewrite <- Val.xor_assoc.
   rewrite <- Val.not_xor. rewrite Val.xor_commut. TrivialExists.
   subst. rewrite Val.not_xor. rewrite <- Val.xor_assoc. rewrite <- Val.not_xor. TrivialExists.
   TrivialExists.
@@ -524,19 +524,19 @@ Lemma eval_mod_aux:
   eval_expr ge sp e m le (mod_aux divop a b) (Val.sub x (Val.mul z y)).
 Proof.
   intros; unfold mod_aux.
-  eapply eval_Elet. eexact H0. eapply eval_Elet. 
+  eapply eval_Elet. eexact H0. eapply eval_Elet.
   apply eval_lift. eexact H1.
-  eapply eval_Eop. eapply eval_Econs. 
+  eapply eval_Eop. eapply eval_Econs.
   eapply eval_Eletvar. simpl; reflexivity.
-  eapply eval_Econs. eapply eval_Eop. 
+  eapply eval_Econs. eapply eval_Eop.
   eapply eval_Econs. eapply eval_Eop.
   eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity.
   eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity.
-  apply eval_Enil.  
+  apply eval_Enil.
   rewrite H. eauto.
   eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity.
-  apply eval_Enil.  
-  simpl; reflexivity. apply eval_Enil. 
+  apply eval_Enil.
+  simpl; reflexivity. apply eval_Enil.
   reflexivity.
 Qed.
 
@@ -547,7 +547,7 @@ Theorem eval_mods_base:
   Val.mods x y = Some z ->
   exists v, eval_expr ge sp e m le (mods_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros; unfold mods_base. 
+  intros; unfold mods_base.
   exploit Val.mods_divs; eauto. intros [v [A B]].
   subst. econstructor; split; eauto.
   apply eval_mod_aux with (semdivop := Val.divs); auto.
@@ -570,7 +570,7 @@ Theorem eval_modu_base:
   Val.modu x y = Some z ->
   exists v, eval_expr ge sp e m le (modu_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros; unfold modu_base. 
+  intros; unfold modu_base.
   exploit Val.modu_divu; eauto. intros [v [A B]].
   subst. econstructor; split; eauto.
   apply eval_mod_aux with (semdivop := Val.divu); auto.
@@ -582,13 +582,13 @@ Theorem eval_shrximm:
   Val.shrx x (Vint n) = Some z ->
   exists v, eval_expr ge sp e m le (shrximm a n) v /\ Val.lessdef z v.
 Proof.
-  intros. unfold shrximm. 
+  intros. unfold shrximm.
   predSpec Int.eq Int.eq_spec n Int.zero.
-  subst n. exists x; split; auto. 
+  subst n. exists x; split; auto.
   destruct x; simpl in H0; try discriminate.
   destruct (Int.ltu Int.zero (Int.repr 31)); inv H0.
-  replace (Int.shrx i Int.zero) with i. auto. 
-  unfold Int.shrx, Int.divs. rewrite Int.shl_zero. 
+  replace (Int.shrx i Int.zero) with i. auto.
+  unfold Int.shrx, Int.divs. rewrite Int.shl_zero.
   change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed; auto.
   econstructor; split. EvalOp. auto.
 Qed.
@@ -597,38 +597,38 @@ Theorem eval_shl: binary_constructor_sound shl Val.shl.
 Proof.
   red; intros until y; unfold shl; case (shl_match b); intros.
   InvEval. apply eval_shlimm; auto.
-  TrivialExists. 
+  TrivialExists.
 Qed.
 
 Theorem eval_shr: binary_constructor_sound shr Val.shr.
 Proof.
   red; intros until y; unfold shr; case (shr_match b); intros.
   InvEval. apply eval_shrimm; auto.
-  TrivialExists. 
+  TrivialExists.
 Qed.
 
 Theorem eval_shru: binary_constructor_sound shru Val.shru.
 Proof.
   red; intros until y; unfold shru; case (shru_match b); intros.
   InvEval. apply eval_shruimm; auto.
-  TrivialExists. 
+  TrivialExists.
 Qed.
 
 Theorem eval_negf: unary_constructor_sound negf Val.negf.
 Proof.
-  red; intros. TrivialExists. 
+  red; intros. TrivialExists.
 Qed.
 
 Theorem eval_absf: unary_constructor_sound absf Val.absf.
 Proof.
-  red; intros. TrivialExists. 
+  red; intros. TrivialExists.
 Qed.
 
 Theorem eval_addf: binary_constructor_sound addf Val.addf.
 Proof.
   red; intros; TrivialExists.
 Qed.
- 
+
 Theorem eval_subf: binary_constructor_sound subf Val.subf.
 Proof.
   red; intros; TrivialExists.
@@ -641,19 +641,19 @@ Qed.
 
 Theorem eval_negfs: unary_constructor_sound negfs Val.negfs.
 Proof.
-  red; intros. TrivialExists. 
+  red; intros. TrivialExists.
 Qed.
 
 Theorem eval_absfs: unary_constructor_sound absfs Val.absfs.
 Proof.
-  red; intros. TrivialExists. 
+  red; intros. TrivialExists.
 Qed.
 
 Theorem eval_addfs: binary_constructor_sound addfs Val.addfs.
 Proof.
   red; intros; TrivialExists.
 Qed.
- 
+
 Theorem eval_subfs: binary_constructor_sound subfs Val.subfs.
 Proof.
   red; intros; TrivialExists.
@@ -687,8 +687,8 @@ Proof.
 (* constant *)
   InvEval. rewrite sem_int. TrivialExists. simpl. destruct (intsem c0 n1 n2); auto.
 (* eq cmp *)
-  InvEval. inv H. simpl in H5. inv H5. 
-  destruct (Int.eq_dec n2 Int.zero). subst n2. TrivialExists. 
+  InvEval. inv H. simpl in H5. inv H5.
+  destruct (Int.eq_dec n2 Int.zero). subst n2. TrivialExists.
   simpl. rewrite eval_negate_condition.
   destruct (eval_condition c0 vl m); simpl.
   unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_eq; auto.
@@ -697,13 +697,13 @@ Proof.
   simpl. destruct (eval_condition c0 vl m); simpl.
   unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_eq; auto.
   rewrite sem_undef; auto.
-  exists (Vint Int.zero); split. EvalOp. 
+  exists (Vint Int.zero); split. EvalOp.
   destruct (eval_condition c0 vl m); simpl.
   unfold Vtrue, Vfalse. destruct b; rewrite sem_eq; rewrite Int.eq_false; auto.
   rewrite sem_undef; auto.
 (* ne cmp *)
-  InvEval. inv H. simpl in H5. inv H5. 
-  destruct (Int.eq_dec n2 Int.zero). subst n2. TrivialExists. 
+  InvEval. inv H. simpl in H5. inv H5.
+  destruct (Int.eq_dec n2 Int.zero). subst n2. TrivialExists.
   simpl. destruct (eval_condition c0 vl m); simpl.
   unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_ne; auto.
   rewrite sem_undef; auto.
@@ -711,21 +711,21 @@ Proof.
   simpl. rewrite eval_negate_condition. destruct (eval_condition c0 vl m); simpl.
   unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_ne; auto.
   rewrite sem_undef; auto.
-  exists (Vint Int.one); split. EvalOp. 
+  exists (Vint Int.one); split. EvalOp.
   destruct (eval_condition c0 vl m); simpl.
   unfold Vtrue, Vfalse. destruct b; rewrite sem_ne; rewrite Int.eq_false; auto.
   rewrite sem_undef; auto.
 (* eq andimm *)
   destruct (Int.eq_dec n2 Int.zero). InvEval; subst.
-  econstructor; split. EvalOp. simpl; eauto. 
-  destruct v1; simpl; try (rewrite sem_undef; auto). rewrite sem_eq. 
-  destruct (Int.eq (Int.and i n1) Int.zero); auto. 
+  econstructor; split. EvalOp. simpl; eauto.
+  destruct v1; simpl; try (rewrite sem_undef; auto). rewrite sem_eq.
+  destruct (Int.eq (Int.and i n1) Int.zero); auto.
   TrivialExists. simpl. rewrite sem_default. auto.
 (* ne andimm *)
   destruct (Int.eq_dec n2 Int.zero). InvEval; subst.
-  econstructor; split. EvalOp. simpl; eauto. 
-  destruct v1; simpl; try (rewrite sem_undef; auto). rewrite sem_ne. 
-  destruct (Int.eq (Int.and i n1) Int.zero); auto. 
+  econstructor; split. EvalOp. simpl; eauto.
+  destruct v1; simpl; try (rewrite sem_undef; auto). rewrite sem_ne.
+  destruct (Int.eq (Int.and i n1) Int.zero); auto.
   TrivialExists. simpl. rewrite sem_default. auto.
 (* default *)
   TrivialExists. simpl. rewrite sem_default. auto.
@@ -740,7 +740,7 @@ Lemma eval_compimm_swap:
   exists v, eval_expr ge sp e m le (compimm default intsem (swap_comparison c) a n2) v
          /\ Val.lessdef (sem c (Vint n2) x) v.
 Proof.
-  intros. rewrite <- sem_swap. eapply eval_compimm; eauto. 
+  intros. rewrite <- sem_swap. eapply eval_compimm; eauto.
 Qed.
 
 End COMP_IMM.
@@ -749,9 +749,9 @@ Theorem eval_comp:
   forall c, binary_constructor_sound (comp c) (Val.cmp c).
 Proof.
   intros; red; intros until y. unfold comp; case (comp_match a b); intros; InvEval.
-  eapply eval_compimm_swap; eauto. 
+  eapply eval_compimm_swap; eauto.
   intros. unfold Val.cmp. rewrite Val.swap_cmp_bool; auto.
-  eapply eval_compimm; eauto. 
+  eapply eval_compimm; eauto.
   TrivialExists.
 Qed.
 
@@ -759,9 +759,9 @@ Theorem eval_compu:
   forall c, binary_constructor_sound (compu c) (Val.cmpu (Mem.valid_pointer m) c).
 Proof.
   intros; red; intros until y. unfold compu; case (compu_match a b); intros; InvEval.
-  eapply eval_compimm_swap; eauto. 
+  eapply eval_compimm_swap; eauto.
   intros. unfold Val.cmpu. rewrite Val.swap_cmpu_bool; auto.
-  eapply eval_compimm; eauto. 
+  eapply eval_compimm; eauto.
   TrivialExists.
 Qed.
 
@@ -777,11 +777,11 @@ Proof.
   intros; red; intros. unfold compfs.
   replace (Val.cmpfs c x y) with
           (Val.cmpf c (Val.floatofsingle x) (Val.floatofsingle y)).
-  TrivialExists. constructor. EvalOp. simpl; reflexivity. 
+  TrivialExists. constructor. EvalOp. simpl; reflexivity.
   constructor. EvalOp. simpl; reflexivity. constructor.
-  auto. 
-  destruct x; auto. destruct y; auto. unfold Val.cmpf, Val.cmpfs; simpl. 
-  rewrite Float32.cmp_double. auto. 
+  auto.
+  destruct x; auto. destruct y; auto. unfold Val.cmpf, Val.cmpfs; simpl.
+  rewrite Float32.cmp_double. auto.
 Qed.
 
 Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8).
@@ -826,7 +826,7 @@ Theorem eval_intoffloat:
   Val.intoffloat x = Some y ->
   exists v, eval_expr ge sp e m le (intoffloat a) v /\ Val.lessdef y v.
 Proof.
-  intros; unfold intoffloat. TrivialExists. 
+  intros; unfold intoffloat. TrivialExists.
 Qed.
 
 Theorem eval_intuoffloat:
@@ -845,24 +845,24 @@ Proof.
   assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar O) (Vfloat fm)).
     constructor. auto.
   econstructor. eauto.
-  econstructor. instantiate (1 := Vfloat fm). EvalOp. 
+  econstructor. instantiate (1 := Vfloat fm). EvalOp.
   eapply eval_Econdition with (va := Float.cmp Clt f fm).
   eauto with evalexpr.
   destruct (Float.cmp Clt f fm) eqn:?.
   exploit Float.to_intu_to_int_1; eauto. intro EQ.
   EvalOp. simpl. rewrite EQ; auto.
-  exploit Float.to_intu_to_int_2; eauto. 
+  exploit Float.to_intu_to_int_2; eauto.
   change Float.ox8000_0000 with im. fold fm. intro EQ.
   set (t2 := subf (Eletvar (S O)) (Eletvar O)).
   set (t3 := intoffloat t2).
   exploit (eval_subf (Vfloat fm :: Vfloat f :: le) (Eletvar (S O)) (Vfloat f) (Eletvar O)); eauto.
-  fold t2. intros [v2 [A2 B2]]. simpl in B2. inv B2. 
+  fold t2. intros [v2 [A2 B2]]. simpl in B2. inv B2.
   exploit (eval_addimm Float.ox8000_0000 (Vfloat fm :: Vfloat f :: le) t3).
-    unfold t3. unfold intoffloat. EvalOp. simpl. rewrite EQ. simpl. eauto. 
-  intros [v4 [A4 B4]]. simpl in B4. inv B4. 
-  rewrite Int.sub_add_opp in A4. rewrite Int.add_assoc in A4. 
-  rewrite (Int.add_commut (Int.neg im)) in A4. 
-  rewrite Int.add_neg_zero in A4. 
+    unfold t3. unfold intoffloat. EvalOp. simpl. rewrite EQ. simpl. eauto.
+  intros [v4 [A4 B4]]. simpl in B4. inv B4.
+  rewrite Int.sub_add_opp in A4. rewrite Int.add_assoc in A4.
+  rewrite (Int.add_commut (Int.neg im)) in A4.
+  rewrite Int.add_neg_zero in A4.
   rewrite Int.add_zero in A4.
   auto.
 Qed.
@@ -874,18 +874,18 @@ Theorem eval_floatofint:
   exists v, eval_expr ge sp e m le (floatofint a) v /\ Val.lessdef y v.
 Proof.
   intros until y. unfold floatofint. destruct (floatofint_match a); intros.
-  InvEval. TrivialExists. 
+  InvEval. TrivialExists.
   rename e0 into a. destruct x; simpl in H0; inv H0.
   exists (Vfloat (Float.of_int i)); split; auto.
   set (t1 := addimm Float.ox8000_0000 a).
   set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: t1 ::: Enil)).
   set (t3 := Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil).
-  exploit (eval_addimm Float.ox8000_0000 le a). eauto. fold t1. 
+  exploit (eval_addimm Float.ox8000_0000 le a). eauto. fold t1.
   intros [v1 [A1 B1]]. simpl in B1. inv B1.
-  exploit (eval_subf le t2). 
-  unfold t2. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. 
-  unfold eval_operation. eauto. 
-  instantiate (2 := t3). unfold t3. EvalOp. simpl; eauto.  
+  exploit (eval_subf le t2).
+  unfold t2. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor.
+  unfold eval_operation. eauto.
+  instantiate (2 := t3). unfold t3. EvalOp. simpl; eauto.
   intros [v2 [A2 B2]]. simpl in B2. inv B2. rewrite Float.of_int_from_words. auto.
 Qed.
 
@@ -902,9 +902,9 @@ Proof.
   unfold floatofintu.
   set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: a ::: Enil)).
   set (t3 := Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil).
-  exploit (eval_subf le t2). 
-  unfold t2. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. 
-  unfold eval_operation. eauto. 
+  exploit (eval_subf le t2).
+  unfold t2. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor.
+  unfold eval_operation. eauto.
   instantiate (2 := t3). unfold t3. EvalOp. simpl; eauto.
   intros [v2 [A2 B2]]. simpl in B2. inv B2. rewrite Float.of_intu_from_words. auto.
 Qed.
@@ -915,14 +915,14 @@ Theorem eval_intofsingle:
   Val.intofsingle x = Some y ->
   exists v, eval_expr ge sp e m le (intofsingle a) v /\ Val.lessdef y v.
 Proof.
-  intros; unfold intofsingle. 
+  intros; unfold intofsingle.
   assert (Val.intoffloat (Val.floatofsingle x) = Some y).
   { destruct x; simpl in H0; try discriminate.
-    destruct (Float32.to_int f) eqn:F; inv H0. 
-    apply Float32.to_int_double in F. 
-    simpl. unfold Float32.to_double in F; rewrite F; auto.  
+    destruct (Float32.to_int f) eqn:F; inv H0.
+    apply Float32.to_int_double in F.
+    simpl. unfold Float32.to_double in F; rewrite F; auto.
   }
-  apply eval_intoffloat with (Val.floatofsingle x); auto. EvalOp. 
+  apply eval_intoffloat with (Val.floatofsingle x); auto. EvalOp.
 Qed.
 
 Theorem eval_singleofint:
@@ -935,11 +935,11 @@ Proof.
   assert (exists z, Val.floatofint x = Some z /\ y = Val.singleoffloat z).
   {
     destruct x; inv H0. simpl. exists (Vfloat (Float.of_int i)); simpl; split; auto.
-    f_equal. apply Float32.of_int_double. 
+    f_equal. apply Float32.of_int_double.
   }
-  destruct H1 as (z & A & B). subst y. 
-  exploit eval_floatofint; eauto. intros (v & C & D). 
-  exists (Val.singleoffloat v); split. EvalOp. inv D; auto. 
+  destruct H1 as (z & A & B). subst y.
+  exploit eval_floatofint; eauto. intros (v & C & D).
+  exists (Val.singleoffloat v); split. EvalOp. inv D; auto.
 Qed.
 
 Theorem eval_intuofsingle:
@@ -948,14 +948,14 @@ Theorem eval_intuofsingle:
   Val.intuofsingle x = Some y ->
   exists v, eval_expr ge sp e m le (intuofsingle a) v /\ Val.lessdef y v.
 Proof.
-  intros; unfold intuofsingle. 
+  intros; unfold intuofsingle.
   assert (Val.intuoffloat (Val.floatofsingle x) = Some y).
   { destruct x; simpl in H0; try discriminate.
-    destruct (Float32.to_intu f) eqn:F; inv H0. 
-    apply Float32.to_intu_double in F. 
-    simpl. unfold Float32.to_double in F; rewrite F; auto.  
+    destruct (Float32.to_intu f) eqn:F; inv H0.
+    apply Float32.to_intu_double in F.
+    simpl. unfold Float32.to_double in F; rewrite F; auto.
   }
-  apply eval_intuoffloat with (Val.floatofsingle x); auto. EvalOp. 
+  apply eval_intuoffloat with (Val.floatofsingle x); auto. EvalOp.
 Qed.
 
 Theorem eval_singleofintu:
@@ -968,11 +968,11 @@ Proof.
   assert (exists z, Val.floatofintu x = Some z /\ y = Val.singleoffloat z).
   {
     destruct x; inv H0. simpl. exists (Vfloat (Float.of_intu i)); simpl; split; auto.
-    f_equal. apply Float32.of_intu_double. 
+    f_equal. apply Float32.of_intu_double.
   }
-  destruct H1 as (z & A & B). subst y. 
-  exploit eval_floatofintu; eauto. intros (v & C & D). 
-  exists (Val.singleoffloat v); split. EvalOp. inv D; auto. 
+  destruct H1 as (z & A & B). subst y.
+  exploit eval_floatofintu; eauto. intros (v & C & D).
+  exists (Val.singleoffloat v); split. EvalOp. inv D; auto.
 Qed.
 
 Theorem eval_addressing:
@@ -981,7 +981,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.
@@ -990,12 +990,12 @@ Proof.
   exists (@nil val). split. eauto with evalexpr. simpl. auto.
   exists (v1 :: nil). split. eauto with evalexpr. simpl. congruence.
   exists (v1 :: nil). split. eauto with evalexpr. simpl. congruence.
-  destruct (can_use_Aindexed2 chunk). 
+  destruct (can_use_Aindexed2 chunk).
   exists (v1 :: v0 :: nil). split. eauto with evalexpr. simpl. congruence.
   exists (Vptr b ofs :: nil). split.
-  constructor. EvalOp. simpl; congruence. constructor. 
+  constructor. EvalOp. simpl; congruence. constructor.
   simpl. rewrite Int.add_zero. auto.
-  exists (v :: nil). split. eauto with evalexpr. subst v. simpl. 
+  exists (v :: nil). split. eauto with evalexpr. subst v. simpl.
   rewrite Int.add_zero. auto.
 Qed.
 
@@ -1007,7 +1007,7 @@ Proof.
   intros until v. unfold builtin_arg; case (builtin_arg_match a); intros; InvEval.
 - constructor.
 - constructor.
-- constructor. 
+- constructor.
 - simpl in H5. inv H5. constructor.
 - subst v. constructor; auto.
 - inv H. InvEval. simpl in H6; inv H6. constructor; auto.