Updated PR by removing whitespaces. Bug 17450.

1 files changed, 282 insertions, 282 deletions

diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index 30f03654..5f78ea6b 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -14,11 +14,11 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Global environments are a component of the dynamic semantics of 
+(** Global environments are a component of the dynamic semantics of
   all languages involved in the compiler.  A global environment
   maps symbol names (names of functions and of global variables)
   to the corresponding memory addresses.  It also maps memory addresses
-  of functions to the corresponding function descriptions.  
+  of functions to the corresponding function descriptions.
 
   Global environments, along with the initial memory state at the beginning
   of program execution, are built from the program of interest, as follows:
@@ -110,7 +110,7 @@ Theorem shift_symbol_address:
   forall ge id ofs n,
   symbol_address ge id (Int.add ofs n) = Val.add (symbol_address ge id ofs) (Vint n).
 Proof.
-  intros. unfold symbol_address. destruct (find_symbol ge id); auto. 
+  intros. unfold symbol_address. destruct (find_symbol ge id); auto.
 Qed.
 
 End Senv.
@@ -137,7 +137,7 @@ Record t: Type := mkgenv {
   genv_vars_range: forall b v, PTree.get b genv_vars = Some v -> Plt b genv_next;
   genv_funs_vars: forall b1 b2 f v,
     PTree.get b1 genv_funs = Some f -> PTree.get b2 genv_vars = Some v -> b1 <> b2;
-  genv_vars_inj: forall id1 id2 b, 
+  genv_vars_inj: forall id1 id2 b,
     PTree.get id1 genv_symb = Some b -> PTree.get id2 genv_symb = Some b -> id1 = id2
 }.
 
@@ -225,18 +225,18 @@ Next Obligation.
   apply Plt_trans_succ; eauto.
 Qed.
 Next Obligation.
-  destruct ge; simpl in *. 
-  destruct g. 
-  rewrite PTree.gsspec in H. 
+  destruct ge; simpl in *.
+  destruct g.
+  rewrite PTree.gsspec in H.
   destruct (peq b genv_next0). inv H. apply Plt_succ.
   apply Plt_trans_succ; eauto.
   apply Plt_trans_succ; eauto.
 Qed.
 Next Obligation.
-  destruct ge; simpl in *. 
+  destruct ge; simpl in *.
   destruct g.
   apply Plt_trans_succ; eauto.
-  rewrite PTree.gsspec in H. 
+  rewrite PTree.gsspec in H.
   destruct (peq b genv_next0). inv H. apply Plt_succ.
   apply Plt_trans_succ; eauto.
 Qed.
@@ -253,8 +253,8 @@ Next Obligation.
   eauto.
 Qed.
 Next Obligation.
-  destruct ge; simpl in *. 
-  rewrite PTree.gsspec in H. rewrite PTree.gsspec in H0. 
+  destruct ge; simpl in *.
+  rewrite PTree.gsspec in H. rewrite PTree.gsspec in H0.
   destruct (peq id1 i); destruct (peq id2 i).
   congruence.
   inv H. eelim Plt_strict. eapply genv_symb_range0; eauto.
@@ -304,9 +304,9 @@ Lemma add_globals_preserves:
   (forall ge id g, P ge -> In (id, g) gl -> P (add_global ge (id, g))) ->
   P ge -> P (add_globals ge gl).
 Proof.
-  induction gl; simpl; intros. 
+  induction gl; simpl; intros.
   auto.
-  destruct a. apply IHgl; auto. 
+  destruct a. apply IHgl; auto.
 Qed.
 
 Lemma add_globals_ensures:
@@ -317,8 +317,8 @@ Lemma add_globals_ensures:
 Proof.
   induction gl; simpl; intros.
   contradiction.
-  destruct H1. subst a. apply add_globals_preserves; auto. 
-  apply IHgl; auto. 
+  destruct H1. subst a. apply add_globals_preserves; auto.
+  apply IHgl; auto.
 Qed.
 
 Lemma add_globals_unique_preserves:
@@ -326,9 +326,9 @@ Lemma add_globals_unique_preserves:
   (forall ge id1 g, P ge -> In (id1, g) gl -> id1 <> id -> P (add_global ge (id1, g))) ->
   ~In id (map fst gl) -> P ge -> P (add_globals ge gl).
 Proof.
-  induction gl; simpl; intros. 
+  induction gl; simpl; intros.
   auto.
-  destruct a. apply IHgl; auto. 
+  destruct a. apply IHgl; auto.
 Qed.
 
 Lemma add_globals_unique_ensures:
@@ -347,10 +347,10 @@ Remark in_norepet_unique:
 Proof.
   induction gl as [|[id1 g1] gl]; simpl; intros.
   contradiction.
-  inv H0. destruct H. 
-  inv H. exists nil, gl. auto. 
-  exploit IHgl; eauto. intros (gl1 & gl2 & X & Y). 
-  exists ((id1, g1) :: gl1), gl2; split; auto. rewrite X; auto. 
+  inv H0. destruct H.
+  inv H. exists nil, gl. auto.
+  exploit IHgl; eauto. intros (gl1 & gl2 & X & Y).
+  exists ((id1, g1) :: gl1), gl2; split; auto. rewrite X; auto.
 Qed.
 
 Lemma add_globals_norepet_ensures:
@@ -359,8 +359,8 @@ Lemma add_globals_norepet_ensures:
   (forall ge, P (add_global ge (id, g))) ->
   In (id, g) gl -> list_norepet (map fst gl) -> P (add_globals ge gl).
 Proof.
-  intros. exploit in_norepet_unique; eauto. intros (gl1 & gl2 & X & Y). 
-  subst gl. apply add_globals_unique_ensures; auto. intros. eapply H; eauto. 
+  intros. exploit in_norepet_unique; eauto. intros (gl1 & gl2 & X & Y).
+  subst gl. apply add_globals_unique_ensures; auto. intros. eapply H; eauto.
   apply in_or_app; simpl; auto.
 Qed.
 
@@ -371,7 +371,7 @@ End GLOBALENV_PRINCIPLES.
 Theorem public_symbol_exists:
   forall ge id, public_symbol ge id = true -> exists b, find_symbol ge id = Some b.
 Proof.
-  unfold public_symbol; intros. destruct (find_symbol ge id) as [b|]. 
+  unfold public_symbol; intros. destruct (find_symbol ge id) as [b|].
   exists b; auto.
   discriminate.
 Qed.
@@ -380,15 +380,15 @@ Theorem shift_symbol_address:
   forall ge id ofs n,
   symbol_address ge id (Int.add ofs n) = Val.add (symbol_address ge id ofs) (Vint n).
 Proof.
-  intros. unfold symbol_address. destruct (find_symbol ge id); auto. 
+  intros. unfold symbol_address. destruct (find_symbol ge id); auto.
 Qed.
 
 Theorem find_funct_inv:
   forall ge v f,
   find_funct ge v = Some f -> exists b, v = Vptr b Int.zero.
 Proof.
-  intros until f; unfold find_funct. 
-  destruct v; try congruence. 
+  intros until f; unfold find_funct.
+  destruct v; try congruence.
   destruct (Int.eq_dec i Int.zero); try congruence.
   intros. exists b; congruence.
 Qed.
@@ -428,7 +428,7 @@ Proof.
   rewrite PTree.gso; auto.
   destruct g1 as [f1 | v1]. rewrite PTree.gso. auto.
   apply Plt_ne. eapply genv_funs_range; eauto.
-  auto. 
+  auto.
 (* ensures *)
   intros. unfold find_symbol, find_funct_ptr in *; simpl.
   exists (genv_next ge); split. apply PTree.gss. apply PTree.gss.
@@ -442,8 +442,8 @@ Corollary find_funct_ptr_exists:
      find_symbol (globalenv p) id = Some b
   /\ find_funct_ptr (globalenv p) b = Some f.
 Proof.
-  intros. exploit in_norepet_unique; eauto. intros (gl1 & gl2 & X & Y). 
-  eapply find_funct_ptr_exists_2; eauto. 
+  intros. exploit in_norepet_unique; eauto. intros (gl1 & gl2 & X & Y).
+  eapply find_funct_ptr_exists_2; eauto.
 Qed.
 
 Theorem find_var_exists_2:
@@ -462,7 +462,7 @@ Proof.
   apply Plt_ne. eapply genv_vars_range; eauto.
 (* ensures *)
   intros. unfold find_symbol, find_var_info in *; simpl.
-  exists (genv_next ge); split. apply PTree.gss. apply PTree.gss. 
+  exists (genv_next ge); split. apply PTree.gss. apply PTree.gss.
 Qed.
 
 Corollary find_var_exists:
@@ -473,8 +473,8 @@ Corollary find_var_exists:
      find_symbol (globalenv p) id = Some b
   /\ find_var_info (globalenv p) b = Some v.
 Proof.
-  intros. exploit in_norepet_unique; eauto. intros (gl1 & gl2 & X & Y). 
-  eapply find_var_exists_2; eauto. 
+  intros. exploit in_norepet_unique; eauto. intros (gl1 & gl2 & X & Y).
+  eapply find_var_exists_2; eauto.
 Qed.
 
 Lemma find_symbol_inversion : forall p x b,
@@ -483,7 +483,7 @@ Lemma find_symbol_inversion : forall p x b,
 Proof.
   intros until b; unfold globalenv. eapply add_globals_preserves.
 (* preserves *)
-  unfold find_symbol; simpl; intros. rewrite PTree.gsspec in H1. 
+  unfold find_symbol; simpl; intros. rewrite PTree.gsspec in H1.
   destruct (peq x id). subst x. change id with (fst (id, g)). apply List.in_map; auto.
   auto.
 (* base *)
@@ -495,9 +495,9 @@ Theorem find_funct_ptr_inversion:
   find_funct_ptr (globalenv p) b = Some f ->
   exists id, In (id, Gfun f) (prog_defs p).
 Proof.
-  intros until f. unfold globalenv. apply add_globals_preserves. 
+  intros until f. unfold globalenv. apply add_globals_preserves.
 (* preserves *)
-  unfold find_funct_ptr; simpl; intros. destruct g; auto. 
+  unfold find_funct_ptr; simpl; intros. destruct g; auto.
   rewrite PTree.gsspec in H1. destruct (peq b (genv_next ge)).
   inv H1. exists id; auto.
   auto.
@@ -510,7 +510,7 @@ Theorem find_funct_inversion:
   find_funct (globalenv p) v = Some f ->
   exists id, In (id, Gfun f) (prog_defs p).
 Proof.
-  intros. exploit find_funct_inv; eauto. intros [b EQ]. subst v. 
+  intros. exploit find_funct_inv; eauto. intros [b EQ]. subst v.
   rewrite find_funct_find_funct_ptr in H.
   eapply find_funct_ptr_inversion; eauto.
 Qed.
@@ -539,9 +539,9 @@ Theorem find_funct_ptr_symbol_inversion:
   find_funct_ptr (globalenv p) b = Some f ->
   In (id, Gfun f) p.(prog_defs).
 Proof.
-  intros until f. unfold globalenv, find_symbol, find_funct_ptr. apply add_globals_preserves. 
+  intros until f. unfold globalenv, find_symbol, find_funct_ptr. apply add_globals_preserves.
 (* preserves *)
-  intros. simpl in *. rewrite PTree.gsspec in H1. destruct (peq id id0). 
+  intros. simpl in *. rewrite PTree.gsspec in H1. destruct (peq id id0).
   inv H1. destruct g as [f1|v1]. rewrite PTree.gss in H2. inv H2. auto.
   eelim Plt_strict. eapply genv_funs_range; eauto.
   destruct g as [f1|v1]. rewrite PTree.gso in H2. auto.
@@ -559,7 +559,7 @@ Theorem global_addresses_distinct:
   find_symbol ge id2 = Some b2 ->
   b1 <> b2.
 Proof.
-  intros. red; intros; subst. elim H. destruct ge. eauto. 
+  intros. red; intros; subst. elim H. destruct ge. eauto.
 Qed.
 
 Theorem invert_find_symbol:
@@ -568,9 +568,9 @@ Theorem invert_find_symbol:
 Proof.
   intros until b; unfold find_symbol, invert_symbol.
   apply PTree_Properties.fold_rec.
-  intros. rewrite H in H0; auto. 
+  intros. rewrite H in H0; auto.
   congruence.
-  intros. destruct (eq_block b v). inv H2. apply PTree.gss. 
+  intros. destruct (eq_block b v). inv H2. apply PTree.gss.
   rewrite PTree.gsspec. destruct (peq id k).
   subst. assert (m!k = Some b) by auto. congruence.
   auto.
@@ -588,9 +588,9 @@ Proof.
   rewrite PTree.gempty; congruence.
   intros. destruct (eq_block b v). exists k; auto.
   rewrite PTree.gsspec in H2. destruct (peq id k).
-  inv H2. congruence. auto. 
+  inv H2. congruence. auto.
 
-  intros; exploit H; eauto. intros [id' A]. 
+  intros; exploit H; eauto. intros [id' A].
   assert (id = id'). eapply genv_vars_inj; eauto. apply invert_find_symbol; auto.
   congruence.
 Qed.
@@ -604,14 +604,14 @@ Remark genv_next_add_globals:
 Proof.
   induction gl; simpl; intros.
   auto.
-  rewrite IHgl. auto. 
+  rewrite IHgl. auto.
 Qed.
 
 Remark genv_public_add_globals:
   forall gl ge,
   genv_public (add_globals ge gl) = genv_public ge.
 Proof.
-  induction gl; simpl; intros. 
+  induction gl; simpl; intros.
   auto.
   rewrite IHgl; auto.
 Qed.
@@ -619,7 +619,7 @@ Qed.
 Theorem globalenv_public:
   forall p, genv_public (globalenv p) = prog_public p.
 Proof.
-  unfold globalenv; intros. rewrite genv_public_add_globals. auto. 
+  unfold globalenv; intros. rewrite genv_public_add_globals. auto.
 Qed.
 
 Theorem block_is_volatile_below:
@@ -765,11 +765,11 @@ Remark store_init_data_list_nextblock:
 Proof.
   induction idl; simpl; intros until m'.
   intros. congruence.
-  caseEq (store_init_data m b p a); try congruence. intros. 
-  transitivity (Mem.nextblock m0). eauto. 
+  caseEq (store_init_data m b p a); try congruence. intros.
+  transitivity (Mem.nextblock m0). eauto.
   destruct a; simpl in H; try (eapply Mem.nextblock_store; eauto; fail).
   congruence.
-  destruct (find_symbol ge i); try congruence. eapply Mem.nextblock_store; eauto. 
+  destruct (find_symbol ge i); try congruence. eapply Mem.nextblock_store; eauto.
 Qed.
 
 Remark alloc_global_nextblock:
@@ -778,10 +778,10 @@ Remark alloc_global_nextblock:
   Mem.nextblock m' = Psucc(Mem.nextblock m).
 Proof.
   unfold alloc_global. intros.
-  destruct g as [id [f|v]]. 
+  destruct g as [id [f|v]].
   (* function *)
   destruct (Mem.alloc m 0 1) as [m1 b] eqn:?.
-  erewrite Mem.nextblock_drop; eauto. erewrite Mem.nextblock_alloc; eauto. 
+  erewrite Mem.nextblock_drop; eauto. erewrite Mem.nextblock_alloc; eauto.
   (* variable *)
   set (init := gvar_init v) in *.
   set (sz := init_data_list_size init) in *.
@@ -824,13 +824,13 @@ Remark store_init_data_list_perm:
   (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm).
 Proof.
   induction idl; simpl; intros until m'.
-  intros. inv H. tauto. 
+  intros. inv H. tauto.
   caseEq (store_init_data m b p a); try congruence. intros.
   rewrite <- (IHidl _ _ _ _ H0).
   assert (forall chunk v,
           Mem.store chunk m b p v = Some m0 ->
           (Mem.perm m b' q k prm <-> Mem.perm m0 b' q k prm)).
-    intros; split; eauto with mem. 
+    intros; split; eauto with mem.
   destruct a; simpl in H; eauto.
   inv H; tauto.
   destruct (find_symbol ge i). eauto. discriminate.
@@ -842,13 +842,13 @@ Remark alloc_global_perm:
   Mem.valid_block m b' ->
   (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm).
 Proof.
-  intros. destruct idg as [id [f|v]]; simpl in H. 
+  intros. destruct idg as [id [f|v]]; simpl in H.
   (* function *)
-  destruct (Mem.alloc m 0 1) as [m1 b] eqn:?. 
+  destruct (Mem.alloc m 0 1) as [m1 b] eqn:?.
   assert (b' <> b). apply Mem.valid_not_valid_diff with m; eauto with mem.
   split; intros.
-  eapply Mem.perm_drop_3; eauto. eapply Mem.perm_alloc_1; eauto. 
-  eapply Mem.perm_alloc_4; eauto. eapply Mem.perm_drop_4; eauto. 
+  eapply Mem.perm_drop_3; eauto. eapply Mem.perm_alloc_1; eauto.
+  eapply Mem.perm_alloc_4; eauto. eapply Mem.perm_drop_4; eauto.
   (* variable *)
   set (init := gvar_init v) in *.
   set (sz := init_data_list_size init) in *.
@@ -860,11 +860,11 @@ Proof.
   eapply Mem.perm_drop_3; eauto.
   erewrite <- store_init_data_list_perm; [idtac|eauto].
   erewrite <- store_zeros_perm; [idtac|eauto].
-  eapply Mem.perm_alloc_1; eauto. 
+  eapply Mem.perm_alloc_1; eauto.
   eapply Mem.perm_alloc_4; eauto.
   erewrite store_zeros_perm; [idtac|eauto].
-  erewrite store_init_data_list_perm; [idtac|eauto]. 
-  eapply Mem.perm_drop_4; eauto. 
+  erewrite store_init_data_list_perm; [idtac|eauto].
+  eapply Mem.perm_drop_4; eauto.
 Qed.
 
 Remark alloc_globals_perm:
@@ -876,7 +876,7 @@ Proof.
   induction gl.
   simpl; intros. inv H. tauto.
   simpl; intros. destruct (alloc_global m a) as [m1|] eqn:?; try discriminate.
-  erewrite alloc_global_perm; eauto. eapply IHgl; eauto. 
+  erewrite alloc_global_perm; eauto. eapply IHgl; eauto.
   unfold Mem.valid_block in *. erewrite alloc_global_nextblock; eauto.
   apply Plt_trans_succ; auto.
 Qed.
@@ -892,9 +892,9 @@ Remark store_zeros_load_outside:
 Proof.
   intros until n. functional induction (store_zeros m b p n); intros.
   inv H; auto.
-  transitivity (Mem.load chunk m' b' p'). 
-  apply IHo. auto. intuition omega. 
-  eapply Mem.load_store_other; eauto. simpl. intuition omega. 
+  transitivity (Mem.load chunk m' b' p').
+  apply IHo. auto. intuition omega.
+  eapply Mem.load_store_other; eauto. simpl. intuition omega.
   discriminate.
 Qed.
 
@@ -907,15 +907,15 @@ Remark store_zeros_loadbytes_outside:
 Proof.
   intros until n. functional induction (store_zeros m b p n); intros.
   inv H; auto.
-  transitivity (Mem.loadbytes m' b' p' n'). 
+  transitivity (Mem.loadbytes m' b' p' n').
   apply IHo. auto. intuition omega.
-  eapply Mem.loadbytes_store_other; eauto. simpl. intuition omega. 
+  eapply Mem.loadbytes_store_other; eauto. simpl. intuition omega.
   discriminate.
 Qed.
 
 Definition read_as_zero (m: mem) (b: block) (ofs len: Z) : Prop :=
   forall chunk p,
-  ofs <= p -> p + size_chunk chunk <= ofs + len -> 
+  ofs <= p -> p + size_chunk chunk <= ofs + len ->
   (align_chunk chunk | p) ->
   Mem.load chunk m b p =
   Some (match chunk with
@@ -938,18 +938,18 @@ Proof.
   rewrite inj_S in H1. omegaContradiction.
 - destruct (zeq p' p).
   + subst p'. destruct n'. simpl. apply Mem.loadbytes_empty. omega.
-    rewrite inj_S in H1. rewrite inj_S. 
+    rewrite inj_S in H1. rewrite inj_S.
     replace (Z.succ (Z.of_nat n')) with (1 + Z.of_nat n') by omega.
     change (list_repeat (S n') (Byte Byte.zero))
       with ((Byte Byte.zero :: nil) ++ list_repeat n' (Byte Byte.zero)).
-    apply Mem.loadbytes_concat. 
+    apply Mem.loadbytes_concat.
     erewrite store_zeros_loadbytes_outside; eauto.
     change (Byte Byte.zero :: nil) with (encode_val Mint8unsigned Vzero).
     change 1 with (size_chunk Mint8unsigned).
-    eapply Mem.loadbytes_store_same; eauto. 
+    eapply Mem.loadbytes_store_same; eauto.
     right; omega.
-    eapply IHo; eauto. omega. omega. omega. omega. 
-  + eapply IHo; eauto. omega. omega. 
+    eapply IHo; eauto. omega. omega. omega. omega.
+  + eapply IHo; eauto. omega. omega.
 - discriminate.
 Qed.
 
@@ -960,9 +960,9 @@ Lemma store_zeros_read_as_zero:
 Proof.
   intros; red; intros.
   transitivity (Some(decode_val chunk (list_repeat (size_chunk_nat chunk) (Byte Byte.zero)))).
-  apply Mem.loadbytes_load; auto. rewrite size_chunk_conv. 
-  eapply store_zeros_loadbytes; eauto. rewrite <- size_chunk_conv; auto. 
-  f_equal. destruct chunk; reflexivity. 
+  apply Mem.loadbytes_load; auto. rewrite size_chunk_conv.
+  eapply store_zeros_loadbytes; eauto. rewrite <- size_chunk_conv; auto.
+  f_equal. destruct chunk; reflexivity.
 Qed.
 
 Remark store_init_data_outside:
@@ -974,8 +974,8 @@ Remark store_init_data_outside:
 Proof.
   intros. destruct i; simpl in *;
   try (eapply Mem.load_store_other; eauto; fail).
-  inv H; auto. 
-  destruct (find_symbol ge i); try congruence. 
+  inv H; auto.
+  destruct (find_symbol ge i); try congruence.
   eapply Mem.load_store_other; eauto; intuition.
 Qed.
 
@@ -991,7 +991,7 @@ Proof.
   intros. destruct (store_init_data m b p a) as [m1|] eqn:?; try congruence.
   transitivity (Mem.load chunk m1 b' q).
   eapply IHil; eauto. generalize (init_data_size_pos a). intuition omega.
-  eapply store_init_data_outside; eauto. tauto. 
+  eapply store_init_data_outside; eauto. tauto.
 Qed.
 
 Fixpoint load_store_init_data (m: mem) (b: block) (p: Z) (il: list init_data) {struct il} : Prop :=
@@ -1041,17 +1041,17 @@ Proof.
     Mem.load chunk m' b p = Some(Val.load_result chunk v)).
   {
     intros. transitivity (Mem.load chunk m1 b p).
-    eapply store_init_data_list_outside; eauto. right. omega. 
-    eapply Mem.load_store_same; eauto. 
+    eapply store_init_data_list_outside; eauto. right. omega.
+    eapply Mem.load_store_same; eauto.
   }
   induction il; simpl.
   auto.
   intros. destruct (store_init_data m b p a) as [m1|] eqn:?; try congruence.
   exploit IHil; eauto.
-  red; intros. transitivity (Mem.load chunk m b p0). 
-  eapply store_init_data_outside. eauto. auto. 
-  apply H0. generalize (init_data_size_pos a); omega. omega. auto.  
-  intro D. 
+  red; intros. transitivity (Mem.load chunk m b p0).
+  eapply store_init_data_outside. eauto. auto.
+  apply H0. generalize (init_data_size_pos a); omega. omega. auto.
+  intro D.
   destruct a; simpl in Heqo; intuition.
   eapply (A Mint8unsigned (Vint i)); eauto.
   eapply (A Mint16unsigned (Vint i)); eauto.
@@ -1059,11 +1059,11 @@ Proof.
   eapply (A Mint64 (Vlong i)); eauto.
   eapply (A Mfloat32 (Vsingle f)); eauto.
   eapply (A Mfloat64 (Vfloat f)); eauto.
-  inv Heqo. red; intros. transitivity (Mem.load chunk m1 b p0). 
-  eapply store_init_data_list_outside; eauto. right. simpl. xomega. 
+  inv Heqo. red; intros. transitivity (Mem.load chunk m1 b p0).
+  eapply store_init_data_list_outside; eauto. right. simpl. xomega.
   apply H0; auto. simpl. generalize (init_data_list_size_pos il); xomega.
-  destruct (find_symbol ge i); try congruence. exists b0; split; auto. 
-  eapply (A Mint32 (Vptr b0 i0)); eauto. 
+  destruct (find_symbol ge i); try congruence. exists b0; split; auto.
+  eapply (A Mint32 (Vptr b0 i0)); eauto.
 Qed.
 
 Remark load_alloc_global:
@@ -1074,10 +1074,10 @@ Remark load_alloc_global:
 Proof.
   intros. destruct g as [f|v]; simpl in H.
   (* function *)
-  destruct (Mem.alloc m 0 1) as [m1 b'] eqn:?. 
+  destruct (Mem.alloc m 0 1) as [m1 b'] eqn:?.
   assert (b <> b'). apply Mem.valid_not_valid_diff with m; eauto with mem.
-  transitivity (Mem.load chunk m1 b p). 
-  eapply Mem.load_drop; eauto. 
+  transitivity (Mem.load chunk m1 b p).
+  eapply Mem.load_drop; eauto.
   eapply Mem.load_alloc_unchanged; eauto.
   (* variable *)
   set (init := gvar_init v) in *.
@@ -1086,10 +1086,10 @@ Proof.
   destruct (store_zeros m1 b' 0 sz) as [m2|] eqn:?; try discriminate.
   destruct (store_init_data_list m2 b' 0 init) as [m3|] eqn:?; try discriminate.
   assert (b <> b'). apply Mem.valid_not_valid_diff with m; eauto with mem.
-  transitivity (Mem.load chunk m3 b p). 
+  transitivity (Mem.load chunk m3 b p).
   eapply Mem.load_drop; eauto.
   transitivity (Mem.load chunk m2 b p).
-  eapply store_init_data_list_outside; eauto. 
+  eapply store_init_data_list_outside; eauto.
   transitivity (Mem.load chunk m1 b p).
   eapply store_zeros_load_outside; eauto.
   eapply Mem.load_alloc_unchanged; eauto.
@@ -1104,11 +1104,11 @@ Proof.
   induction gl; simpl; intros.
   congruence.
   destruct (alloc_global m a) as [m''|] eqn:?; try discriminate.
-  transitivity (Mem.load chunk m'' b p). 
-  apply IHgl; auto. unfold Mem.valid_block in *. 
-  erewrite alloc_global_nextblock; eauto. 
+  transitivity (Mem.load chunk m'' b p).
+  apply IHgl; auto. unfold Mem.valid_block in *.
+  erewrite alloc_global_nextblock; eauto.
   apply Plt_trans with (Mem.nextblock m); auto. apply Plt_succ.
-  destruct a as [id g]. eapply load_alloc_global; eauto. 
+  destruct a as [id g]. eapply load_alloc_global; eauto.
 Qed.
 
 Remark load_store_init_data_invariant:
@@ -1119,7 +1119,7 @@ Remark load_store_init_data_invariant:
 Proof.
   induction il; intro p; simpl.
   auto.
-  repeat rewrite H. destruct a; intuition. red; intros; rewrite H; auto. 
+  repeat rewrite H. destruct a; intuition. red; intros; rewrite H; auto.
 Qed.
 
 Definition variables_initialized (g: t) (m: mem) :=
@@ -1146,19 +1146,19 @@ Lemma alloc_global_initialized:
   /\ functions_initialized (add_global ge (id, g)) m'
   /\ genv_next (add_global ge (id, g)) = Mem.nextblock m'.
 Proof.
-  intros. 
+  intros.
   exploit alloc_global_nextblock; eauto. intros NB. split.
 (* variables-initialized *)
   destruct g as [f|v].
 (* function *)
-  red; intros. unfold find_var_info in H3. simpl in H3. 
+  red; intros. unfold find_var_info in H3. simpl in H3.
   exploit H1; eauto. intros [A [B C]].
-  assert (D: Mem.valid_block m b). 
+  assert (D: Mem.valid_block m b).
     red. exploit genv_vars_range; eauto. rewrite H; auto.
-  split. red; intros. erewrite <- alloc_global_perm; eauto. 
-  split. intros. eapply B. erewrite alloc_global_perm; eauto. 
-  intros. apply load_store_init_data_invariant with m; auto. 
-  intros. eapply load_alloc_global; eauto. 
+  split. red; intros. erewrite <- alloc_global_perm; eauto.
+  split. intros. eapply B. erewrite alloc_global_perm; eauto.
+  intros. apply load_store_init_data_invariant with m; auto.
+  intros. eapply load_alloc_global; eauto.
 (* variable *)
   red; intros. unfold find_var_info in H3. simpl in H3. rewrite PTree.gsspec in H3.
   destruct (peq b (genv_next ge0)).
@@ -1169,29 +1169,29 @@ Proof.
   destruct (Mem.alloc m 0 sz) as [m1 b'] eqn:?.
   destruct (store_zeros m1 b' 0 sz) as [m2|] eqn:?; try discriminate.
   destruct (store_init_data_list m2 b' 0 init) as [m3|] eqn:?; try discriminate.
-  exploit Mem.alloc_result; eauto. intro RES. 
+  exploit Mem.alloc_result; eauto. intro RES.
   replace (genv_next ge0) with b' by congruence.
   split. red; intros. eapply Mem.perm_drop_1; eauto.
   split. intros.
   assert (0 <= ofs < sz).
     eapply Mem.perm_alloc_3; eauto.
     erewrite store_zeros_perm; [idtac|eauto].
-    erewrite store_init_data_list_perm; [idtac|eauto]. 
+    erewrite store_init_data_list_perm; [idtac|eauto].
     eapply Mem.perm_drop_4; eauto.
   split. auto. eapply Mem.perm_drop_2; eauto.
-  intros. apply load_store_init_data_invariant with m3. 
-  intros. eapply Mem.load_drop; eauto. 
-  right; right; right. unfold perm_globvar. rewrite H3. 
+  intros. apply load_store_init_data_invariant with m3.
+  intros. eapply Mem.load_drop; eauto.
+  right; right; right. unfold perm_globvar. rewrite H3.
   destruct (gvar_readonly gv); auto with mem.
   eapply store_init_data_list_charact; eauto.
-  eapply store_zeros_read_as_zero; eauto. 
+  eapply store_zeros_read_as_zero; eauto.
   (* older var *)
   exploit H1; eauto. intros [A [B C]].
-  assert (D: Mem.valid_block m b). 
-    red. exploit genv_vars_range; eauto. rewrite H; auto. 
-  split. red; intros. erewrite <- alloc_global_perm; eauto. 
-  split. intros. eapply B. erewrite alloc_global_perm; eauto. 
-  intros. apply load_store_init_data_invariant with m; auto. 
+  assert (D: Mem.valid_block m b).
+    red. exploit genv_vars_range; eauto. rewrite H; auto.
+  split. red; intros. erewrite <- alloc_global_perm; eauto.
+  split. intros. eapply B. erewrite alloc_global_perm; eauto.
+  intros. apply load_store_init_data_invariant with m; auto.
   intros. eapply load_alloc_global; eauto.
 (* functions-initialized *)
   split. destruct g as [f|v].
@@ -1199,11 +1199,11 @@ Proof.
   red; intros. unfold find_funct_ptr in H3. simpl in H3. rewrite PTree.gsspec in H3.
   destruct (peq b (genv_next ge0)).
   (* same *)
-  inv H3. simpl in H0. 
-  destruct (Mem.alloc m 0 1) as [m1 b'] eqn:?. 
-  exploit Mem.alloc_result; eauto. intro RES. 
+  inv H3. simpl in H0.
+  destruct (Mem.alloc m 0 1) as [m1 b'] eqn:?.
+  exploit Mem.alloc_result; eauto. intro RES.
   replace (genv_next ge0) with b' by congruence.
-  split. eapply Mem.perm_drop_1; eauto. omega. 
+  split. eapply Mem.perm_drop_1; eauto. omega.
   intros.
   assert (0 <= ofs < 1).
     eapply Mem.perm_alloc_3; eauto.
@@ -1211,16 +1211,16 @@ Proof.
   split. omega. eapply Mem.perm_drop_2; eauto.
   (* older function *)
   exploit H2; eauto. intros [A B].
-  assert (D: Mem.valid_block m b). 
+  assert (D: Mem.valid_block m b).
     red. exploit genv_funs_range; eauto. rewrite H; auto.
-  split. erewrite <- alloc_global_perm; eauto. 
+  split. erewrite <- alloc_global_perm; eauto.
   intros. eapply B. erewrite alloc_global_perm; eauto.
 (* variables *)
-  red; intros. unfold find_funct_ptr in H3. simpl in H3. 
+  red; intros. unfold find_funct_ptr in H3. simpl in H3.
   exploit H2; eauto. intros [A B].
-  assert (D: Mem.valid_block m b). 
+  assert (D: Mem.valid_block m b).
     red. exploit genv_funs_range; eauto. rewrite H; auto.
-  split. erewrite <- alloc_global_perm; eauto. 
+  split. erewrite <- alloc_global_perm; eauto.
   intros. eapply B. erewrite alloc_global_perm; eauto.
 (* nextblock *)
   rewrite NB. simpl. rewrite H. auto.
@@ -1238,7 +1238,7 @@ Proof.
   inv H0; auto.
   destruct a as [id g]. destruct (alloc_global m (id, g)) as [m1|] eqn:?; try discriminate.
   exploit alloc_global_initialized; eauto. intros [P [Q R]].
-  eapply IHgl; eauto. 
+  eapply IHgl; eauto.
 Qed.
 
 End INITMEM.
@@ -1247,12 +1247,12 @@ Definition init_mem (p: program F V) :=
   alloc_globals (globalenv p) Mem.empty p.(prog_defs).
 
 Lemma init_mem_genv_next: forall p m,
-  init_mem p = Some m -> 
+  init_mem p = Some m ->
   genv_next (globalenv p) = Mem.nextblock m.
 Proof.
   unfold init_mem; intros.
   exploit alloc_globals_nextblock; eauto. rewrite Mem.nextblock_empty. intro.
-  generalize (genv_next_add_globals (prog_defs p) (empty_genv (prog_public p))). 
+  generalize (genv_next_add_globals (prog_defs p) (empty_genv (prog_public p))).
   fold (globalenv p). simpl genv_next. intros. congruence.
 Qed.
 
@@ -1261,7 +1261,7 @@ Theorem find_symbol_not_fresh:
   init_mem p = Some m ->
   find_symbol (globalenv p) id = Some b -> Mem.valid_block m b.
 Proof.
-  intros. red. erewrite <- init_mem_genv_next; eauto. 
+  intros. red. erewrite <- init_mem_genv_next; eauto.
   eapply genv_symb_range; eauto.
 Qed.
 
@@ -1270,7 +1270,7 @@ Theorem find_funct_ptr_not_fresh:
   init_mem p = Some m ->
   find_funct_ptr (globalenv p) b = Some f -> Mem.valid_block m b.
 Proof.
-  intros. red. erewrite <- init_mem_genv_next; eauto. 
+  intros. red. erewrite <- init_mem_genv_next; eauto.
   eapply genv_funs_range; eauto.
 Qed.
 
@@ -1279,7 +1279,7 @@ Theorem find_var_info_not_fresh:
   init_mem p = Some m ->
   find_var_info (globalenv p) b = Some gv -> Mem.valid_block m b.
 Proof.
-  intros. red. erewrite <- init_mem_genv_next; eauto. 
+  intros. red. erewrite <- init_mem_genv_next; eauto.
   eapply genv_vars_range; eauto.
 Qed.
 
@@ -1293,7 +1293,7 @@ Theorem init_mem_characterization:
   /\ (gv.(gvar_volatile) = false -> load_store_init_data (globalenv p) m b 0 gv.(gvar_init)).
 Proof.
   intros. eapply alloc_globals_initialized; eauto.
-  rewrite Mem.nextblock_empty. auto. 
+  rewrite Mem.nextblock_empty. auto.
   red; intros. unfold find_var_info in H1. simpl in H1. rewrite PTree.gempty in H1. congruence.
   red; intros. unfold find_funct_ptr in H1. simpl in H1. rewrite PTree.gempty in H1. congruence.
 Qed.
@@ -1328,7 +1328,7 @@ Lemma store_zeros_neutral:
 Proof.
   intros until n. functional induction (store_zeros m b p n); intros.
   inv H1; auto.
-  apply IHo; auto. eapply Mem.store_inject_neutral; eauto. constructor.  
+  apply IHo; auto. eapply Mem.store_inject_neutral; eauto. constructor.
   inv H1.
 Qed.
 
@@ -1343,9 +1343,9 @@ Proof.
   destruct id; simpl in H1; try (eapply Mem.store_inject_neutral; eauto; fail).
   congruence.
   destruct (find_symbol ge i) as [b'|] eqn:E; try discriminate.
-  eapply Mem.store_inject_neutral; eauto. 
-  econstructor. unfold Mem.flat_inj. apply pred_dec_true; auto. eauto.  
-  rewrite Int.add_zero. auto. 
+  eapply Mem.store_inject_neutral; eauto.
+  econstructor. unfold Mem.flat_inj. apply pred_dec_true; auto. eauto.
+  rewrite Int.add_zero. auto.
 Qed.
 
 Lemma store_init_data_list_neutral:
@@ -1358,7 +1358,7 @@ Proof.
   induction idl; simpl; intros.
   congruence.
   destruct (store_init_data ge m b p a) as [m1|] eqn:E; try discriminate.
-  eapply IHidl. eapply store_init_data_neutral; eauto. auto. eauto. 
+  eapply IHidl. eapply store_init_data_neutral; eauto. auto. eauto.
 Qed.
 
 Lemma alloc_global_neutral:
@@ -1372,7 +1372,7 @@ Proof.
   (* function *)
   destruct (Mem.alloc m 0 1) as [m1 b] eqn:?.
   assert (Plt b thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto.
-  eapply Mem.drop_inject_neutral; eauto. 
+  eapply Mem.drop_inject_neutral; eauto.
   eapply Mem.alloc_inject_neutral; eauto.
   (* variable *)
   set (init := gvar_init v) in *.
@@ -1381,9 +1381,9 @@ Proof.
   destruct (store_zeros m1 b 0 sz) as [m2|] eqn:?; try discriminate.
   destruct (store_init_data_list ge m2 b 0 init) as [m3|] eqn:?; try discriminate.
   assert (Plt b thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto.
-  eapply Mem.drop_inject_neutral; eauto. 
+  eapply Mem.drop_inject_neutral; eauto.
   eapply store_init_data_list_neutral with (m := m2) (b := b); eauto.
-  eapply store_zeros_neutral with (m := m1); eauto. 
+  eapply store_zeros_neutral with (m := m1); eauto.
   eapply Mem.alloc_inject_neutral; eauto.
 Qed.
 
@@ -1403,7 +1403,7 @@ Lemma alloc_globals_neutral:
 Proof.
   induction gl; intros.
   simpl in *. congruence.
-  exploit alloc_globals_nextblock; eauto. intros EQ. 
+  exploit alloc_globals_nextblock; eauto. intros EQ.
   simpl in *. destruct (alloc_global ge m a) as [m1|] eqn:E; try discriminate.
   exploit alloc_global_neutral; eauto.
   assert (Ple (Psucc (Mem.nextblock m)) (Mem.nextblock m')).
@@ -1419,14 +1419,14 @@ Theorem initmem_inject:
   Mem.inject (Mem.flat_inj (Mem.nextblock m)) m m.
 Proof.
   unfold init_mem; intros.
-  apply Mem.neutral_inject. 
-  eapply alloc_globals_neutral; eauto. 
+  apply Mem.neutral_inject.
+  eapply alloc_globals_neutral; eauto.
   intros. exploit find_symbol_not_fresh; eauto.
   apply Mem.empty_inject_neutral.
   apply Ple_refl.
 Qed.
 
-Section INITMEM_AUGMENT_INJ. 
+Section INITMEM_AUGMENT_INJ.
 
 Variable ge: t.
 Variable thr: block.
@@ -1440,58 +1440,58 @@ Lemma store_zeros_augment:
 Proof.
   intros until n. functional induction (store_zeros m2 b p n); intros.
   inv H1; auto.
-  apply IHo; auto. exploit Mem.store_outside_inject; eauto. simpl. 
-  intros. exfalso. unfold Mem.flat_inj in H2. destruct (plt b' thr). 
+  apply IHo; auto. exploit Mem.store_outside_inject; eauto. simpl.
+  intros. exfalso. unfold Mem.flat_inj in H2. destruct (plt b' thr).
   inv H2. unfold Plt, Ple in *. zify; omega.
   discriminate.
   discriminate.
 Qed.
 
-Lemma store_init_data_augment: 
-  forall m1 m2 b p id m2', 
-  Mem.inject (Mem.flat_inj thr) m1 m2 -> 
-  Ple thr b -> 
+Lemma store_init_data_augment:
+  forall m1 m2 b p id m2',
+  Mem.inject (Mem.flat_inj thr) m1 m2 ->
+  Ple thr b ->
   store_init_data ge m2 b p id = Some m2' ->
   Mem.inject (Mem.flat_inj thr) m1 m2'.
-Proof. 
-  intros until m2'. intros INJ BND ST. 
-  assert (P: forall chunk ofs v m2', 
-             Mem.store chunk m2 b ofs v = Some m2' -> 
-             Mem.inject (Mem.flat_inj thr) m1 m2'). 
-    intros. eapply Mem.store_outside_inject; eauto. 
+Proof.
+  intros until m2'. intros INJ BND ST.
+  assert (P: forall chunk ofs v m2',
+             Mem.store chunk m2 b ofs v = Some m2' ->
+             Mem.inject (Mem.flat_inj thr) m1 m2').
+    intros. eapply Mem.store_outside_inject; eauto.
     intros. unfold Mem.flat_inj in H0.
     destruct (plt b' thr); inv H0. unfold Plt, Ple in *. zify; omega.
   destruct id; simpl in ST; try (eapply P; eauto; fail).
   congruence.
-  revert ST.  caseEq (find_symbol ge i); try congruence. intros; eapply P; eauto. 
+  revert ST.  caseEq (find_symbol ge i); try congruence. intros; eapply P; eauto.
 Qed.
 
 Lemma store_init_data_list_augment:
-  forall b idl m1 m2 p m2', 
-  Mem.inject (Mem.flat_inj thr) m1 m2 -> 
-  Ple thr b -> 
+  forall b idl m1 m2 p m2',
+  Mem.inject (Mem.flat_inj thr) m1 m2 ->
+  Ple thr b ->
   store_init_data_list ge m2 b p idl = Some m2' ->
   Mem.inject (Mem.flat_inj thr) m1 m2'.
-Proof. 
+Proof.
   induction idl; simpl.
   intros; congruence.
   intros until m2'; intros INJ FB.
-  caseEq (store_init_data ge m2 b p a); try congruence. intros. 
-  eapply IHidl. eapply store_init_data_augment; eauto. auto. eauto. 
+  caseEq (store_init_data ge m2 b p a); try congruence. intros.
+  eapply IHidl. eapply store_init_data_augment; eauto. auto. eauto.
 Qed.
 
 Lemma alloc_global_augment:
   forall idg m1 m2 m2',
   alloc_global ge m2 idg = Some m2' ->
-  Mem.inject (Mem.flat_inj thr) m1 m2 -> 
-  Ple thr (Mem.nextblock m2) -> 
+  Mem.inject (Mem.flat_inj thr) m1 m2 ->
+  Ple thr (Mem.nextblock m2) ->
   Mem.inject (Mem.flat_inj thr) m1 m2'.
 Proof.
   intros. destruct idg as [id [f|v]]; simpl in H.
   (* function *)
   destruct (Mem.alloc m2 0 1) as [m3 b] eqn:?.
   assert (Ple thr b). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto.
-  eapply Mem.drop_outside_inject. 2: eauto. 
+  eapply Mem.drop_outside_inject. 2: eauto.
   eapply Mem.alloc_right_inject; eauto.
   intros. unfold Mem.flat_inj in H3. destruct (plt b' thr); inv H3.
   unfold Plt, Ple in *. zify; omega.
@@ -1502,7 +1502,7 @@ Proof.
   destruct (store_zeros m3 b 0 sz) as [m4|] eqn:?; try discriminate.
   destruct (store_init_data_list ge m4 b 0 init) as [m5|] eqn:?; try discriminate.
   assert (Ple thr b). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto.
-  eapply Mem.drop_outside_inject. 2: eauto. 
+  eapply Mem.drop_outside_inject. 2: eauto.
   eapply store_init_data_list_augment. 3: eauto. 2: eauto.
   eapply store_zeros_augment. 3: eauto. 2: eauto.
   eapply Mem.alloc_right_inject; eauto.
@@ -1520,13 +1520,13 @@ Proof.
   induction gl; simpl.
   intros. congruence.
   intros until m2'. caseEq (alloc_global ge m2 a); try congruence. intros.
-  eapply IHgl with (m2 := m); eauto.  
-    eapply alloc_global_augment; eauto. 
-    rewrite (alloc_global_nextblock _ _ _ H). 
+  eapply IHgl with (m2 := m); eauto.
+    eapply alloc_global_augment; eauto.
+    rewrite (alloc_global_nextblock _ _ _ H).
     apply Ple_trans with (Mem.nextblock m2); auto. apply Ple_succ.
 Qed.
 
-End INITMEM_AUGMENT_INJ. 
+End INITMEM_AUGMENT_INJ.
 
 End GENV.
 
@@ -1545,7 +1545,7 @@ Inductive match_globvar: globvar V -> globvar W -> Prop :=
       match_varinfo info1 info2 ->
       match_globvar (mkglobvar info1 init ro vo) (mkglobvar info2 init ro vo).
 
-Record match_genvs (new_globs : list (ident * globdef B W)) 
+Record match_genvs (new_globs : list (ident * globdef B W))
                    (ge1: t A V) (ge2: t B W): Prop := {
   mge_next:
     genv_next ge2 = advance_next new_globs (genv_next ge1);
@@ -1557,9 +1557,9 @@ Record match_genvs (new_globs : list (ident * globdef B W))
     exists tf, PTree.get b (genv_funs ge2) = Some tf /\ match_fun f tf;
   mge_rev_funs:
     forall b tf, PTree.get b (genv_funs ge2) = Some tf ->
-    if plt b (genv_next ge1) then 
+    if plt b (genv_next ge1) then
       exists f, PTree.get b (genv_funs ge1) = Some f /\ match_fun f tf
-    else 
+    else
       In (Gfun tf) (map snd new_globs);
   mge_vars:
     forall b v, PTree.get b (genv_vars ge1) = Some v ->
@@ -1583,43 +1583,43 @@ Proof.
 (* two functions *)
   constructor; simpl.
   congruence.
-  intros. rewrite mge_next0. 
+  intros. rewrite mge_next0.
     repeat rewrite PTree.gsspec. destruct (peq id0 id); auto.
-  rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec. 
-    destruct (peq b (genv_next ge1)). 
+  rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec.
+    destruct (peq b (genv_next ge1)).
      exists f2; split; congruence.
      eauto.
-  rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec. 
-   destruct (peq b (genv_next ge1)). 
+  rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec.
+   destruct (peq b (genv_next ge1)).
     subst b. rewrite pred_dec_true. exists f1; split; congruence. apply Plt_succ.
-    pose proof (mge_rev_funs0 b tf H0). 
+    pose proof (mge_rev_funs0 b tf H0).
     destruct (plt b (genv_next ge1)). rewrite pred_dec_true. auto. apply Plt_trans_succ; auto.
     contradiction.
   eauto.
   intros.
-    pose proof (mge_rev_vars0 b tv H0). 
+    pose proof (mge_rev_vars0 b tv H0).
     destruct (plt b (genv_next ge1)). rewrite pred_dec_true. auto.
     apply Plt_trans with (genv_next ge1); auto. apply Plt_succ.
     contradiction.
 (* two variables *)
   constructor; simpl.
   congruence.
-  intros. rewrite mge_next0. 
+  intros. rewrite mge_next0.
     repeat rewrite PTree.gsspec. destruct (peq id0 id); auto.
   eauto.
   intros.
-    pose proof (mge_rev_funs0 b tf H0). 
+    pose proof (mge_rev_funs0 b tf H0).
     destruct (plt b (genv_next ge1)). rewrite pred_dec_true. auto. apply Plt_trans_succ; auto.
     contradiction.
-  rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec. 
+  rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec.
     destruct (peq b (genv_next ge1)).
-    econstructor; split. eauto. inv H0. constructor; auto. 
+    econstructor; split. eauto. inv H0. constructor; auto.
     eauto.
-  rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec. 
-   destruct (peq b (genv_next ge1)). 
+  rewrite mge_next0. intros. rewrite PTree.gsspec in H0. rewrite PTree.gsspec.
+   destruct (peq b (genv_next ge1)).
     subst b. rewrite pred_dec_true.
     econstructor; split. eauto. inv H0. constructor; auto. apply Plt_succ.
-    pose proof (mge_rev_vars0 b tv H0). 
+    pose proof (mge_rev_vars0 b tv H0).
     destruct (plt b (genv_next ge1)). rewrite pred_dec_true. auto. apply Plt_trans_succ; auto.
     contradiction.
 Qed.
@@ -1629,56 +1629,56 @@ Lemma add_globals_match:
   forall ge1 ge2, match_genvs nil ge1 ge2 ->
   match_genvs nil (add_globals ge1 gl1) (add_globals ge2 gl2).
 Proof.
-  induction 1; intros; simpl. 
+  induction 1; intros; simpl.
   auto.
   apply IHlist_forall2. apply add_global_match; auto.
 Qed.
 
-Lemma add_global_augment_match: 
+Lemma add_global_augment_match:
   forall new_globs ge1 ge2 idg,
   match_genvs new_globs ge1 ge2 ->
   match_genvs (new_globs ++ (idg :: nil)) ge1 (add_global ge2 idg).
 Proof.
-  intros. destruct H. 
+  intros. destruct H.
   assert (LE: Ple (genv_next ge1) (genv_next ge2)).
   { rewrite mge_next0; apply advance_next_le. }
   constructor; simpl.
   rewrite mge_next0. unfold advance_next. rewrite fold_left_app. simpl. auto.
-  intros. rewrite map_app in H. rewrite in_app in H. simpl in H. 
-    destruct (peq id idg#1). subst. intuition. rewrite PTree.gso. 
-    apply mge_symb0. intuition. auto. 
+  intros. rewrite map_app in H. rewrite in_app in H. simpl in H.
+    destruct (peq id idg#1). subst. intuition. rewrite PTree.gso.
+    apply mge_symb0. intuition. auto.
   intros. destruct idg as [id1 [f1|v1]]; simpl; eauto.
     rewrite PTree.gso. eauto.
     exploit genv_funs_range; eauto. intros.
     unfold Plt, Ple in *; zify; omega.
   intros. rewrite map_app. destruct idg as [id1 [f1|v1]]; simpl in H.
-    rewrite PTree.gsspec in H. destruct (peq b (genv_next ge2)). 
+    rewrite PTree.gsspec in H. destruct (peq b (genv_next ge2)).
     rewrite pred_dec_false. rewrite in_app. simpl; right; left. congruence.
     subst b. unfold Plt, Ple in *; zify; omega.
-    exploit mge_rev_funs0; eauto. destruct (plt b (genv_next ge1)); auto. 
+    exploit mge_rev_funs0; eauto. destruct (plt b (genv_next ge1)); auto.
     rewrite in_app. tauto.
-    exploit mge_rev_funs0; eauto. destruct (plt b (genv_next ge1)); auto. 
+    exploit mge_rev_funs0; eauto. destruct (plt b (genv_next ge1)); auto.
     rewrite in_app. tauto.
   intros. destruct idg as [id1 [f1|v1]]; simpl; eauto.
-    rewrite PTree.gso. eauto. exploit genv_vars_range; eauto. 
+    rewrite PTree.gso. eauto. exploit genv_vars_range; eauto.
     unfold Plt, Ple in *; zify; omega.
   intros. rewrite map_app. destruct idg as [id1 [f1|v1]]; simpl in H.
-    exploit mge_rev_vars0; eauto. destruct (plt b (genv_next ge1)); auto. 
+    exploit mge_rev_vars0; eauto. destruct (plt b (genv_next ge1)); auto.
     rewrite in_app. tauto.
-    rewrite PTree.gsspec in H. destruct (peq b (genv_next ge2)). 
+    rewrite PTree.gsspec in H. destruct (peq b (genv_next ge2)).
     rewrite pred_dec_false. rewrite in_app. simpl; right; left. congruence.
     subst b. unfold Plt, Ple in *; zify; omega.
-    exploit mge_rev_vars0; eauto. destruct (plt b (genv_next ge1)); auto. 
+    exploit mge_rev_vars0; eauto. destruct (plt b (genv_next ge1)); auto.
     rewrite in_app. tauto.
 Qed.
 
-Lemma add_globals_augment_match: 
+Lemma add_globals_augment_match:
   forall gl new_globs ge1 ge2,
   match_genvs new_globs ge1 ge2 ->
   match_genvs (new_globs ++ gl) ge1 (add_globals ge2 gl).
 Proof.
-  induction gl; simpl. 
-    intros. rewrite app_nil_r. auto. 
+  induction gl; simpl.
+    intros. rewrite app_nil_r. auto.
     intros. change (a :: gl) with ((a :: nil) ++ gl). rewrite <- app_ass.
       apply IHgl. apply add_global_augment_match. auto.
 Qed.
@@ -1688,15 +1688,15 @@ Variable new_main : ident.
 
 Variable p: program A V.
 Variable p': program B W.
-Hypothesis progmatch: 
+Hypothesis progmatch:
   match_program match_fun match_varinfo new_globs new_main p p'.
 
 Lemma globalenvs_match:
   match_genvs new_globs (globalenv p) (globalenv p').
 Proof.
   unfold globalenv. destruct progmatch as [[tglob [P Q]] R].
-  rewrite Q. rewrite add_globals_app. 
-  change new_globs with (nil ++ new_globs) at 1. 
+  rewrite Q. rewrite add_globals_app.
+  change new_globs with (nil ++ new_globs) at 1.
   apply add_globals_augment_match.
   apply add_globals_match; auto.
   constructor; simpl; auto; intros; rewrite PTree.gempty in H; congruence.
@@ -1712,9 +1712,9 @@ Proof (mge_funs globalenvs_match).
 Theorem find_funct_ptr_rev_match:
   forall (b : block) (tf : B),
   find_funct_ptr (globalenv p') b = Some tf ->
-  if plt b (genv_next (globalenv p)) then 
+  if plt b (genv_next (globalenv p)) then
       exists f, find_funct_ptr (globalenv p) b = Some f /\ match_fun f tf
-  else 
+  else
       In (Gfun tf) (map snd new_globs).
 Proof (mge_rev_funs globalenvs_match).
 
@@ -1723,8 +1723,8 @@ Theorem find_funct_match:
   find_funct (globalenv p) v = Some f ->
   exists tf : B, find_funct (globalenv p') v = Some tf /\ match_fun f tf.
 Proof.
-  intros. exploit find_funct_inv; eauto. intros [b EQ]. subst v. 
-  rewrite find_funct_find_funct_ptr in H. 
+  intros. exploit find_funct_inv; eauto. intros [b EQ]. subst v.
+  rewrite find_funct_find_funct_ptr in H.
   rewrite find_funct_find_funct_ptr.
   apply find_funct_ptr_match. auto.
 Qed.
@@ -1732,13 +1732,13 @@ Qed.
 Theorem find_funct_rev_match:
   forall (v : val) (tf : B),
   find_funct (globalenv p') v = Some tf ->
-  (exists f, find_funct (globalenv p) v = Some f /\ match_fun f tf) 
+  (exists f, find_funct (globalenv p) v = Some f /\ match_fun f tf)
   \/ (In (Gfun tf) (map snd new_globs)).
 Proof.
-  intros. exploit find_funct_inv; eauto. intros [b EQ]. subst v. 
-  rewrite find_funct_find_funct_ptr in H. 
+  intros. exploit find_funct_inv; eauto. intros [b EQ]. subst v.
+  rewrite find_funct_find_funct_ptr in H.
   rewrite find_funct_find_funct_ptr.
-  apply find_funct_ptr_rev_match in H. 
+  apply find_funct_ptr_rev_match in H.
    destruct (plt b (genv_next (globalenv p))); auto.
 Qed.
 
@@ -1752,7 +1752,7 @@ Proof (mge_vars globalenvs_match).
 Theorem find_var_info_rev_match:
   forall (b : block) (tv : globvar W),
   find_var_info (globalenv p') b = Some tv ->
-  if plt b (genv_next (globalenv p)) then 
+  if plt b (genv_next (globalenv p)) then
     exists v, find_var_info (globalenv p) b = Some v /\ match_globvar v tv
   else
     In (Gvar tv) (map snd new_globs).
@@ -1763,7 +1763,7 @@ Theorem find_symbol_match:
   ~In s (map fst new_globs) ->
   find_symbol (globalenv p') s = find_symbol (globalenv p) s.
 Proof.
-  intros. destruct globalenvs_match. unfold find_symbol.  auto. 
+  intros. destruct globalenvs_match. unfold find_symbol.  auto.
 Qed.
 
 Theorem public_symbol_match:
@@ -1771,11 +1771,11 @@ Theorem public_symbol_match:
   ~In s (map fst new_globs) ->
   public_symbol (globalenv p') s = public_symbol (globalenv p) s.
 Proof.
-  intros. unfold public_symbol. rewrite find_symbol_match by auto. 
+  intros. unfold public_symbol. rewrite find_symbol_match by auto.
   destruct (find_symbol (globalenv p) s); auto.
-  rewrite ! globalenv_public. 
-  destruct progmatch as (P & Q & R). rewrite R. auto. 
-Qed. 
+  rewrite ! globalenv_public.
+  destruct progmatch as (P & Q & R). rewrite R. auto.
+Qed.
 
 Hypothesis new_ids_fresh:
   forall s, In s (prog_defs_names p) -> In s (map fst new_globs) -> False.
@@ -1787,47 +1787,47 @@ Lemma store_init_data_list_match:
   store_init_data_list (globalenv p) m b ofs idl = Some m' ->
   store_init_data_list (globalenv p') m b ofs idl = Some m'.
 Proof.
-  induction idl; simpl; intros. 
+  induction idl; simpl; intros.
   auto.
   assert (forall m', store_init_data (globalenv p) m b ofs a = Some m' ->
           store_init_data (globalenv p') m b ofs a = Some m').
    destruct a; simpl; auto. rewrite find_symbol_match. auto.
    simpl in H. destruct (find_symbol (globalenv p) i) as [b'|] eqn:?; try discriminate.
-   red; intros. exploit find_symbol_inversion; eauto. 
-  case_eq (store_init_data (globalenv p) m b ofs a); intros. 
-    rewrite H1 in H. 
-    pose proof (H0 _ H1). rewrite H2. auto. 
-    rewrite H1 in H. inversion H. 
+   red; intros. exploit find_symbol_inversion; eauto.
+  case_eq (store_init_data (globalenv p) m b ofs a); intros.
+    rewrite H1 in H.
+    pose proof (H0 _ H1). rewrite H2. auto.
+    rewrite H1 in H. inversion H.
 Qed.
 
 Lemma alloc_globals_match:
   forall gl1 gl2, list_forall2 (match_globdef match_fun match_varinfo) gl1 gl2 ->
   forall m m',
-  alloc_globals (globalenv p) m gl1 = Some m' -> 
+  alloc_globals (globalenv p) m gl1 = Some m' ->
   alloc_globals (globalenv p') m gl2 = Some m'.
 Proof.
   induction 1; simpl; intros.
   auto.
   destruct (alloc_global (globalenv p) m a1) as [m1|] eqn:?; try discriminate.
   assert (alloc_global (globalenv p') m b1 = Some m1).
-    inv H; simpl in *. 
+    inv H; simpl in *.
     auto.
     set (sz := init_data_list_size init) in *.
     destruct (Mem.alloc m 0 sz) as [m2 b] eqn:?.
     destruct (store_zeros m2 b 0 sz) as [m3|] eqn:?; try discriminate.
     destruct (store_init_data_list (globalenv p) m3 b 0 init) as [m4|] eqn:?; try discriminate.
-    erewrite store_init_data_list_match; eauto. 
+    erewrite store_init_data_list_match; eauto.
   rewrite H2. eauto.
 Qed.
 
 Theorem init_mem_match:
-  forall m, init_mem p = Some m -> 
+  forall m, init_mem p = Some m ->
   init_mem p' = alloc_globals (globalenv p') m new_globs.
 Proof.
   unfold init_mem; intros.
   destruct progmatch as [[tglob [P Q]] R].
-  rewrite Q. erewrite <- alloc_globals_app; eauto. 
-  eapply alloc_globals_match; eauto. 
+  rewrite Q. erewrite <- alloc_globals_app; eauto.
+  eapply alloc_globals_match; eauto.
 Qed.
 
 Theorem find_new_funct_ptr_match:
@@ -1838,9 +1838,9 @@ Theorem find_new_funct_ptr_match:
 Proof.
   intros.
   destruct progmatch as [[tglob [P Q]] R].
-  exploit in_norepet_unique; eauto. intros (gl1 & gl2 & S & T). 
-  rewrite S in Q. rewrite <- app_ass in Q. 
-  eapply find_funct_ptr_exists_2; eauto. 
+  exploit in_norepet_unique; eauto. intros (gl1 & gl2 & S & T).
+  rewrite S in Q. rewrite <- app_ass in Q.
+  eapply find_funct_ptr_exists_2; eauto.
 Qed.
 
 Theorem find_new_var_match:
@@ -1851,9 +1851,9 @@ Theorem find_new_var_match:
 Proof.
   intros.
   destruct progmatch as [[tglob [P Q]] R].
-  exploit in_norepet_unique; eauto. intros (gl1 & gl2 & S & T). 
-  rewrite S in Q. rewrite <- app_ass in Q. 
-  eapply find_var_exists_2; eauto. 
+  exploit in_norepet_unique; eauto. intros (gl1 & gl2 & S & T).
+  rewrite S in Q. rewrite <- app_ass in Q.
+  eapply find_var_exists_2; eauto.
 Qed.
 
 End MATCH_PROGRAMS.
@@ -1889,8 +1889,8 @@ Theorem find_funct_ptr_transf_augment:
   exists f',
   find_funct_ptr (globalenv p') b = Some f' /\ transf_fun f = OK f'.
 Proof.
-  intros. 
-  exploit find_funct_ptr_match. eexact prog_match. eauto. 
+  intros.
+  exploit find_funct_ptr_match. eexact prog_match. eauto.
   intros [tf [X Y]]. exists tf; auto.
 Qed.
 
@@ -1899,10 +1899,10 @@ Theorem find_funct_ptr_rev_transf_augment:
   find_funct_ptr (globalenv p') b = Some tf ->
   if plt b (genv_next (globalenv p)) then
    (exists f, find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf)
-  else 
+  else
    In (Gfun tf) (map snd new_globs).
 Proof.
-  intros. 
+  intros.
   exploit find_funct_ptr_rev_match; eauto.
 Qed.
 
@@ -1912,18 +1912,18 @@ Theorem find_funct_transf_augment:
   exists f',
   find_funct (globalenv p') v = Some f' /\ transf_fun f = OK f'.
 Proof.
-  intros. 
-  exploit find_funct_match. eexact prog_match. eauto. auto. 
+  intros.
+  exploit find_funct_match. eexact prog_match. eauto. auto.
 Qed.
 
-Theorem find_funct_rev_transf_augment: 
+Theorem find_funct_rev_transf_augment:
   forall (v: val) (tf: B),
   find_funct (globalenv p') v = Some tf ->
   (exists f, find_funct (globalenv p) v = Some f /\ transf_fun f = OK tf) \/
   In (Gfun tf) (map snd new_globs).
 Proof.
-  intros. 
-  exploit find_funct_rev_match. eexact prog_match. eauto. auto. 
+  intros.
+  exploit find_funct_rev_match. eexact prog_match. eauto. auto.
 Qed.
 
 Theorem find_var_info_transf_augment:
@@ -1932,8 +1932,8 @@ Theorem find_var_info_transf_augment:
   exists v',
   find_var_info (globalenv p') b = Some v' /\ transf_globvar transf_var v = OK v'.
 Proof.
-  intros. 
-  exploit find_var_info_match. eexact prog_match. eauto. intros [tv [X Y]]. 
+  intros.
+  exploit find_var_info_match. eexact prog_match. eauto. intros [tv [X Y]].
   exists tv; split; auto. inv Y. unfold transf_globvar; simpl.
   rewrite H0; simpl. auto.
 Qed.
@@ -1946,23 +1946,23 @@ Theorem find_var_info_rev_transf_augment:
   else
     (In (Gvar v') (map snd new_globs)).
 Proof.
-  intros. 
+  intros.
   exploit find_var_info_rev_match. eexact prog_match. eauto.
   destruct (plt b (genv_next (globalenv p))); auto.
-  intros [v [X Y]]. exists v; split; auto. inv Y. unfold transf_globvar; simpl. 
+  intros [v [X Y]]. exists v; split; auto. inv Y. unfold transf_globvar; simpl.
   rewrite H0; simpl. auto.
 Qed.
 
-Theorem find_symbol_transf_augment:  
-  forall (s: ident), 
+Theorem find_symbol_transf_augment:
+  forall (s: ident),
   ~ In s (map fst new_globs) ->
   find_symbol (globalenv p') s = find_symbol (globalenv p) s.
 Proof.
   intros. eapply find_symbol_match. eexact prog_match. auto.
 Qed.
 
-Theorem public_symbol_transf_augment:  
-  forall (s: ident), 
+Theorem public_symbol_transf_augment:
+  forall (s: ident),
   ~ In s (map fst new_globs) ->
   public_symbol (globalenv p') s = public_symbol (globalenv p) s.
 Proof.
@@ -1974,38 +1974,38 @@ Hypothesis new_ids_fresh:
 Hypothesis new_ids_unique:
   list_norepet (map fst new_globs).
 
-Theorem init_mem_transf_augment: 
-   forall m, init_mem p = Some m -> 
+Theorem init_mem_transf_augment:
+   forall m, init_mem p = Some m ->
    init_mem p' = alloc_globals (globalenv p') m new_globs.
 Proof.
   intros. eapply init_mem_match. eexact prog_match. auto. auto.
 Qed.
- 
+
 Theorem init_mem_inject_transf_augment:
   forall m, init_mem p = Some m ->
-  forall m', init_mem p' = Some m' -> 
+  forall m', init_mem p' = Some m' ->
   Mem.inject (Mem.flat_inj (Mem.nextblock m)) m m'.
 Proof.
-  intros. 
-  pose proof (initmem_inject p H). 
-  erewrite init_mem_transf_augment in H0; eauto. 
-  eapply alloc_globals_augment; eauto. apply Ple_refl. 
+  intros.
+  pose proof (initmem_inject p H).
+  erewrite init_mem_transf_augment in H0; eauto.
+  eapply alloc_globals_augment; eauto. apply Ple_refl.
 Qed.
 
-Theorem find_new_funct_ptr_exists: 
-  forall id f, In (id, Gfun f) new_globs -> 
+Theorem find_new_funct_ptr_exists:
+  forall id f, In (id, Gfun f) new_globs ->
   exists b, find_symbol (globalenv p') id = Some b
          /\ find_funct_ptr (globalenv p') b = Some f.
 Proof.
-  intros. eapply find_new_funct_ptr_match; eauto. 
+  intros. eapply find_new_funct_ptr_match; eauto.
 Qed.
 
 Theorem find_new_var_exists:
-  forall id gv, In (id, Gvar gv) new_globs -> 
+  forall id gv, In (id, Gvar gv) new_globs ->
   exists b, find_symbol (globalenv p') id = Some b
          /\ find_var_info (globalenv p') b = Some gv.
 Proof.
-  intros. eapply find_new_var_match; eauto. 
+  intros. eapply find_new_var_match; eauto.
 Qed.
 
 End TRANSF_PROGRAM_AUGMENT.
@@ -2041,7 +2041,7 @@ Theorem find_funct_ptr_rev_transf_partial2:
   exists f, find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf.
 Proof.
   pose proof (@find_funct_ptr_rev_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
-  intros.  pose proof (H b tf H0). 
+  intros.  pose proof (H b tf H0).
   destruct (plt b (genv_next (globalenv p))).  auto. contradiction.
 Qed.
 
@@ -2060,7 +2060,7 @@ Theorem find_funct_rev_transf_partial2:
   exists f, find_funct (globalenv p) v = Some f /\ transf_fun f = OK tf.
 Proof.
   pose proof (@find_funct_rev_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
-  intros. pose proof (H v tf H0). 
+  intros. pose proof (H v tf H0).
   destruct H1. auto. contradiction.
 Qed.
 
@@ -2080,7 +2080,7 @@ Theorem find_var_info_rev_transf_partial2:
   find_var_info (globalenv p) b = Some v /\ transf_globvar transf_var v = OK v'.
 Proof.
   pose proof (@find_var_info_rev_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
-  intros.  pose proof (H b v' H0). 
+  intros.  pose proof (H b v' H0).
   destruct (plt b (genv_next (globalenv p))).  auto. contradiction.
 Qed.
 
@@ -2104,10 +2104,10 @@ Theorem block_is_volatile_transf_partial2:
   forall (b: block),
   block_is_volatile (globalenv p') b = block_is_volatile (globalenv p) b.
 Proof.
-  unfold block_is_volatile; intros. 
+  unfold block_is_volatile; intros.
   destruct (find_var_info (globalenv p) b) as [v|] eqn:FV.
   exploit find_var_info_transf_partial2; eauto. intros (v' & P & Q).
-  rewrite P. monadInv Q. auto. 
+  rewrite P. monadInv Q. auto.
   destruct (find_var_info (globalenv p') b) as [v'|] eqn:FV'.
   exploit find_var_info_rev_transf_partial2; eauto. intros (v & P & Q). congruence.
   auto.
@@ -2117,7 +2117,7 @@ Theorem init_mem_transf_partial2:
   forall m, init_mem p = Some m -> init_mem p' = Some m.
 Proof.
   pose proof (@init_mem_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK).
-  intros. simpl in H. apply H; auto.  
+  intros. simpl in H. apply H; auto.
 Qed.
 
 End TRANSF_PROGRAM_PARTIAL2.
@@ -2183,11 +2183,11 @@ Theorem find_var_info_transf_partial:
   find_var_info (globalenv p') b = find_var_info (globalenv p) b.
 Proof.
   intros. case_eq (find_var_info (globalenv p) b); intros.
-  exploit find_var_info_transf_partial2. eexact transf_OK. eauto. 
-  intros [v' [P Q]]. monadInv Q. rewrite P. inv EQ. destruct g; auto. 
+  exploit find_var_info_transf_partial2. eexact transf_OK. eauto.
+  intros [v' [P Q]]. monadInv Q. rewrite P. inv EQ. destruct g; auto.
   case_eq (find_var_info (globalenv p') b); intros.
   exploit find_var_info_rev_transf_partial2. eexact transf_OK. eauto.
-  intros [v' [P Q]]. monadInv Q. inv EQ. congruence. 
+  intros [v' [P Q]]. monadInv Q. inv EQ. congruence.
   auto.
 Qed.
 
@@ -2216,7 +2216,7 @@ Let tp := transform_program transf p.
 Remark transf_OK:
   transform_partial_program (fun x => OK (transf x)) p = OK tp.
 Proof.
-  unfold tp. apply transform_program_partial_program. 
+  unfold tp. apply transform_program_partial_program.
 Qed.
 
 Theorem find_funct_ptr_transf:
@@ -2224,7 +2224,7 @@ Theorem find_funct_ptr_transf:
   find_funct_ptr (globalenv p) b = Some f ->
   find_funct_ptr (globalenv tp) b = Some (transf f).
 Proof.
-  intros. 
+  intros.
   destruct (@find_funct_ptr_transf_partial _ _ _ _ _ _ transf_OK _ _ H)
   as [f' [X Y]]. congruence.
 Qed.
@@ -2243,7 +2243,7 @@ Theorem find_funct_transf:
   find_funct (globalenv p) v = Some f ->
   find_funct (globalenv tp) v = Some (transf f).
 Proof.
-  intros. 
+  intros.
   destruct (@find_funct_transf_partial _ _ _ _ _ _ transf_OK _ _ H)
   as [f' [X Y]]. congruence.
 Qed.