Updated PR by removing whitespaces. Bug 17450.

1 files changed, 207 insertions, 207 deletions

diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v
index 4d7547f0..7c1b60a9 100644
--- a/backend/Unusedglobproof.v
+++ b/backend/Unusedglobproof.v
@@ -37,7 +37,7 @@ Module ISP := FSetProperties.Properties(IS).
 
 (** Monotonic evolution of the workset. *)
 
-Inductive workset_incl (w1 w2: workset) : Prop := 
+Inductive workset_incl (w1 w2: workset) : Prop :=
   workset_incl_intro:
     forall (SEEN: IS.Subset w1.(w_seen) w2.(w_seen))
            (TODO: List.incl w1.(w_todo) w2.(w_todo))
@@ -53,7 +53,7 @@ Qed.
 
 Lemma workset_incl_refl: forall w, workset_incl w w.
 Proof.
-  intros; split. red; auto. red; auto. auto. 
+  intros; split. red; auto. red; auto. auto.
 Qed.
 
 Lemma workset_incl_trans:
@@ -62,7 +62,7 @@ Proof.
   intros. destruct H, H0; split.
   red; eauto.
   red; eauto.
-  intros. edestruct TRACK0; eauto. edestruct TRACK; eauto. 
+  intros. edestruct TRACK0; eauto. edestruct TRACK; eauto.
 Qed.
 
 Lemma add_workset_incl:
@@ -73,13 +73,13 @@ Proof.
 - split; simpl.
   + red; intros. apply IS.add_2; auto.
   + red; simpl; auto.
-  + intros. destruct (ident_eq id id0); auto. apply IS.add_3 in H; auto. 
+  + intros. destruct (ident_eq id id0); auto. apply IS.add_3 in H; auto.
 Qed.
 
 Lemma addlist_workset_incl:
   forall l w, workset_incl w (addlist_workset l w).
 Proof.
-  induction l; simpl; intros. 
+  induction l; simpl; intros.
   apply workset_incl_refl.
   eapply workset_incl_trans. apply add_workset_incl. eauto.
 Qed.
@@ -90,14 +90,14 @@ Proof.
   unfold add_ref_function; intros. apply PTree_Properties.fold_rec.
 - auto.
 - apply workset_incl_refl.
-- intros. apply workset_incl_trans with a; auto. 
+- intros. apply workset_incl_trans with a; auto.
   unfold add_ref_instruction. apply addlist_workset_incl.
 Qed.
 
 Lemma add_ref_globvar_incl:
   forall gv w, workset_incl w (add_ref_globvar gv w).
 Proof.
-  unfold add_ref_globvar; intros. 
+  unfold add_ref_globvar; intros.
   revert w. induction (gvar_init gv); simpl; intros.
   apply workset_incl_refl.
   eapply workset_incl_trans; [ | eauto ].
@@ -108,7 +108,7 @@ Qed.
 Lemma add_ref_definition_incl:
   forall pm id w, workset_incl w (add_ref_definition pm id w).
 Proof.
-  unfold add_ref_definition; intros. 
+  unfold add_ref_definition; intros.
   destruct (pm!id) as [[[] | ? ] | ].
   apply add_ref_function_incl.
   apply workset_incl_refl.
@@ -120,10 +120,10 @@ Lemma initial_workset_incl:
   forall p, workset_incl {| w_seen := IS.empty; w_todo := nil |} (initial_workset p).
 Proof.
   unfold initial_workset; intros.
-  eapply workset_incl_trans. 2: apply add_workset_incl. 
+  eapply workset_incl_trans. 2: apply add_workset_incl.
   generalize {| w_seen := IS.empty; w_todo := nil |}. induction (prog_public p); simpl; intros.
   apply workset_incl_refl.
-  eapply workset_incl_trans. eapply add_workset_incl. eapply IHl. 
+  eapply workset_incl_trans. eapply add_workset_incl. eapply IHl.
 Qed.
 
 (** Soundness properties for functions that add identifiers to the workset *)
@@ -141,7 +141,7 @@ Lemma seen_addlist_workset:
   forall id l (w: workset),
   In id l -> IS.In id (addlist_workset l w).
 Proof.
-  induction l; simpl; intros. 
+  induction l; simpl; intros.
   tauto.
   destruct H. subst a.
   eapply seen_workset_incl. apply addlist_workset_incl. apply seen_add_workset.
@@ -159,9 +159,9 @@ Proof.
 - destruct H1 as (pc & i & A & B). apply H0; auto. exists pc, i; split; auto. rewrite H; auto.
 - destruct H as (pc & i & A & B). rewrite PTree.gempty in A; discriminate.
 - destruct H2 as (pc & i & A & B). rewrite PTree.gsspec in A. destruct (peq pc k).
-  + inv A. unfold add_ref_instruction. apply seen_addlist_workset; auto. 
-  + unfold add_ref_instruction. eapply seen_workset_incl. apply addlist_workset_incl. 
-    apply H1. exists pc, i; auto. 
+  + inv A. unfold add_ref_instruction. apply seen_addlist_workset; auto.
+  + unfold add_ref_instruction. eapply seen_workset_incl. apply addlist_workset_incl.
+    apply H1. exists pc, i; auto.
 Qed.
 
 Definition ref_fundef (fd: fundef) (id: ident) : Prop :=
@@ -186,35 +186,35 @@ Proof.
           IS.In id' w \/ In (Init_addrof id' ofs) l ->
           IS.In id' (fold_left add_ref_init_data l w)).
   {
-    induction l; simpl; intros. 
+    induction l; simpl; intros.
     tauto.
     apply IHl. intuition auto.
-    left. destruct a; simpl; auto. eapply seen_workset_incl. apply add_workset_incl. auto. 
+    left. destruct a; simpl; auto. eapply seen_workset_incl. apply add_workset_incl. auto.
     subst; left; simpl. apply seen_add_workset.
   }
-  apply H0; auto. 
+  apply H0; auto.
 Qed.
 
 Lemma seen_main_initial_workset:
   forall p, IS.In p.(prog_main) (initial_workset p).
 Proof.
-  unfold initial_workset; intros. apply seen_add_workset. 
+  unfold initial_workset; intros. apply seen_add_workset.
 Qed.
 
 Lemma seen_public_initial_workset:
   forall p id, In id p.(prog_public) -> IS.In id (initial_workset p).
 Proof.
-  intros. unfold initial_workset. eapply seen_workset_incl. apply add_workset_incl. 
+  intros. unfold initial_workset. eapply seen_workset_incl. apply add_workset_incl.
   assert (forall l (w: workset),
           IS.In id w \/ In id l -> IS.In id (fold_left (fun w id => add_workset id w) l w)).
   {
     induction l; simpl; intros.
     tauto.
     apply IHl. intuition auto; left.
-    eapply seen_workset_incl. apply add_workset_incl. auto. 
-    subst a. apply seen_add_workset. 
+    eapply seen_workset_incl. apply add_workset_incl. auto.
+    subst a. apply seen_add_workset.
   }
-  apply H0. auto. 
+  apply H0. auto.
 Qed.
 
 (** * Semantic preservation *)
@@ -248,16 +248,16 @@ Lemma iter_step_invariant:
   | inr w' => workset_invariant w'
   end.
 Proof.
-  unfold iter_step, workset_invariant, used_set_closed; intros. 
+  unfold iter_step, workset_invariant, used_set_closed; intros.
   destruct (w_todo w) as [ | id rem ]; intros.
 - eapply H; eauto.
 - set (w' := {| w_seen := w.(w_seen); w_todo := rem |}) in *.
   destruct (add_ref_definition_incl pm id w').
   destruct (ident_eq id id0).
-  + subst id0. eapply seen_add_ref_definition; eauto. 
+  + subst id0. eapply seen_add_ref_definition; eauto.
   + exploit TRACK; eauto. intros [A|A].
-    * apply SEEN. eapply H; eauto. simpl. 
-      assert (~ In id0 rem). 
+    * apply SEEN. eapply H; eauto. simpl.
+      assert (~ In id0 rem).
       { change rem with (w_todo w'). red; intros. elim H1; auto. }
       tauto.
     * contradiction.
@@ -267,10 +267,10 @@ Theorem used_globals_sound:
   forall u, used_globals p = Some u -> used_set_closed u.
 Proof.
   unfold used_globals; intros. eapply PrimIter.iterate_prop with (P := workset_invariant); eauto.
-- intros. apply iter_step_invariant; auto. 
-- destruct (initial_workset_incl p). 
-  red; intros. edestruct TRACK; eauto. 
-  simpl in H4. eelim IS.empty_1; eauto. 
+- intros. apply iter_step_invariant; auto.
+- destruct (initial_workset_incl p).
+  red; intros. edestruct TRACK; eauto.
+  simpl in H4. eelim IS.empty_1; eauto.
   contradiction.
 Qed.
 
@@ -286,7 +286,7 @@ Proof.
 - red; auto.
 Qed.
 
-Definition used: IS.t := 
+Definition used: IS.t :=
   match used_globals p with Some u => u | None => IS.empty end.
 
 Remark USED_GLOBALS: used_globals p = Some used.
@@ -322,7 +322,7 @@ Remark filter_globdefs_accu:
 Proof.
   induction defs; simpl; intros.
   auto.
-  destruct a as [id gd]. destruct (IS.mem id u); auto. 
+  destruct a as [id gd]. destruct (IS.mem id u); auto.
   rewrite <- IHdefs. auto.
 Qed.
 
@@ -330,28 +330,28 @@ Remark filter_globdefs_nil:
   forall u accu defs,
   filter_globdefs u accu defs = filter_globdefs u nil defs ++ accu.
 Proof.
-  intros. rewrite <- filter_globdefs_accu. auto. 
+  intros. rewrite <- filter_globdefs_accu. auto.
 Qed.
 
 Theorem transform_program_charact:
   forall id, (program_map tp)!id = if IS.mem id used then pm!id else None.
 Proof.
-  intros. 
+  intros.
   assert (X: forall l u m1 m2,
              IS.In id u ->
              m1!id = m2!id ->
              (fold_left add_def_prog_map (filter_globdefs u nil l) m1)!id =
              (fold_left add_def_prog_map (List.rev l) m2)!id).
   {
-    induction l; simpl; intros. 
+    induction l; simpl; intros.
     auto.
-    destruct a as [id1 gd1]. rewrite fold_left_app. simpl. 
+    destruct a as [id1 gd1]. rewrite fold_left_app. simpl.
     destruct (IS.mem id1 u) eqn:MEM.
-    rewrite filter_globdefs_nil. rewrite fold_left_app. simpl. 
-    unfold add_def_prog_map at 1 3. simpl. 
+    rewrite filter_globdefs_nil. rewrite fold_left_app. simpl.
+    unfold add_def_prog_map at 1 3. simpl.
     rewrite ! PTree.gsspec. destruct (peq id id1). auto.
-    apply IHl; auto. apply IS.remove_2; auto. 
-    unfold add_def_prog_map at 2. simpl. rewrite PTree.gso. apply IHl; auto. 
+    apply IHl; auto. apply IS.remove_2; auto.
+    unfold add_def_prog_map at 2. simpl. rewrite PTree.gso. apply IHl; auto.
     red; intros; subst id1.
     assert (IS.mem id u = true) by (apply IS.mem_1; auto). congruence.
   }
@@ -364,9 +364,9 @@ Proof.
     auto.
     destruct a as [id1 gd1].
     destruct (IS.mem id1 u) eqn:MEM.
-    rewrite filter_globdefs_nil. rewrite fold_left_app. simpl. 
+    rewrite filter_globdefs_nil. rewrite fold_left_app. simpl.
     unfold add_def_prog_map at 1. simpl. rewrite PTree.gso by congruence. eapply IHl; eauto.
-    rewrite ISF.remove_b. rewrite H; auto. 
+    rewrite ISF.remove_b. rewrite H; auto.
     eapply IHl; eauto.
   }
   unfold pm, program_map.
@@ -393,8 +393,8 @@ Definition genv_progmap_match (ge: genv) (pm: prog_map) : Prop :=
 Lemma genv_program_map:
   forall p, genv_progmap_match (Genv.globalenv p) (program_map p).
 Proof.
-  intros. unfold Genv.globalenv, program_map. 
-  assert (REC: forall defs g m, 
+  intros. unfold Genv.globalenv, program_map.
+  assert (REC: forall defs g m,
                genv_progmap_match g m ->
                genv_progmap_match (Genv.add_globals g defs) (fold_left add_def_prog_map defs m)).
   {
@@ -407,12 +407,12 @@ Proof.
   - rewrite PTree.gsspec. destruct (peq id id1); subst.
     + rewrite ! PTree.gss. auto.
     + destruct (Genv.genv_symb g)!id as [b|] eqn:S; rewrite PTree.gso by auto.
-      * rewrite PTree.gso. auto. apply Plt_ne. eapply Genv.genv_symb_range; eauto. 
+      * rewrite PTree.gso. auto. apply Plt_ne. eapply Genv.genv_symb_range; eauto.
       * auto.
   - rewrite PTree.gsspec. destruct (peq id id1); subst.
     + rewrite ! PTree.gss. auto.
     + destruct (Genv.genv_symb g)!id as [b|] eqn:S; rewrite PTree.gso by auto.
-      * rewrite PTree.gso. auto. apply Plt_ne. eapply Genv.genv_symb_range; eauto. 
+      * rewrite PTree.gso. auto. apply Plt_ne. eapply Genv.genv_symb_range; eauto.
       * auto.
   }
   apply REC. red; intros. unfold Genv.find_symbol, Genv.empty_genv; simpl. rewrite ! PTree.gempty; auto.
@@ -421,7 +421,7 @@ Qed.
 Lemma transform_program_kept:
   forall id b, Genv.find_symbol tge id = Some b -> kept id.
 Proof.
-  intros. generalize (genv_program_map tp id). fold tge; rewrite H. 
+  intros. generalize (genv_program_map tp id). fold tge; rewrite H.
   rewrite transform_program_charact. intros. destruct (IS.mem id used) eqn:U.
   unfold kept; apply IS.mem_2; auto.
   contradiction.
@@ -454,7 +454,7 @@ Record meminj_preserves_globals (f: meminj) : Prop := {
 Definition init_meminj : meminj :=
   fun b =>
     match Genv.invert_symbol ge b with
-    | Some id => 
+    | Some id =>
         match Genv.find_symbol tge id with
         | Some b' => Some (b', 0)
         | None => None
@@ -471,7 +471,7 @@ Proof.
   destruct (Genv.invert_symbol ge b) as [id|] eqn:S; try discriminate.
   destruct (Genv.find_symbol tge id) as [b''|] eqn:F; inv H.
   split. auto. exists id. split. apply Genv.invert_find_symbol; auto. auto.
-Qed. 
+Qed.
 
 Lemma init_meminj_preserves_globals:
   meminj_preserves_globals init_meminj.
@@ -487,35 +487,35 @@ Proof.
   exists b'; auto. rewrite H2 in H1; contradiction.
 - generalize (genv_program_map tp id). fold tge. rewrite H. intros.
   destruct (program_map tp)!id as [gd|] eqn:PM; try contradiction.
-  generalize (transform_program_charact id). rewrite PM. 
+  generalize (transform_program_charact id). rewrite PM.
   destruct (IS.mem id used) eqn:USED; intros; try discriminate.
   generalize (genv_program_map p id). fold ge; fold pm.
   destruct (Genv.find_symbol ge id) as [b|] eqn:FS; intros; try congruence.
-  exists b; split; auto. unfold init_meminj. 
+  exists b; split; auto. unfold init_meminj.
   erewrite Genv.find_invert_symbol by eauto. rewrite H. auto.
 - exploit init_meminj_invert; eauto. intros (A & id & B & C).
   generalize (genv_program_map p id) (genv_program_map tp id). fold ge; fold tge; fold pm.
   rewrite transform_program_charact. rewrite B, C. intros.
   destruct (IS.mem id used) eqn:KEPT; try contradiction.
-  destruct (pm!id) as [gd|] eqn:PM; try contradiction. 
+  destruct (pm!id) as [gd|] eqn:PM; try contradiction.
   destruct gd as [fd'|gv'].
-  + assert (fd' = fd) by congruence. subst fd'. split. auto. split. auto. 
-    intros. eapply kept_closed; eauto. red; apply IS.mem_2; auto. 
+  + assert (fd' = fd) by congruence. subst fd'. split. auto. split. auto.
+    intros. eapply kept_closed; eauto. red; apply IS.mem_2; auto.
   + assert (b <> b) by (eapply Genv.genv_funs_vars; eassumption). congruence.
 - exploit init_meminj_invert; eauto. intros (A & id & B & C). split; auto.
   generalize (genv_program_map p id) (genv_program_map tp id). fold ge; fold tge; fold pm.
   rewrite transform_program_charact. rewrite B, C. intros.
   destruct (IS.mem id used); try contradiction.
-  destruct (pm!id) as [gd|]; try contradiction. 
-  destruct gd as [fd'|gv']. 
+  destruct (pm!id) as [gd|]; try contradiction.
+  destruct gd as [fd'|gv'].
   + assert (b <> b) by (eapply Genv.genv_funs_vars; eassumption). congruence.
   + congruence.
 - exploit init_meminj_invert; eauto. intros (A & id & B & C). split; auto.
   generalize (genv_program_map p id) (genv_program_map tp id). fold ge; fold tge; fold pm.
   rewrite transform_program_charact. rewrite B, C. intros.
   destruct (IS.mem id used); try contradiction.
-  destruct (pm!id) as [gd|]; try contradiction. 
-  destruct gd as [fd'|gv']. 
+  destruct (pm!id) as [gd|]; try contradiction.
+  destruct gd as [fd'|gv'].
   + assert (b' <> b') by (eapply Genv.genv_funs_vars; eassumption). congruence.
   + congruence.
 Qed.
@@ -523,28 +523,28 @@ Qed.
 Lemma globals_symbols_inject:
   forall j, meminj_preserves_globals j -> symbols_inject j ge tge.
 Proof.
-  intros. 
+  intros.
   assert (E1: Genv.genv_public ge = p.(prog_public)).
   { apply Genv.globalenv_public. }
   assert (E2: Genv.genv_public tge = p.(prog_public)).
-  { unfold tge; rewrite Genv.globalenv_public. 
+  { unfold tge; rewrite Genv.globalenv_public.
     unfold transform_program in TRANSF. rewrite USED_GLOBALS in TRANSF. inversion TRANSF. auto. }
   split; [|split;[|split]]; intros.
   + simpl; unfold Genv.public_symbol; rewrite E1, E2.
     destruct (Genv.find_symbol tge id) as [b'|] eqn:TFS.
-    exploit symbols_inject_3; eauto. intros (b & FS & INJ). rewrite FS. auto. 
+    exploit symbols_inject_3; eauto. intros (b & FS & INJ). rewrite FS. auto.
     destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto.
     destruct (in_dec ident_eq id (prog_public p)); simpl; auto.
-    exploit symbols_inject_2; eauto. apply kept_public; auto. 
+    exploit symbols_inject_2; eauto. apply kept_public; auto.
     intros (b' & TFS' & INJ). congruence.
-  + eapply symbols_inject_1; eauto. 
-  + simpl in *; unfold Genv.public_symbol in H0. 
+  + eapply symbols_inject_1; eauto.
+  + simpl in *; unfold Genv.public_symbol in H0.
     destruct (Genv.find_symbol ge id) as [b|] eqn:FS; try discriminate.
-    rewrite E1 in H0. 
+    rewrite E1 in H0.
     destruct (in_dec ident_eq id (prog_public p)); try discriminate. inv H1.
-    exploit symbols_inject_2; eauto. apply kept_public; auto. 
+    exploit symbols_inject_2; eauto. apply kept_public; auto.
     intros (b' & A & B); exists b'; auto.
-  + simpl. unfold Genv.block_is_volatile. 
+  + simpl. unfold Genv.block_is_volatile.
     destruct (Genv.find_var_info ge b1) as [gv|] eqn:V1.
     exploit var_info_inject; eauto. intros [A B]. rewrite A. auto.
     destruct (Genv.find_var_info tge b2) as [gv|] eqn:V2; auto.
@@ -552,14 +552,14 @@ Proof.
 Qed.
 
 Lemma symbol_address_inject:
-  forall j id ofs, 
+  forall j id ofs,
   meminj_preserves_globals j -> kept id ->
   Val.inject j (Genv.symbol_address ge id ofs) (Genv.symbol_address tge id ofs).
 Proof.
   intros. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto.
-  exploit symbols_inject_2; eauto. intros (b' & TFS & INJ). rewrite TFS. 
+  exploit symbols_inject_2; eauto. intros (b' & TFS & INJ). rewrite TFS.
   econstructor; eauto. rewrite Int.add_zero; auto.
-Qed. 
+Qed.
 
 (** Semantic preservation *)
 
@@ -569,7 +569,7 @@ Definition regset_inject (f: meminj) (rs rs': regset): Prop :=
 Lemma regs_inject:
   forall f rs rs', regset_inject f rs rs' -> forall l, Val.inject_list f rs##l rs'##l.
 Proof.
-  induction l; simpl. constructor. constructor; auto. 
+  induction l; simpl. constructor. constructor; auto.
 Qed.
 
 Lemma set_reg_inject:
@@ -577,7 +577,7 @@ Lemma set_reg_inject:
   regset_inject f rs rs' -> Val.inject f v v' ->
   regset_inject f (rs#r <- v) (rs'#r <- v').
 Proof.
-  intros; red; intros. rewrite ! Regmap.gsspec. destruct (peq r0 r); auto. 
+  intros; red; intros. rewrite ! Regmap.gsspec. destruct (peq r0 r); auto.
 Qed.
 
 Lemma set_res_inject:
@@ -585,13 +585,13 @@ Lemma set_res_inject:
   regset_inject f rs rs' -> Val.inject f v v' ->
   regset_inject f (regmap_setres res v rs) (regmap_setres res v' rs').
 Proof.
-  intros. destruct res; auto. apply set_reg_inject; auto. 
+  intros. destruct res; auto. apply set_reg_inject; auto.
 Qed.
 
 Lemma regset_inject_incr:
   forall f f' rs rs', regset_inject f rs rs' -> inject_incr f f' -> regset_inject f' rs rs'.
 Proof.
-  intros; red; intros. apply val_inject_incr with f; auto. 
+  intros; red; intros. apply val_inject_incr with f; auto.
 Qed.
 
 Lemma regset_undef_inject:
@@ -606,7 +606,7 @@ Lemma init_regs_inject:
   regset_inject f (init_regs args params) (init_regs args' params).
 Proof.
   induction 1; intros; destruct params; simpl; try (apply regset_undef_inject).
-  apply set_reg_inject; auto. 
+  apply set_reg_inject; auto.
 Qed.
 
 Inductive match_stacks (j: meminj):
@@ -631,7 +631,7 @@ Lemma match_stacks_preserves_globals:
   match_stacks j s ts bound tbound ->
   meminj_preserves_globals j.
 Proof.
-  induction 1; auto. 
+  induction 1; auto.
 Qed.
 
 Lemma match_stacks_incr:
@@ -645,7 +645,7 @@ Proof.
 - assert (SAME: forall b b' delta, Plt b (Genv.genv_next ge) ->
                                    j' b = Some(b', delta) -> j b = Some(b', delta)).
   { intros. destruct (j b) as [[b1 delta1] | ] eqn: J.
-    exploit H; eauto. congruence. 
+    exploit H; eauto. congruence.
     exploit H3; eauto. intros [A B]. elim (Plt_strict b).
     eapply Plt_Ple_trans. eauto. eapply Ple_trans; eauto. }
   assert (SAME': forall b b' delta, Plt b' (Genv.genv_next tge) ->
@@ -655,19 +655,19 @@ Proof.
     exploit H3; eauto. intros [A B]. elim (Plt_strict b').
     eapply Plt_Ple_trans. eauto. eapply Ple_trans; eauto. }
   constructor; auto.  constructor; intros.
-  + exploit symbols_inject_1; eauto. apply SAME; auto. 
-    eapply Genv.genv_symb_range; eauto. 
-  + exploit symbols_inject_2; eauto. intros (b' & A & B). 
+  + exploit symbols_inject_1; eauto. apply SAME; auto.
+    eapply Genv.genv_symb_range; eauto.
+  + exploit symbols_inject_2; eauto. intros (b' & A & B).
     exists b'; auto.
   + exploit symbols_inject_3; eauto. intros (b & A & B).
     exists b; auto.
-  + eapply funct_ptr_inject; eauto. apply SAME; auto. 
+  + eapply funct_ptr_inject; eauto. apply SAME; auto.
     eapply Genv.genv_funs_range; eauto.
-  + eapply var_info_inject; eauto. apply SAME; auto. 
+  + eapply var_info_inject; eauto. apply SAME; auto.
     eapply Genv.genv_vars_range; eauto.
-  + eapply var_info_rev_inject; eauto. apply SAME'; auto. 
+  + eapply var_info_rev_inject; eauto. apply SAME'; auto.
     eapply Genv.genv_vars_range; eauto.
-- econstructor; eauto. 
+- econstructor; eauto.
   apply IHmatch_stacks.
   intros. exploit H1; eauto. intros [A B]. split; eapply Ple_trans; eauto.
   apply Plt_Ple; auto. apply Plt_Ple; auto.
@@ -681,8 +681,8 @@ Lemma match_stacks_bound:
   match_stacks j s ts bound' tbound'.
 Proof.
   induction 1; intros.
-- constructor; auto. eapply Ple_trans; eauto. eapply Ple_trans; eauto.  
-- econstructor; eauto. eapply Plt_Ple_trans; eauto. eapply Plt_Ple_trans; eauto. 
+- constructor; auto. eapply Ple_trans; eauto. eapply Ple_trans; eauto.
+- econstructor; eauto. eapply Plt_Ple_trans; eauto. eapply Plt_Ple_trans; eauto.
 Qed.
 
 Inductive match_states: state -> state -> Prop :=
@@ -735,14 +735,14 @@ Lemma find_function_inject:
   find_function tge ros trs = Some fd /\ (forall id, ref_fundef fd id -> kept id).
 Proof.
   intros. destruct ros as [r|id]; simpl in *.
-- exploit Genv.find_funct_inv; eauto. intros (b & R). rewrite R in H0. 
-  rewrite Genv.find_funct_find_funct_ptr in H0. 
-  specialize (H1 r). rewrite R in H1. inv H1. 
-  exploit funct_ptr_inject; eauto. intros (A & B & C). 
+- exploit Genv.find_funct_inv; eauto. intros (b & R). rewrite R in H0.
+  rewrite Genv.find_funct_find_funct_ptr in H0.
+  specialize (H1 r). rewrite R in H1. inv H1.
+  exploit funct_ptr_inject; eauto. intros (A & B & C).
   rewrite B; auto.
 - destruct (Genv.find_symbol ge id) as [b|] eqn:FS; try discriminate.
-  exploit symbols_inject_2; eauto. intros (tb & P & Q). rewrite P. 
-  exploit funct_ptr_inject; eauto. intros (A & B & C). 
+  exploit symbols_inject_2; eauto. intros (tb & P & Q). rewrite P.
+  exploit funct_ptr_inject; eauto. intros (A & B & C).
   auto.
 Qed.
 
@@ -759,28 +759,28 @@ Lemma eval_builtin_arg_inject:
   /\ Val.inject j v v'.
 Proof.
   induction 1; intros SP GL RS MI K; simpl in K.
-- exists rs'#x; split; auto. constructor. 
+- exists rs'#x; split; auto. constructor.
 - econstructor; eauto with barg.
 - econstructor; eauto with barg.
 - econstructor; eauto with barg.
 - econstructor; eauto with barg.
-- simpl in H. exploit Mem.load_inject; eauto. rewrite Zplus_0_r. 
+- simpl in H. exploit Mem.load_inject; eauto. rewrite Zplus_0_r.
   intros (v' & A & B). exists v'; auto with barg.
 - econstructor; split; eauto with barg. simpl. econstructor; eauto. rewrite Int.add_zero; auto.
 - assert (Val.inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address tge id ofs)).
-  { unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. 
+  { unfold Senv.symbol_address; simpl; unfold Genv.symbol_address.
     destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto.
-    exploit symbols_inject_2; eauto. intros (b' & A & B). rewrite A. 
+    exploit symbols_inject_2; eauto. intros (b' & A & B). rewrite A.
     econstructor; eauto. rewrite Int.add_zero; auto. }
   exploit Mem.loadv_inject; eauto. intros (v' & A & B). exists v'; auto with barg.
 - econstructor; split; eauto with barg.
-  unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. 
+  unfold Senv.symbol_address; simpl; unfold Genv.symbol_address.
   destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto.
-  exploit symbols_inject_2; eauto. intros (b' & A & B). rewrite A. 
+  exploit symbols_inject_2; eauto. intros (b' & A & B). rewrite A.
   econstructor; eauto. rewrite Int.add_zero; auto.
 - destruct IHeval_builtin_arg1 as (v1' & A1 & B1); eauto using in_or_app.
   destruct IHeval_builtin_arg2 as (v2' & A2 & B2); eauto using in_or_app.
-  exists (Val.longofwords v1' v2'); split; auto with barg. 
+  exists (Val.longofwords v1' v2'); split; auto with barg.
   apply Val.longofwords_inject; auto.
 Qed.
 
@@ -796,11 +796,11 @@ Lemma eval_builtin_args_inject:
      eval_builtin_args tge (fun r => rs'#r) (Vptr sp' Int.zero) m' al vl'
   /\ Val.inject_list j vl vl'.
 Proof.
-  induction 1; intros. 
+  induction 1; intros.
 - exists (@nil val); split; constructor.
-- simpl in H5. 
+- simpl in H5.
   exploit eval_builtin_arg_inject; eauto using in_or_app. intros (v1' & A & B).
-  destruct IHlist_forall2 as (vl' & C & D); eauto using in_or_app. 
+  destruct IHlist_forall2 as (vl' & C & D); eauto using in_or_app.
   exists (v1' :: vl'); split; constructor; auto.
 Qed.
 
@@ -812,36 +812,36 @@ Proof.
   induction 1; intros; inv MS.
 
 - (* nop *)
-  econstructor; split. 
-  eapply exec_Inop; eauto. 
-  econstructor; eauto. 
+  econstructor; split.
+  eapply exec_Inop; eauto.
+  econstructor; eauto.
 
 - (* op *)
-  assert (A: exists tv, 
+  assert (A: exists tv,
                eval_operation tge (Vptr tsp Int.zero) op trs##args tm = Some tv
             /\ Val.inject j v tv).
-  { apply eval_operation_inj with (ge1 := ge) (m1 := m) (sp1 := Vptr sp0 Int.zero) (vl1 := rs##args). 
+  { apply eval_operation_inj with (ge1 := ge) (m1 := m) (sp1 := Vptr sp0 Int.zero) (vl1 := rs##args).
     intros; eapply Mem.valid_pointer_inject_val; eauto.
     intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
     intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
     intros; eapply Mem.different_pointers_inject; eauto.
     intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto.
     apply KEPT. red. exists pc, (Iop op args res pc'); auto.
-    econstructor; eauto. 
+    econstructor; eauto.
     apply regs_inject; auto.
     assumption. }
   destruct A as (tv & B & C).
   econstructor; split. eapply exec_Iop; eauto.
-  econstructor; eauto. apply set_reg_inject; auto. 
+  econstructor; eauto. apply set_reg_inject; auto.
 
 - (* load *)
-  assert (A: exists ta, 
+  assert (A: exists ta,
                eval_addressing tge (Vptr tsp Int.zero) addr trs##args = Some ta
             /\ Val.inject j a ta).
-  { apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Int.zero) (vl1 := rs##args). 
+  { apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Int.zero) (vl1 := rs##args).
     intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto.
     apply KEPT. red. exists pc, (Iload chunk addr args dst pc'); auto.
-    econstructor; eauto. 
+    econstructor; eauto.
     apply regs_inject; auto.
     assumption. }
   destruct A as (ta & B & C).
@@ -850,13 +850,13 @@ Proof.
   econstructor; eauto. apply set_reg_inject; auto.
 
 - (* store *)
-  assert (A: exists ta, 
+  assert (A: exists ta,
                eval_addressing tge (Vptr tsp Int.zero) addr trs##args = Some ta
             /\ Val.inject j a ta).
-  { apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Int.zero) (vl1 := rs##args). 
+  { apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Int.zero) (vl1 := rs##args).
     intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto.
     apply KEPT. red. exists pc, (Istore chunk addr args src pc'); auto.
-    econstructor; eauto. 
+    econstructor; eauto.
     apply regs_inject; auto.
     assumption. }
   destruct A as (ta & B & C).
@@ -865,45 +865,45 @@ Proof.
   econstructor; eauto.
 
 - (* call *)
-  exploit find_function_inject. 
-  eapply match_stacks_preserves_globals; eauto. eauto. 
+  exploit find_function_inject.
+  eapply match_stacks_preserves_globals; eauto. eauto.
   destruct ros as [r|id]. eauto. apply KEPT. red. econstructor; econstructor; split; eauto. simpl; auto.
   intros (A & B).
-  econstructor; split. eapply exec_Icall; eauto. 
-  econstructor; eauto. 
+  econstructor; split. eapply exec_Icall; eauto.
+  econstructor; eauto.
   econstructor; eauto.
-  change (Mem.valid_block m sp0). eapply Mem.valid_block_inject_1; eauto. 
-  change (Mem.valid_block tm tsp). eapply Mem.valid_block_inject_2; eauto. 
+  change (Mem.valid_block m sp0). eapply Mem.valid_block_inject_1; eauto.
+  change (Mem.valid_block tm tsp). eapply Mem.valid_block_inject_2; eauto.
   apply regs_inject; auto.
 
 - (* tailcall *)
-  exploit find_function_inject. 
-  eapply match_stacks_preserves_globals; eauto. eauto. 
+  exploit find_function_inject.
+  eapply match_stacks_preserves_globals; eauto. eauto.
   destruct ros as [r|id]. eauto. apply KEPT. red. econstructor; econstructor; split; eauto. simpl; auto.
   intros (A & B).
   exploit Mem.free_parallel_inject; eauto. rewrite ! Zplus_0_r. intros (tm' & C & D).
   econstructor; split.
-  eapply exec_Itailcall; eauto. 
-  econstructor; eauto. 
+  eapply exec_Itailcall; eauto.
+  econstructor; eauto.
   apply match_stacks_bound with stk tsp; auto.
-  apply Plt_Ple. 
+  apply Plt_Ple.
   change (Mem.valid_block m' stk). eapply Mem.valid_block_inject_1; eauto.
-  apply Plt_Ple. 
+  apply Plt_Ple.
   change (Mem.valid_block tm' tsp). eapply Mem.valid_block_inject_2; eauto.
   apply regs_inject; auto.
 
 - (* builtin *)
-  exploit eval_builtin_args_inject; eauto. 
+  exploit eval_builtin_args_inject; eauto.
   eapply match_stacks_preserves_globals; eauto.
-  intros. apply KEPT. red. econstructor; econstructor; eauto. 
+  intros. apply KEPT. red. econstructor; econstructor; eauto.
   intros (vargs' & P & Q).
-  exploit external_call_inject; eauto. 
+  exploit external_call_inject; eauto.
   eapply match_stacks_preserves_globals; eauto.
   intros (j' & tv & tm' & A & B & C & D & E & F & G).
   econstructor; split.
   eapply exec_Ibuiltin; eauto.
-  eapply match_states_regular with (j := j'); eauto. 
-  apply match_stacks_incr with j; auto. 
+  eapply match_states_regular with (j := j'); eauto.
+  apply match_stacks_incr with j; auto.
   intros. exploit G; eauto. intros [U V].
   assert (Mem.valid_block m sp0) by (eapply Mem.valid_block_inject_1; eauto).
   assert (Mem.valid_block tm tsp) by (eapply Mem.valid_block_inject_2; eauto).
@@ -914,52 +914,52 @@ Proof.
   assert (C: eval_condition cond trs##args tm = Some b).
   { eapply eval_condition_inject; eauto. apply regs_inject; auto. }
   econstructor; split.
-  eapply exec_Icond with (pc' := if b then ifso else ifnot); eauto. 
+  eapply exec_Icond with (pc' := if b then ifso else ifnot); eauto.
   econstructor; eauto.
 
 - (* jumptbl *)
   generalize (REGINJ arg); rewrite H0; intros INJ; inv INJ.
   econstructor; split.
-  eapply exec_Ijumptable; eauto. 
+  eapply exec_Ijumptable; eauto.
   econstructor; eauto.
 
 - (* return *)
   exploit Mem.free_parallel_inject; eauto. rewrite ! Zplus_0_r. intros (tm' & C & D).
   econstructor; split.
-  eapply exec_Ireturn; eauto. 
-  econstructor; eauto. 
+  eapply exec_Ireturn; eauto.
+  econstructor; eauto.
   apply match_stacks_bound with stk tsp; auto.
-  apply Plt_Ple. 
+  apply Plt_Ple.
   change (Mem.valid_block m' stk). eapply Mem.valid_block_inject_1; eauto.
-  apply Plt_Ple. 
+  apply Plt_Ple.
   change (Mem.valid_block tm' tsp). eapply Mem.valid_block_inject_2; eauto.
-  destruct or; simpl; auto. 
+  destruct or; simpl; auto.
 
 - (* internal function *)
-  exploit Mem.alloc_parallel_inject. eauto. eauto. apply Zle_refl. apply Zle_refl. 
+  exploit Mem.alloc_parallel_inject. eauto. eauto. apply Zle_refl. apply Zle_refl.
   intros (j' & tm' & tstk & C & D & E & F & G).
-  assert (STK: stk = Mem.nextblock m) by (eapply Mem.alloc_result; eauto). 
-  assert (TSTK: tstk = Mem.nextblock tm) by (eapply Mem.alloc_result; eauto). 
+  assert (STK: stk = Mem.nextblock m) by (eapply Mem.alloc_result; eauto).
+  assert (TSTK: tstk = Mem.nextblock tm) by (eapply Mem.alloc_result; eauto).
   assert (STACKS': match_stacks j' s ts stk tstk).
-  { rewrite STK, TSTK. 
-    apply match_stacks_incr with j; auto. 
-    intros. destruct (eq_block b1 stk). 
-    subst b1. rewrite F in H1; inv H1. subst b2. split; apply Ple_refl. 
+  { rewrite STK, TSTK.
+    apply match_stacks_incr with j; auto.
+    intros. destruct (eq_block b1 stk).
+    subst b1. rewrite F in H1; inv H1. subst b2. split; apply Ple_refl.
     rewrite G in H1 by auto. congruence. }
-  econstructor; split. 
+  econstructor; split.
   eapply exec_function_internal; eauto.
   eapply match_states_regular with (j := j'); eauto.
-  apply init_regs_inject; auto. apply val_inject_list_incr with j; auto. 
+  apply init_regs_inject; auto. apply val_inject_list_incr with j; auto.
 
 - (* external function *)
-  exploit external_call_inject; eauto. 
+  exploit external_call_inject; eauto.
   eapply match_stacks_preserves_globals; eauto.
   intros (j' & tres & tm' & A & B & C & D & E & F & G).
   econstructor; split.
   eapply exec_function_external; eauto.
   eapply match_states_return with (j := j'); eauto.
   apply match_stacks_bound with (Mem.nextblock m) (Mem.nextblock tm).
-  apply match_stacks_incr with j; auto. 
+  apply match_stacks_incr with j; auto.
   intros. exploit G; eauto. intros [P Q].
   unfold Mem.valid_block in *; xomega.
   eapply external_call_nextblock; eauto.
@@ -967,8 +967,8 @@ Proof.
 
 - (* return *)
   inv STACKS. econstructor; split.
-  eapply exec_return. 
-  econstructor; eauto. apply set_reg_inject; auto. 
+  eapply exec_return.
+  econstructor; eauto. apply set_reg_inject; auto.
 Qed.
 
 (** Relating initial memory states *)
@@ -976,11 +976,11 @@ Qed.
 Remark init_meminj_no_overlap:
   forall m, Mem.meminj_no_overlap init_meminj m.
 Proof.
-  intros; red; intros. 
+  intros; red; intros.
   exploit init_meminj_invert. eexact H0. intros (A1 & id1 & B1 & C1).
   exploit init_meminj_invert. eexact H1. intros (A2 & id2 & B2 & C2).
-  left; red; intros; subst b2'. 
-  assert (id1 = id2) by (eapply Genv.genv_vars_inj; eauto). 
+  left; red; intros; subst b2'.
+  assert (id1 = id2) by (eapply Genv.genv_vars_inj; eauto).
   congruence.
 Qed.
 
@@ -994,7 +994,7 @@ Lemma store_zeros_unmapped_inj:
 Proof.
   intros until m1'. functional induction (store_zeros m1 b1 i n); intros.
   inv H. auto.
-  eapply IHo; eauto. eapply Mem.store_unmapped_inj; eauto. 
+  eapply IHo; eauto. eapply Mem.store_unmapped_inj; eauto.
   discriminate.
 Qed.
 
@@ -1007,10 +1007,10 @@ Lemma store_zeros_mapped_inj:
   exists m2', store_zeros m2 b2 i n = Some m2' /\ Mem.mem_inj init_meminj m1' m2'.
 Proof.
   intros until m1'. functional induction (store_zeros m1 b1 i n); intros.
-  inv H. exists m2; split; auto. rewrite store_zeros_equation, e; auto. 
-  exploit Mem.store_mapped_inj; eauto. apply init_meminj_no_overlap. instantiate (1 := Vzero); constructor. 
+  inv H. exists m2; split; auto. rewrite store_zeros_equation, e; auto.
+  exploit Mem.store_mapped_inj; eauto. apply init_meminj_no_overlap. instantiate (1 := Vzero); constructor.
   intros (m2' & A & B). rewrite Zplus_0_r in A.
-  exploit IHo; eauto. intros (m3' & C & D). 
+  exploit IHo; eauto. intros (m3' & C & D).
   exists m3'; split; auto. rewrite store_zeros_equation, e, A, C; auto.
   discriminate.
 Qed.
@@ -1022,7 +1022,7 @@ Lemma store_init_data_unmapped_inj:
   init_meminj b1 = None ->
   Mem.mem_inj init_meminj m1' m2.
 Proof.
-  intros. destruct id; simpl in H; try (eapply Mem.store_unmapped_inj; now eauto). 
+  intros. destruct id; simpl in H; try (eapply Mem.store_unmapped_inj; now eauto).
   inv H; auto.
   destruct (Genv.find_symbol ge i0); try discriminate. eapply Mem.store_unmapped_inj; now eauto.
 Qed.
@@ -1039,8 +1039,8 @@ Proof.
   destruct init; simpl in *; try (eapply Mem.store_mapped_inj; now eauto).
   inv H. exists m2; auto.
   destruct (Genv.find_symbol ge i0) as [bi|] eqn:FS1; try discriminate.
-  exploit symbols_inject_2. eapply init_meminj_preserves_globals. eapply H2; eauto. eauto. 
-  intros (bi' & A & B). rewrite A. eapply Mem.store_mapped_inj; eauto. 
+  exploit symbols_inject_2. eapply init_meminj_preserves_globals. eapply H2; eauto. eauto.
+  intros (bi' & A & B). rewrite A. eapply Mem.store_mapped_inj; eauto.
   econstructor; eauto. rewrite Int.add_zero; auto.
 Qed.
 
@@ -1051,7 +1051,7 @@ Qed.
   init_meminj b1 = None ->
   Mem.mem_inj init_meminj m1' m2.
 Proof.
-  induction initlist; simpl; intros. 
+  induction initlist; simpl; intros.
 - inv H; auto.
 - destruct (Genv.store_init_data ge m1 b1 i a) as [m1''|] eqn:ST; try discriminate.
   eapply IHinitlist; eauto. eapply store_init_data_unmapped_inj; eauto.
@@ -1070,7 +1070,7 @@ Proof.
 - destruct (Genv.store_init_data ge m1 b1 i a) as [m1''|] eqn:ST; try discriminate.
   exploit store_init_data_mapped_inj; eauto. intros (m2'' & A & B).
   exploit IHinitlist; eauto. intros (m2' & C & D).
-  exists m2'; split; auto. rewrite A; auto. 
+  exists m2'; split; auto. rewrite A; auto.
 Qed.
 
 Lemma alloc_global_unmapped_inj:
@@ -1082,16 +1082,16 @@ Lemma alloc_global_unmapped_inj:
 Proof.
   unfold Genv.alloc_global; intros. destruct g as [fd|gv].
 - destruct (Mem.alloc m1 0 1) as (m1a, b) eqn:ALLOC.
-  exploit Mem.alloc_result; eauto. intros EQ. rewrite <- EQ in H1. 
-  eapply Mem.drop_unmapped_inj with (m1 := m1a); eauto. 
+  exploit Mem.alloc_result; eauto. intros EQ. rewrite <- EQ in H1.
+  eapply Mem.drop_unmapped_inj with (m1 := m1a); eauto.
   eapply Mem.alloc_left_unmapped_inj; eauto.
 - set (sz := Genv.init_data_list_size (gvar_init gv)) in *.
   destruct (Mem.alloc m1 0 sz) as (m1a, b) eqn:ALLOC.
   destruct (store_zeros m1a b 0 sz) as [m1b|] eqn: STZ; try discriminate.
   destruct (Genv.store_init_data_list ge m1b b 0 (gvar_init gv)) as [m1c|] eqn:ST; try discriminate.
-  exploit Mem.alloc_result; eauto. intros EQ. rewrite <- EQ in H1. 
+  exploit Mem.alloc_result; eauto. intros EQ. rewrite <- EQ in H1.
   eapply Mem.drop_unmapped_inj with (m1 := m1c); eauto.
-  eapply store_init_data_list_unmapped_inj with (m1 := m1b); eauto. 
+  eapply store_init_data_list_unmapped_inj with (m1 := m1b); eauto.
   eapply store_zeros_unmapped_inj with (m1 := m1a); eauto.
   eapply Mem.alloc_left_unmapped_inj; eauto.
 Qed.
@@ -1114,10 +1114,10 @@ Proof.
   { eapply Mem.alloc_left_mapped_inj with (b1 := b1) (b2 := b2) (delta := 0).
     eapply Mem.alloc_right_inj; eauto.
     eauto.
-    eauto with mem. 
+    eauto with mem.
     red; intros; apply Z.divide_0_r.
-    intros. apply Mem.perm_implies with Freeable; auto with mem. 
-    eapply Mem.perm_alloc_2; eauto. omega. 
+    intros. apply Mem.perm_implies with Freeable; auto with mem.
+    eapply Mem.perm_alloc_2; eauto. omega.
     auto.
   }
   exploit Mem.drop_mapped_inj; eauto. apply init_meminj_no_overlap.
@@ -1132,14 +1132,14 @@ Proof.
   { eapply Mem.alloc_left_mapped_inj with (b1 := b1) (b2 := b2) (delta := 0).
     eapply Mem.alloc_right_inj; eauto.
     eauto.
-    eauto with mem. 
+    eauto with mem.
     red; intros; apply Z.divide_0_r.
-    intros. apply Mem.perm_implies with Freeable; auto with mem. 
-    eapply Mem.perm_alloc_2; eauto. omega. 
+    intros. apply Mem.perm_implies with Freeable; auto with mem.
+    eapply Mem.perm_alloc_2; eauto. omega.
     auto.
   }
   exploit store_zeros_mapped_inj; eauto. intros (m2b & A & B).
-  exploit store_init_data_list_mapped_inj; eauto. 
+  exploit store_init_data_list_mapped_inj; eauto.
   intros. apply H2. red. exists ofs; auto. intros (m2c & C & D).
   exploit Mem.drop_mapped_inj; eauto. apply init_meminj_no_overlap. intros (m2' & E & F).
   exists m2'; split; auto. rewrite ! Zplus_0_r in E. rewrite A, C, E. auto.
@@ -1153,8 +1153,8 @@ Lemma alloc_globals_app:
   | Some m1 => Genv.alloc_globals g m1 defs2
   end.
 Proof.
-  induction defs1; simpl; intros. auto. 
-  destruct (Genv.alloc_global g m a); auto. 
+  induction defs1; simpl; intros. auto.
+  destruct (Genv.alloc_global g m a); auto.
 Qed.
 
 Lemma alloc_globals_snoc:
@@ -1166,7 +1166,7 @@ Lemma alloc_globals_snoc:
   end.
 Proof.
   intros. rewrite alloc_globals_app.
-  destruct (Genv.alloc_globals g m defs1); auto. unfold Genv.alloc_globals. 
+  destruct (Genv.alloc_globals g m defs1); auto. unfold Genv.alloc_globals.
   destruct (Genv.alloc_global g m0 id_def); auto.
 Qed.
 
@@ -1187,20 +1187,20 @@ Lemma alloc_globals_inj:
 Proof.
   induction defs; simpl; intros until g2; intros ALLOC GE1 GE2 NEXT1 SYMB1 SYMB2 SYMB3 PROGMAP.
 - inv ALLOC. exists Mem.empty. intuition auto. constructor; intros.
-  eelim Mem.perm_empty; eauto. 
-  exploit init_meminj_invert; eauto. intros [A B]. subst delta. apply Z.divide_0_r. 
   eelim Mem.perm_empty; eauto.
-- rewrite Genv.add_globals_app in GE1. simpl in GE1. 
+  exploit init_meminj_invert; eauto. intros [A B]. subst delta. apply Z.divide_0_r.
+  eelim Mem.perm_empty; eauto.
+- rewrite Genv.add_globals_app in GE1. simpl in GE1.
   set (g1' := Genv.add_globals (Genv.empty_genv fundef unit pubs) (rev defs)) in *.
   rewrite alloc_globals_snoc in ALLOC.
   destruct (Genv.alloc_globals ge Mem.empty (rev defs)) as [m1'|] eqn:ALLOC1'; try discriminate.
   exploit Genv.alloc_global_nextblock; eauto. intros NEXTBLOCK1.
-  assert (NEXTGE1: Genv.genv_next g1 = Pos.succ (Genv.genv_next g1')) by (rewrite GE1; reflexivity). 
+  assert (NEXTGE1: Genv.genv_next g1 = Pos.succ (Genv.genv_next g1')) by (rewrite GE1; reflexivity).
   assert (NEXT1': Mem.nextblock m1' = Genv.genv_next g1') by (unfold block in *; xomega).
   rewrite fold_left_app in PROGMAP. simpl in PROGMAP.
   destruct a as [id gd]. unfold add_def_prog_map at 1 in PROGMAP. simpl in PROGMAP.
   destruct (IS.mem id u) eqn:MEM.
-  + rewrite filter_globdefs_nil in *. rewrite alloc_globals_snoc. 
+  + rewrite filter_globdefs_nil in *. rewrite alloc_globals_snoc.
     rewrite Genv.add_globals_app in GE2. simpl in GE2.
     set (g2' := Genv.add_globals (Genv.empty_genv fundef unit pubs) (filter_globdefs (IS.remove id u) nil defs)) in *.
     assert (NEXTGE2: Genv.genv_next g2 = Pos.succ (Genv.genv_next g2')) by (rewrite GE2; reflexivity).
@@ -1209,15 +1209,15 @@ Proof.
       rewrite GE1. unfold Genv.find_symbol; simpl. rewrite PTree.gss. congruence. }
     exploit (IHdefs m1' (IS.remove id u) g1' g2'); eauto.
       intros. rewrite ISF.remove_iff in H; destruct H.
-      rewrite <- SYMB1 by auto. rewrite GE1. unfold Genv.find_symbol; simpl. 
+      rewrite <- SYMB1 by auto. rewrite GE1. unfold Genv.find_symbol; simpl.
       rewrite PTree.gso; auto.
       intros. rewrite ISF.remove_iff in H; destruct H.
-      rewrite <- SYMB2 by auto. rewrite GE2. unfold Genv.find_symbol; simpl. 
+      rewrite <- SYMB2 by auto. rewrite GE2. unfold Genv.find_symbol; simpl.
       rewrite PTree.gso; auto.
       intros. rewrite ISF.remove_iff. destruct (ident_eq id id0).
       subst id0. rewrite FS1 in H. inv H. eelim Plt_strict; eauto.
-      exploit SYMB3. eexact H. unfold block in *; xomega. auto. tauto. 
-      intros. rewrite ISF.remove_iff in H; destruct H. 
+      exploit SYMB3. eexact H. unfold block in *; xomega. auto. tauto.
+      intros. rewrite ISF.remove_iff in H; destruct H.
       rewrite <- PROGMAP by auto. rewrite PTree.gso by auto. auto.
     intros (m2' & A & B & C). fold g2' in B.
     assert (FS2: Genv.find_symbol tge id = Some (Mem.nextblock m2')).
@@ -1226,16 +1226,16 @@ Proof.
     assert (INJ: init_meminj (Mem.nextblock m1') = Some (Mem.nextblock m2', 0)).
     { apply Genv.find_invert_symbol in FS1. unfold init_meminj. rewrite FS1, FS2. auto. }
     exploit alloc_global_mapped_inj. eexact ALLOC. eexact C. exact INJ.
-    intros. apply kept_closed with id gd. eapply transform_program_kept; eauto. 
-    rewrite <- PROGMAP by (apply IS.mem_2; auto). apply PTree.gss. auto. 
+    intros. apply kept_closed with id gd. eapply transform_program_kept; eauto.
+    rewrite <- PROGMAP by (apply IS.mem_2; auto). apply PTree.gss. auto.
     intros (m2 & D & E).
-    exploit Genv.alloc_global_nextblock; eauto. intros NEXTBLOCK2. 
-    exists m2; split. rewrite A, D. auto. 
+    exploit Genv.alloc_global_nextblock; eauto. intros NEXTBLOCK2.
+    exists m2; split. rewrite A, D. auto.
     split. unfold block in *; xomega.
     auto.
-  + exploit (IHdefs m1' u g1' g2); auto. 
-    intros. rewrite <- SYMB1 by auto. rewrite GE1. 
-    unfold Genv.find_symbol; simpl. rewrite PTree.gso; auto. 
+  + exploit (IHdefs m1' u g1' g2); auto.
+    intros. rewrite <- SYMB1 by auto. rewrite GE1.
+    unfold Genv.find_symbol; simpl. rewrite PTree.gso; auto.
     red; intros; subst id0. apply IS.mem_1 in H. congruence.
     intros. eapply SYMB3; eauto. unfold block in *; xomega.
     intros. rewrite <- PROGMAP by auto. rewrite PTree.gso; auto.
@@ -1248,8 +1248,8 @@ Proof.
       eapply transform_program_kept; eauto.
       intros P.
       revert V. rewrite <- SYMB1, GE1 by auto. unfold Genv.find_symbol; simpl.
-      rewrite PTree.gsspec. rewrite NEXT1'. destruct (peq id1 id); intros Q. 
-      subst id1. apply IS.mem_1 in P. congruence. 
+      rewrite PTree.gsspec. rewrite NEXT1'. destruct (peq id1 id); intros Q.
+      subst id1. apply IS.mem_1 in P. congruence.
       eelim Plt_strict. eapply Genv.genv_symb_range; eauto. }
     exists m2; intuition auto. eapply alloc_global_unmapped_inj; eauto.
 Qed.
@@ -1262,15 +1262,15 @@ Proof.
   intros.
   unfold transform_program in TRANSF; rewrite USED_GLOBALS in TRANSF; injection TRANSF. intros EQ.
   destruct (alloc_globals_inj (prog_public p) (List.rev (prog_defs p)) m used ge tge) as (tm & A & B & C).
-  rewrite rev_involutive; auto. 
+  rewrite rev_involutive; auto.
   rewrite rev_involutive; auto.
   unfold tge; rewrite <- EQ; auto.
-  symmetry. apply Genv.init_mem_genv_next; auto. 
+  symmetry. apply Genv.init_mem_genv_next; auto.
   auto. auto. auto.
   intros. rewrite rev_involutive. auto.
   assert (D: Genv.init_mem tp = Some tm).
   { unfold Genv.init_mem. fold tge. rewrite <- EQ. exact A. }
-  pose proof (init_meminj_preserves_globals). 
+  pose proof (init_meminj_preserves_globals).
   exists init_meminj, tm; intuition auto.
   constructor; intros.
   + auto.
@@ -1280,7 +1280,7 @@ Proof.
   + exploit init_meminj_invert; eauto. intros (P & id & Q & R).
     eapply Genv.find_symbol_not_fresh; eauto.
   + apply init_meminj_no_overlap.
-  + exploit init_meminj_invert; eauto. intros (P & id & Q & R). 
+  + exploit init_meminj_invert; eauto. intros (P & id & Q & R).
     split. omega. generalize (Int.unsigned_range_2 ofs). omega.
 Qed.
 
@@ -1289,28 +1289,28 @@ Lemma transf_initial_states:
 Proof.
   intros. inv H. exploit init_mem_inject; eauto. intros (j & tm & A & B & C).
   exploit symbols_inject_2. eauto. apply kept_main. eexact H1. intros (tb & P & Q).
-  exploit funct_ptr_inject. eauto. eexact Q. exact H2. 
+  exploit funct_ptr_inject. eauto. eexact Q. exact H2.
   intros (R & S & T).
   exists (Callstate nil f nil tm); split.
   econstructor; eauto.
-    fold tge. unfold transform_program in TRANSF; rewrite USED_GLOBALS in TRANSF; inversion TRANSF; auto. 
+    fold tge. unfold transform_program in TRANSF; rewrite USED_GLOBALS in TRANSF; inversion TRANSF; auto.
   econstructor; eauto.
-  constructor. auto. 
-  erewrite <- Genv.init_mem_genv_next by eauto. apply Ple_refl. 
-  erewrite <- Genv.init_mem_genv_next by eauto. apply Ple_refl. 
+  constructor. auto.
+  erewrite <- Genv.init_mem_genv_next by eauto. apply Ple_refl.
+  erewrite <- Genv.init_mem_genv_next by eauto. apply Ple_refl.
 Qed.
 
 Lemma transf_final_states:
   forall S1 S2 r,
   match_states S1 S2 -> final_state S1 r -> final_state S2 r.
 Proof.
-  intros. inv H0. inv H. inv STACKS. inv RESINJ. constructor. 
+  intros. inv H0. inv H. inv STACKS. inv RESINJ. constructor.
 Qed.
 
 Theorem transf_program_correct:
   forward_simulation (semantics p) (semantics tp).
 Proof.
-  intros. 
+  intros.
   eapply forward_simulation_step.
   exploit globals_symbols_inject. apply init_meminj_preserves_globals. intros [A B]. exact A.
   eexact transf_initial_states.