diff --git a/aarch64/Op.v b/aarch64/Op.v
index f8d2510e7..4963baf14 100644
--- a/aarch64/Op.v
+++ b/aarch64/Op.v
@@ -1691,20 +1691,12 @@ Section EVAL_INJECT.
 Variable F V: Type.
 Variable genv: Genv.t F V.
 Variable f: meminj.
-Hypothesis globals: meminj_preserves_globals genv f.
+Hypothesis globals: Genv.inject f genv.
 Variable sp1: block.
 Variable sp2: block.
 Variable delta: Z.
 Hypothesis sp_inj: f sp1 = Some(sp2, delta).
 
-Remark symbol_address_inject:
-  forall id ofs, Val.inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs).
-Proof.
-  intros. unfold Genv.symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto.
-  exploit (proj1 globals); eauto. intros.
-  econstructor; eauto. rewrite Ptrofs.add_zero; auto.
-Qed.
-
 Lemma eval_condition_inject:
   forall cond vl1 vl2 b m1 m2,
   Val.inject_list f vl1 vl2 ->
@@ -1729,8 +1721,7 @@ Lemma eval_addressing_inject:
 Proof.
   intros.
   rewrite eval_shift_stack_addressing.
-  eapply eval_addressing_inj with (sp1 := Vptr sp1 Ptrofs.zero); eauto.
-  intros. apply symbol_address_inject.
+  eapply eval_addressing_inj with (sp1 := Vptr sp1 Ptrofs.zero); eauto using Genv.symbol_address_inject.
   econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. 
 Qed.
 
@@ -1750,7 +1741,7 @@ Proof.
   intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
   intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
   intros; eapply Mem.different_pointers_inject; eauto.
-  intros. apply symbol_address_inject.
+  intros. eapply Genv.symbol_address_inject; eauto.
   econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. 
 Qed.
 
diff --git a/arm/Op.v b/arm/Op.v
index 375a626dc..0777620a9 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -1085,20 +1085,12 @@ Section EVAL_INJECT.
 Variable F V: Type.
 Variable genv: Genv.t F V.
 Variable f: meminj.
-Hypothesis globals: meminj_preserves_globals genv f.
+Hypothesis globals: Genv.inject f genv.
 Variable sp1: block.
 Variable sp2: block.
 Variable delta: Z.
 Hypothesis sp_inj: f sp1 = Some(sp2, delta).
 
-Remark symbol_address_inject:
-  forall id ofs, Val.inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs).
-Proof.
-  intros. unfold Genv.symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto.
-  exploit (proj1 globals); eauto. intros.
-  econstructor; eauto. rewrite Ptrofs.add_zero; auto.
-Qed.
-
 Lemma eval_condition_inject:
   forall cond vl1 vl2 b m1 m2,
   Val.inject_list f vl1 vl2 ->
@@ -1123,8 +1115,7 @@ Lemma eval_addressing_inject:
 Proof.
   intros.
   rewrite eval_shift_stack_addressing.
-  eapply eval_addressing_inj with (sp1 := Vptr sp1 Ptrofs.zero); eauto.
-  intros. apply symbol_address_inject.
+  eapply eval_addressing_inj with (sp1 := Vptr sp1 Ptrofs.zero); eauto using Genv.symbol_address_inject.
   econstructor; eauto. rewrite Ptrofs.add_zero_l; auto.
 Qed.
 
@@ -1144,7 +1135,7 @@ Proof.
   intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
   intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
   intros; eapply Mem.different_pointers_inject; eauto.
-  intros; apply symbol_address_inject.
+  intros; eapply Genv.symbol_address_inject; eauto.
   econstructor; eauto. rewrite Ptrofs.add_zero_l; auto.
 Qed.
 
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index c28b57e45..a894c6f2f 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -356,32 +356,18 @@ Qed.
 
 (** ** Relating global environments *)
 
-Inductive match_globalenvs (F: meminj) (bound: block): Prop :=
-  | mk_match_globalenvs
-      (DOMAIN: forall b, Plt b bound -> F b = Some(b, 0))
-      (IMAGE: forall b1 b2 delta, F b1 = Some(b2, delta) -> Plt b2 bound -> b1 = b2)
-      (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> Plt b bound)
-      (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> Plt b bound)
-      (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> Plt b bound).
-
 Lemma find_function_agree:
-  forall ros rs fd F ctx rs' bound,
+  forall ros rs fd F ctx rs',
   find_function ge ros rs = Some fd ->
   agree_regs F ctx rs rs' ->
-  match_globalenvs F bound ->
+  Genv.inject F ge ->
   exists cu fd',
   find_function tge (sros ctx ros) rs' = Some fd' /\ transf_fundef (funenv_program cu) fd = OK fd' /\ linkorder cu prog.
 Proof.
   intros. destruct ros as [r | id]; simpl in *.
 - (* register *)
   assert (EQ: rs'#(sreg ctx r) = rs#r).
-  { exploit Genv.find_funct_inv; eauto. intros [b EQ].
-    assert (A: Val.inject F rs#r rs'#(sreg ctx r)). eapply agree_val_reg; eauto.
-    rewrite EQ in A; inv A.
-    inv H1. rewrite DOMAIN in H5. inv H5. auto.
-    apply FUNCTIONS with fd.
-    rewrite EQ in H; rewrite Genv.find_funct_find_funct_ptr in H. auto.
-  }
+  { eapply Genv.find_funct_inject; eauto using agree_val_reg. }
   rewrite EQ. eapply functions_translated; eauto.
 - (* symbol *)
   rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try discriminate.
@@ -405,8 +391,8 @@ Qed.
 (** Translation of builtin arguments. *)
 
 Lemma tr_builtin_arg:
-  forall F bound ctx rs rs' sp sp' m m',
-  match_globalenvs F bound ->
+  forall F ctx rs rs' sp sp' m m',
+  Genv.inject F ge ->
   agree_regs F ctx rs rs' ->
   F sp = Some(sp', ctx.(dstk)) ->
   Mem.inject F m m' ->
@@ -415,7 +401,12 @@ Lemma tr_builtin_arg:
   exists v', eval_builtin_arg tge (fun r => rs'#r) (Vptr sp' Ptrofs.zero) m' (sbuiltinarg ctx a) v'
           /\ Val.inject F v v'.
 Proof.
-  intros until m'; intros MG AG SP MI. induction 1; simpl.
+  intros until m'; intros MG AG SP MI.
+  assert (SYMB: forall id ofs, Val.inject F (Senv.symbol_address ge id ofs) (Senv.symbol_address tge id ofs)).
+  { intros. unfold Senv.symbol_address; simpl. rewrite symbols_preserved.
+    destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto.
+    eauto using Val.inject_ptr_flat, Genv.find_symbol_inject. }
+  induction 1; simpl.
 - exists rs'#(sreg ctx x); split. constructor. eapply agree_val_reg; eauto.
 - econstructor; eauto with barg.
 - econstructor; eauto with barg.
@@ -426,16 +417,8 @@ Proof.
   simpl. econstructor; eauto. rewrite Ptrofs.add_zero_l; auto.
   intros (v' & A & B). exists v'; split; auto. constructor. simpl. rewrite Ptrofs.add_zero_l; auto.
 - econstructor; split. constructor. simpl. econstructor; eauto. rewrite ! Ptrofs.add_zero_l; auto.
-- assert (Val.inject F (Senv.symbol_address ge id ofs) (Senv.symbol_address tge id ofs)).
-  { unfold Senv.symbol_address; simpl; unfold Genv.symbol_address.
-    rewrite symbols_preserved. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto.
-    inv MG. econstructor. eauto. rewrite Ptrofs.add_zero; auto. }
-  exploit Mem.loadv_inject; eauto. intros (v' & A & B).
-  exists v'; eauto with barg.
-- econstructor; split. constructor.
-  unfold Senv.symbol_address; simpl; unfold Genv.symbol_address.
-  rewrite symbols_preserved. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto.
-  inv MG. econstructor. eauto. rewrite Ptrofs.add_zero; auto.
+- exploit Mem.loadv_inject; eauto. intros (v' & A & B). exists v'; eauto with barg.
+- econstructor; split. constructor. auto.
 - destruct IHeval_builtin_arg1 as (v1' & A1 & B1).
   destruct IHeval_builtin_arg2 as (v2' & A2 & B2).
   econstructor; split. eauto with barg. apply Val.longofwords_inject; auto.
@@ -446,8 +429,8 @@ Proof.
 Qed.
 
 Lemma tr_builtin_args:
-  forall F bound ctx rs rs' sp sp' m m',
-  match_globalenvs F bound ->
+  forall F ctx rs rs' sp sp' m m',
+  Genv.inject F ge ->
   agree_regs F ctx rs rs' ->
   F sp = Some(sp', ctx.(dstk)) ->
   Mem.inject F m m' ->
@@ -467,9 +450,9 @@ Qed.
 
 Inductive match_stacks (F: meminj) (m m': mem):
              list stackframe -> list stackframe -> block -> Prop :=
-  | match_stacks_nil: forall bound1 bound
-        (MG: match_globalenvs F bound1)
-        (BELOW: Ple bound1 bound),
+  | match_stacks_nil: forall bound
+        (GINJ: Genv.inject F ge)
+        (BELOW: Ple (Genv.genv_next ge) bound),
       match_stacks F m m' nil nil bound
   | match_stacks_cons: forall res f sp pc rs stk f' sp' rs' stk' bound fenv ctx
         (MS: match_stacks_inside F m m' stk stk' f' ctx sp' rs')
@@ -528,30 +511,15 @@ Variables m m': mem.
 
 Lemma match_stacks_globalenvs:
   forall stk stk' bound,
-  match_stacks F m m' stk stk' bound -> exists b, match_globalenvs F b
+  match_stacks F m m' stk stk' bound -> Genv.inject F ge
 with match_stacks_inside_globalenvs:
   forall stk stk' f ctx sp rs',
-  match_stacks_inside F m m' stk stk' f ctx sp rs' -> exists b, match_globalenvs F b.
+  match_stacks_inside F m m' stk stk' f ctx sp rs' -> Genv.inject F ge.
 Proof.
   induction 1; eauto.
   induction 1; eauto.
 Qed.
 
-Lemma match_globalenvs_preserves_globals:
-  forall b, match_globalenvs F b -> meminj_preserves_globals ge F.
-Proof.
-  intros. inv H. red. split. eauto. split. eauto.
-  intros. symmetry. eapply IMAGE; eauto.
-Qed.
-
-Lemma match_stacks_inside_globals:
-  forall stk stk' f ctx sp rs',
-  match_stacks_inside F m m' stk stk' f ctx sp rs' -> meminj_preserves_globals ge F.
-Proof.
-  intros. exploit match_stacks_inside_globalenvs; eauto. intros [b A].
-  eapply match_globalenvs_preserves_globals; eauto.
-Qed.
-
 Lemma match_stacks_bound:
   forall stk stk' bound bound1,
   match_stacks F m m' stk stk' bound ->
@@ -559,7 +527,7 @@ Lemma match_stacks_bound:
   match_stacks F m m' stk stk' bound1.
 Proof.
   intros. inv H.
-  apply match_stacks_nil with bound0. auto. eapply Ple_trans; eauto.
+  apply match_stacks_nil. auto. eapply Ple_trans; eauto.
   eapply match_stacks_cons; eauto. eapply Pos.lt_le_trans; eauto.
   eapply match_stacks_untailcall; eauto. eapply Pos.lt_le_trans; eauto.
 Qed.
@@ -600,10 +568,10 @@ with match_stacks_inside_invariant:
 Proof.
   induction 1; intros.
   (* nil *)
-  apply match_stacks_nil with (bound1 := bound1).
-  inv MG. constructor; auto.
-  intros. apply IMAGE with delta. eapply INJ; eauto. eapply Pos.lt_le_trans; eauto.
-  auto. auto.
+  apply match_stacks_nil; auto.
+  destruct GINJ as [A B]. split; intros.
+  apply INCR. apply A. extlia.
+  apply B; auto. apply INJ; auto. extlia.
   (* cons *)
   apply match_stacks_cons with (fenv := fenv) (ctx := ctx); auto.
   eapply match_stacks_inside_invariant; eauto.
@@ -773,10 +741,10 @@ with match_stacks_inside_extcall:
   match_stacks_inside F2 m2 m2' stk stk' f' ctx sp' rs'.
 Proof.
   induction 1; intros.
-  apply match_stacks_nil with bound1; auto.
-    inv MG. constructor; intros; eauto.
-    destruct (F1 b1) as [[b2' delta']|] eqn:?.
-    exploit INCR; eauto. intros EQ; rewrite H0 in EQ; inv EQ. eapply IMAGE; eauto.
+  apply match_stacks_nil; auto.
+    destruct GINJ as [P Q]. split; intros; eauto.
+    destruct (F1 b) as [[b0 delta0]|] eqn:?.
+    exploit INCR; eauto. intros EQ; rewrite H0 in EQ; inv EQ. eauto.
     exploit SEP; eauto. intros [A B]. elim B. red. extlia.
   eapply match_stacks_cons; eauto.
     eapply match_stacks_inside_extcall; eauto. extlia.
@@ -921,7 +889,7 @@ Proof.
 - (* op *)
   exploit tr_funbody_inv; eauto. intros TR; inv TR.
   exploit eval_operation_inject.
-    eapply match_stacks_inside_globals; eauto.
+    eapply match_stacks_inside_globalenvs; eauto.
     eexact SP.
     instantiate (2 := rs##args). instantiate (1 := rs'##(sregs ctx args)). eapply agree_val_regs; eauto.
     eexact MINJ. eauto.
@@ -936,7 +904,7 @@ Proof.
 - (* load *)
   exploit tr_funbody_inv; eauto. intros TR; inv TR.
   exploit eval_addressing_inject.
-    eapply match_stacks_inside_globals; eauto.
+    eapply match_stacks_inside_globalenvs; eauto.
     eexact SP.
     instantiate (2 := rs##args). instantiate (1 := rs'##(sregs ctx args)). eapply agree_val_regs; eauto.
     eauto.
@@ -953,7 +921,7 @@ Proof.
 - (* store *)
   exploit tr_funbody_inv; eauto. intros TR; inv TR.
   exploit eval_addressing_inject.
-    eapply match_stacks_inside_globals; eauto.
+    eapply match_stacks_inside_globalenvs; eauto.
     eexact SP.
     instantiate (2 := rs##args). instantiate (1 := rs'##(sregs ctx args)). eapply agree_val_regs; eauto.
     eauto.
@@ -973,8 +941,7 @@ Proof.
   intros. eapply SSZ2. eapply Mem.perm_store_2; eauto with mem.
 
 - (* call *)
-  exploit match_stacks_inside_globalenvs; eauto. intros [bound G].
-  exploit find_function_agree; eauto. intros (cu & fd' & A & B & C).
+  exploit find_function_agree; eauto using match_stacks_inside_globalenvs. intros (cu & fd' & A & B & C).
   exploit tr_funbody_inv; eauto. intros TR; inv TR.
 + (* not inlined *)
   left; econstructor; split.
@@ -994,8 +961,7 @@ Proof.
   red; intros; apply PRIV. destruct H16. lia.
 
 - (* tailcall *)
-  exploit match_stacks_inside_globalenvs; eauto. intros [bound G].
-  exploit find_function_agree; eauto. intros (cu & fd' & A & B & C).
+  exploit find_function_agree; eauto using match_stacks_inside_globalenvs. intros (cu & fd' & A & B & C).
   assert (PRIV': range_private F m' m'0 sp' (dstk ctx) f'.(fn_stacksize)).
   { eapply range_private_free_left; eauto. inv FB. rewrite <- H4. auto. }
   exploit tr_funbody_inv; eauto. intros TR; inv TR.
@@ -1050,10 +1016,8 @@ Proof.
 
 - (* builtin *)
   exploit tr_funbody_inv; eauto. intros TR; inv TR.
-  exploit match_stacks_inside_globalenvs; eauto. intros [bound MG].
-  exploit tr_builtin_args; eauto. intros (vargs' & P & Q).
-  exploit external_call_mem_inject; eauto.
-    eapply match_stacks_inside_globals; eauto.
+  exploit tr_builtin_args; eauto using match_stacks_inside_globalenvs. intros (vargs' & P & Q).
+  exploit external_call_mem_inject; eauto using match_stacks_inside_globalenvs.
   intros [F1 [v1 [m1' [A [B [C [D [E [J K]]]]]]]]].
   left; econstructor; split.
   eapply plus_one. eapply exec_Ibuiltin; eauto.
@@ -1205,9 +1169,7 @@ Proof.
   auto. auto.
 
 - (* external function *)
-  exploit match_stacks_globalenvs; eauto. intros [bound MG].
-  exploit external_call_mem_inject; eauto.
-    eapply match_globalenvs_preserves_globals; eauto.
+  exploit external_call_mem_inject; eauto using match_stacks_globalenvs.
   intros [F1 [v1 [m1' [A [B [C [D [E [J K]]]]]]]]].
   simpl in FD. inv FD.
   left; econstructor; split.
@@ -1272,14 +1234,8 @@ Proof.
     rewrite <- H3. eapply sig_function_translated; eauto.
   econstructor; eauto.
   instantiate (1 := Mem.flat_inj (Mem.nextblock m0)).
-  apply match_stacks_nil with (Mem.nextblock m0).
-  constructor; intros.
-    unfold Mem.flat_inj. apply pred_dec_true; auto.
-    unfold Mem.flat_inj in H. destruct (plt b1 (Mem.nextblock m0)); congruence.
-    eapply Genv.find_symbol_not_fresh; eauto.
-    eapply Genv.find_funct_ptr_not_fresh; eauto.
-    eapply Genv.find_var_info_not_fresh; eauto.
-    apply Ple_refl.
+  erewrite <- Genv.init_mem_genv_next by eauto.
+  apply match_stacks_nil. apply Genv.init_inject. apply Ple_refl.
   eapply Genv.initmem_inject; eauto.
 Qed.
 
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index 2d9de77b7..2fda22b30 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -1610,14 +1610,13 @@ Lemma find_function_translated:
   /\ Genv.find_funct_ptr tge bf = Some tf
   /\ transf_fundef f = OK tf.
 Proof.
-  intros until f; intros AG [bound [_ [?????]]] FF.
+  intros until f; intros AG [BOUND GINJ] FF.
   destruct ros; simpl in FF.
-- exploit Genv.find_funct_inv; eauto. intros [b EQ]. rewrite EQ in FF.
+- exploit Genv.find_funct_inject; eauto. intros EQ.
+  exploit Genv.find_funct_inv; eauto. intros [b EQ']. rewrite EQ' in FF.
   rewrite Genv.find_funct_find_funct_ptr in FF.
   exploit function_ptr_translated; eauto. intros [tf [A B]].
-  exists b; exists tf; split; auto. simpl.
-  generalize (AG m0). rewrite EQ. intro INJ. inv INJ.
-  rewrite DOMAIN in H2. inv H2. simpl. auto. eapply FUNCTIONS; eauto.
+  exists b; exists tf; split; auto. simpl. rewrite EQ, EQ'. auto.
 - destruct (Genv.find_symbol ge i) as [b|] eqn:?; try discriminate.
   exploit function_ptr_translated; eauto. intros [tf [A B]].
   exists b; exists tf; split; auto. simpl.
@@ -1734,11 +1733,8 @@ Lemma transl_builtin_arg_correct:
   /\ Val.inject j v v'.
 Proof.
   assert (SYMB: forall id ofs, Val.inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address ge id ofs)).
-  { assert (G: meminj_preserves_globals ge j).
-    { eapply globalenv_inject_preserves_globals. eapply sep_proj2. eapply sep_proj2. eexact SEP. }
-    intros; unfold Senv.symbol_address; simpl; unfold Genv.symbol_address.
-    destruct (Genv.find_symbol ge id) eqn:FS; auto.
-    destruct G. econstructor. eauto. rewrite Ptrofs.add_zero; auto. }
+  { intros. apply Genv.symbol_address_inject.
+    eapply globalenv_inject_preserves_globals. eapply sep_proj2. eapply sep_proj2. eexact SEP. }
 Local Opaque fe.
   induction 1; simpl; intros VALID BOUNDS.
 - assert (loc_valid f x = true) by auto.
@@ -2171,13 +2167,8 @@ Proof.
   red; simpl; auto.
   simpl. rewrite sep_pure. split; auto. split;[|split].
   eapply Genv.initmem_inject; eauto.
-  simpl. exists (Mem.nextblock m0); split. apply Ple_refl.
-  unfold j, Mem.flat_inj; constructor; intros.
-    apply pred_dec_true; auto.
-    destruct (plt b1 (Mem.nextblock m0)); congruence.
-    change (Mem.valid_block m0 b0). eapply Genv.find_symbol_not_fresh; eauto.
-    change (Mem.valid_block m0 b0). eapply Genv.find_funct_ptr_not_fresh; eauto.
-    change (Mem.valid_block m0 b0). eapply Genv.find_var_info_not_fresh; eauto.
+  simpl. unfold j. erewrite <- Genv.init_mem_genv_next by eauto. 
+  auto using Genv.init_inject, Ple_refl.
   red; simpl; tauto.
 Qed.
 
diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v
index c741e96fc..81c128427 100644
--- a/backend/Unusedglobproof.v
+++ b/backend/Unusedglobproof.v
@@ -586,14 +586,14 @@ Proof.
 Qed.
 
 Lemma globals_symbols_inject:
-  forall j, meminj_preserves_globals j -> symbols_inject j ge tge.
+  forall j, meminj_preserves_globals j -> Senv.inject j ge tge.
 Proof.
   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. eapply match_prog_public; eauto. }
-  split; [|split;[|split]]; intros.
+  constructor; 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.
@@ -628,7 +628,7 @@ Lemma symbol_address_inject:
 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.
-  econstructor; eauto. rewrite Ptrofs.add_zero; auto.
+  eapply Val.inject_ptr_flat; eauto.
 Qed.
 
 (** Semantic preservation *)
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 498ff8e50..9d142ce84 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -956,7 +956,7 @@ Proof.
   intros until am; intros EC GENV ARGS RO MM NOSTACK.
   (* Part 1: using ec_mem_inject *)
   exploit (@external_call_mem_inject ef _ _ ge vargs m t vres m' (inj_of_bc bc) m vargs).
-  apply inj_of_bc_preserves_globals; auto.
+  apply inj_of_bc_inject_globals; auto.
   exact EC.
   eapply mmatch_inj; eauto. eapply mmatch_below; eauto.
   revert ARGS. generalize vargs.
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 165540777..c65b6bddb 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -5037,14 +5037,12 @@ Proof.
   rewrite Z.add_0_r in H2. auto.
 Qed.
 
-Lemma inj_of_bc_preserves_globals:
-  forall bc ge, genv_match bc ge -> meminj_preserves_globals ge (inj_of_bc bc).
-Proof.
-  intros. destruct H as [A B].
-  split. intros. apply inj_of_bc_valid. rewrite A in H. congruence.
-  split. intros. apply inj_of_bc_valid. apply B.
-    rewrite Genv.find_var_info_iff in H. eapply Genv.genv_defs_range; eauto.
-  intros. exploit inj_of_bc_inv; eauto. intros (P & Q & R). auto.
+Lemma inj_of_bc_inject_globals:
+  forall bc ge, genv_match bc ge -> Genv.inject (inj_of_bc bc) ge.
+Proof.
+  intros. destruct H as [A B]. split; intros.
+- apply inj_of_bc_valid. apply B; auto.
+- eapply inj_of_bc_inv; eauto. 
 Qed.
 
 Lemma pmatch_inj_top:
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index c02b05c57..47c5a82a2 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -416,30 +416,6 @@ Proof.
   congruence.
 Qed.
 
-(** * Correspondence between global environments *)
-
-(** Global environments match if the memory injection [f] leaves unchanged
-  the references to global symbols and functions. *)
-
-Inductive match_globalenvs (f: meminj) (bound: block): Prop :=
-  | mk_match_globalenvs
-      (DOMAIN: forall b, Plt b bound -> f b = Some(b, 0))
-      (IMAGE: forall b1 b2 delta, f b1 = Some(b2, delta) -> Plt b2 bound -> b1 = b2)
-      (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> Plt b bound)
-      (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> Plt b bound)
-      (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> Plt b bound).
-
-Remark inj_preserves_globals:
-  forall f hi,
-  match_globalenvs f hi ->
-  meminj_preserves_globals ge f.
-Proof.
-  intros. inv H.
-  split. intros. apply DOMAIN. eapply SYMBOLS. eauto.
-  split. intros. apply DOMAIN. eapply VARINFOS. eauto.
-  intros. symmetry. eapply IMAGE; eauto.
-Qed.
-
 (** * Invariant on abstract call stacks  *)
 
 (** Call stacks represent abstractly the execution state of the current
@@ -471,9 +447,9 @@ Definition callstack : Type := list frame.
 Inductive match_callstack (f: meminj) (m: mem) (tm: mem):
                           callstack -> block -> block -> Prop :=
   | mcs_nil:
-      forall hi bound tbound,
-      match_globalenvs f hi ->
-      Ple hi bound -> Ple hi tbound ->
+      forall bound tbound,
+      Genv.inject f ge ->
+      Ple (Genv.genv_next ge) bound -> Ple (Genv.genv_next ge) tbound ->
       match_callstack f m tm nil bound tbound
   | mcs_cons:
       forall cenv tf e le te sp lo hi cs bound tbound
@@ -486,12 +462,12 @@ Inductive match_callstack (f: meminj) (m: mem) (tm: mem):
         (MCS: match_callstack f m tm cs lo sp),
       match_callstack f m tm (Frame cenv tf e le te sp lo hi :: cs) bound tbound.
 
-(** [match_callstack] implies [match_globalenvs]. *)
+(** [match_callstack] implies [Genv.inject]. *)
 
-Lemma match_callstack_match_globalenvs:
+Lemma match_callstack_genv_inject:
   forall f m tm cs bound tbound,
   match_callstack f m tm cs bound tbound ->
-  exists hi, match_globalenvs f hi.
+  Genv.inject f ge.
 Proof.
   induction 1; eauto.
 Qed.
@@ -509,11 +485,11 @@ Lemma match_callstack_invariant:
   match_callstack f2 m2 tm2 cs bound tbound.
 Proof.
   induction 1; intros.
-  (* base case *)
-  econstructor; eauto.
-  inv H. constructor; intros; eauto.
-  eapply IMAGE; eauto. eapply H6; eauto. extlia.
-  (* inductive case *)
+- (* base case *)
+  econstructor; eauto. destruct H as [A B]; split; intros.
++ rewrite H5 by extlia; auto.
++ apply B; auto. apply H6; auto. extlia.
+- (* inductive case *)
   assert (Ple lo hi) by (eapply me_low_high; eauto).
   econstructor; eauto.
   eapply match_temps_invariant; eauto.
@@ -631,13 +607,14 @@ Proof.
   intros until m2'.
   intros UNMAPPED OUTOFREACH INCR SEPARATED MAXPERMS.
   induction 1; intros.
-(* base case *)
-  apply mcs_nil with hi; auto.
-  inv H. constructor; auto.
-  intros. case_eq (f1 b1).
-  intros [b2' delta'] EQ. rewrite (INCR _ _ _ EQ) in H. inv H. eauto.
-  intro EQ. exploit SEPARATED; eauto. intros [A B]. elim B. red. extlia.
-(* inductive case *)
+- (* base case *)
+  apply mcs_nil; auto.
+  destruct H as [P Q]. split; intros.
++ apply INCR; auto.
++ destruct (f1 b) as [[b0 delta0] | ] eqn:EQ.
+  rewrite (INCR _ _ _ EQ) in H. inv H. eauto.
+  exploit SEPARATED; eauto. intros [A B]. elim B. red. extlia.
+- (* inductive case *)
   constructor. auto. auto.
   eapply match_temps_invariant; eauto.
   eapply match_env_invariant; eauto.
@@ -1418,10 +1395,10 @@ Proof.
   constructor. simpl. rewrite Ptrofs.add_zero_l; auto.
   congruence.
   (* global *)
-  exploit match_callstack_match_globalenvs; eauto. intros [bnd MG]. inv MG.
+  exploit Genv.find_symbol_inject; eauto using match_callstack_genv_inject. intros IMG.
   exists (Vptr b Ptrofs.zero); split.
   constructor. simpl. unfold Genv.symbol_address. 
-  rewrite symbols_preserved. rewrite H2. auto.
+  rewrite symbols_preserved, H2. auto.
   econstructor; eauto.
 Qed.
 
@@ -1601,19 +1578,6 @@ Inductive match_states: Csharpminor.state -> Cminor.state -> Prop :=
       match_states (Csharpminor.Returnstate v k m)
                    (Returnstate tv tk tm).
 
-Remark val_inject_function_pointer:
-  forall bound v fd f tv,
-  Genv.find_funct ge v = Some fd ->
-  match_globalenvs f bound ->
-  Val.inject f v tv ->
-  tv = v.
-Proof.
-  intros. exploit Genv.find_funct_inv; eauto. intros [b EQ]. subst v.
-  rewrite Genv.find_funct_find_funct_ptr in H.
-  assert (f b = Some(b, 0)). inv H0. apply DOMAIN. eapply FUNCTIONS; eauto.
-  inv H1. rewrite H2 in H5; inv H5. reflexivity.
-Qed.
-
 Lemma match_call_cont:
   forall k tk cenv xenv cs,
   match_cont k tk cenv xenv cs ->
@@ -1986,8 +1950,7 @@ Proof.
   monadInv TR.
   exploit transl_expr_correct; eauto. intros [tvf [EVAL1 VINJ1]].
   assert (tvf = vf).
-    exploit match_callstack_match_globalenvs; eauto. intros [bnd MG].
-    eapply val_inject_function_pointer; eauto.
+  { eapply Genv.find_funct_inject; eauto using match_callstack_genv_inject. }
   subst tvf.
   exploit transl_exprlist_correct; eauto.
   intros [tvargs [EVAL2 VINJ2]].
@@ -2002,9 +1965,7 @@ Proof.
   monadInv TR.
   exploit transl_exprlist_correct; eauto.
   intros [tvargs [EVAL2 VINJ2]].
-  exploit match_callstack_match_globalenvs; eauto. intros [hi' MG].
-  exploit external_call_mem_inject; eauto.
-  eapply inj_preserves_globals; eauto.
+  exploit external_call_mem_inject; eauto using match_callstack_genv_inject.
   intros [f' [vres' [tm' [EC [VINJ [MINJ' [UNMAPPED [OUTOFREACH [INCR SEPARATED]]]]]]]]].
   left; econstructor; split.
   apply plus_one. econstructor. eauto.
@@ -2156,9 +2117,7 @@ Opaque PTree.set.
 
 (* external call *)
   monadInv TR.
-  exploit match_callstack_match_globalenvs; eauto. intros [hi MG].
-  exploit external_call_mem_inject; eauto.
-  eapply inj_preserves_globals; eauto.
+  exploit external_call_mem_inject; eauto using match_callstack_genv_inject.
   intros [f' [vres' [tm' [EC [VINJ [MINJ' [UNMAPPED [OUTOFREACH [INCR SEPARATED]]]]]]]]].
   left; econstructor; split.
   apply plus_one. econstructor.
@@ -2179,20 +2138,6 @@ Opaque PTree.set.
   eapply match_callstack_set_temp; eauto.
 Qed.
 
-Lemma match_globalenvs_init:
-  forall m,
-  Genv.init_mem prog = Some m ->
-  match_globalenvs (Mem.flat_inj (Mem.nextblock m)) (Mem.nextblock m).
-Proof.
-  intros. constructor.
-  intros. unfold Mem.flat_inj. apply pred_dec_true; auto.
-  intros. unfold Mem.flat_inj in H0.
-  destruct (plt b1 (Mem.nextblock m)); congruence.
-  intros. eapply Genv.find_symbol_not_fresh; eauto.
-  intros. eapply Genv.find_funct_ptr_not_fresh; eauto.
-  intros. eapply Genv.find_var_info_not_fresh; eauto.
-Qed.
-
 Lemma transl_initial_states:
   forall S, Csharpminor.initial_state prog S ->
   exists R, Cminor.initial_state tprog R /\ match_states S R.
@@ -2211,8 +2156,9 @@ Proof.
   eapply match_callstate with (f := Mem.flat_inj (Mem.nextblock m0)) (cs := @nil frame) (cenv := PTree.empty Z).
   auto.
   eapply Genv.initmem_inject; eauto.
-  apply mcs_nil with (Mem.nextblock m0). apply match_globalenvs_init; auto. extlia. extlia.
-  constructor. red; auto.
+  erewrite <- Genv.init_mem_genv_next by eauto. apply mcs_nil; auto using Genv.init_inject, Ple_refl.
+  constructor.
+  red; auto.
   constructor.
 Qed.
 
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 8fde56f5f..a911e420d 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -1370,25 +1370,6 @@ Local Opaque ge tge.
   rewrite <- comp_env_preserved. lia.
 Qed.
 
-(** Matching global environments *)
-
-Inductive match_globalenvs (f: meminj) (bound: block): Prop :=
-  | mk_match_globalenvs
-      (DOMAIN: forall b, Plt b bound -> f b = Some(b, 0))
-      (IMAGE: forall b1 b2 delta, f b1 = Some(b2, delta) -> Plt b2 bound -> b1 = b2)
-      (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> Plt b bound)
-      (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> Plt b bound)
-      (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> Plt b bound).
-
-Lemma match_globalenvs_preserves_globals:
-  forall f,
-  (exists bound, match_globalenvs f bound) ->
-  meminj_preserves_globals ge f.
-Proof.
-  intros. destruct H as [bound MG]. inv MG.
-  split; intros. eauto. split; intros. eauto. symmetry. eapply IMAGE; eauto.
-Qed.
-
 (** Evaluation of expressions *)
 
 Section EVAL_EXPR.
@@ -1401,7 +1382,7 @@ Variable cenv: compilenv.
 Variables lo hi tlo thi: block.
 Hypothesis MATCH: match_envs f cenv e le m lo hi te tle tlo thi.
 Hypothesis MEMINJ: Mem.inject f m tm.
-Hypothesis GLOB: exists bound, match_globalenvs f bound.
+Hypothesis GLOB: Genv.inject f ge.
 
 Lemma typeof_simpl_expr:
   forall a, typeof (simpl_expr cenv a) = typeof a.
@@ -1511,8 +1492,7 @@ Proof.
   exploit me_vars; eauto. instantiate (1 := id). intros MV. inv MV; try congruence.
   exists l; exists Ptrofs.zero; split.
   apply eval_Evar_global. auto. rewrite <- H0. apply symbols_preserved.
-  destruct GLOB as [bound GLOB1]. inv GLOB1.
-  econstructor; eauto.
+  eauto using Val.inject_ptr_flat, Genv.find_symbol_inject.
 (* deref *)
   exploit eval_simpl_expr; eauto. intros [tv [A B]].
   inversion B. subst.
@@ -1558,8 +1538,8 @@ End EVAL_EXPR.
 (** Matching continuations *)
 
 Inductive match_cont (f: meminj): compilenv -> cont -> cont -> mem -> block -> block -> Prop :=
-  | match_Kstop: forall cenv m bound tbound hi,
-      match_globalenvs f hi -> Ple hi bound -> Ple hi tbound ->
+  | match_Kstop: forall cenv m bound tbound,
+      Genv.inject f ge -> Ple (Genv.genv_next ge) bound -> Ple (Genv.genv_next ge) tbound ->
       match_cont f cenv Kstop Kstop m bound tbound
   | match_Kseq: forall cenv s k ts tk m bound tbound,
       simpl_stmt cenv s = OK ts ->
@@ -1604,9 +1584,9 @@ Lemma match_cont_invariant:
 Proof.
   induction 1; intros LOAD INCR INJ1 INJ2; econstructor; eauto.
 (* globalenvs *)
-  inv H. constructor; intros; eauto.
-  assert (f b1 = Some (b2, delta)). rewrite <- H; symmetry; eapply INJ2; eauto. extlia.
-  eapply IMAGE; eauto.
+  destruct H as [A B]. split; intros; eauto.
+  assert (f b = Some (b', delta)). rewrite <- H; symmetry; eapply INJ2; eauto. extlia.
+  eapply B; eauto.
 (* call *)
   eapply match_envs_invariant; eauto.
   intros. apply LOAD; auto. extlia.
@@ -1748,9 +1728,9 @@ Qed.
 Lemma match_cont_globalenv:
   forall f cenv k tk m bound tbound,
   match_cont f cenv k tk m bound tbound ->
-  exists bound, match_globalenvs f bound.
+  Genv.inject f ge.
 Proof.
-  induction 1; auto. exists hi; auto.
+  induction 1; auto.
 Qed.
 
 Hint Resolve match_cont_globalenv: compat.
@@ -1762,13 +1742,11 @@ Lemma match_cont_find_funct:
   Val.inject f vf tvf ->
   exists tfd, Genv.find_funct tge tvf = Some tfd /\ transf_fundef fd = OK tfd.
 Proof.
-  intros. exploit match_cont_globalenv; eauto. intros [bound1 MG]. destruct MG.
-  inv H1; simpl in H0; try discriminate. destruct (Ptrofs.eq_dec ofs1 Ptrofs.zero); try discriminate.
-  subst ofs1.
-  assert (f b1 = Some(b1, 0)).
-    apply DOMAIN. eapply FUNCTIONS; eauto.
-  rewrite H1 in H2; inv H2.
-  rewrite Ptrofs.add_zero. simpl. rewrite dec_eq_true. apply function_ptr_translated; auto.
+  intros.
+  exploit Genv.find_funct_inject; eauto using match_cont_globalenv. intro EQ; subst tvf.
+  exploit Genv.find_funct_inv; eauto. intros (b & EQ). subst vf.
+  rewrite ! Genv.find_funct_find_funct_ptr in *.
+  eapply function_ptr_translated; eauto.
 Qed.
 
 (** Relating execution states *)
@@ -2039,7 +2017,7 @@ Proof.
   generalize (is_liftable_var_charact (cenv_for f) a1); destruct (is_liftable_var (cenv_for f) a1) as [id|]; monadInv TRS.
   (* liftable *)
   intros [ty [P Q]]; subst a1; simpl in *.
-  exploit eval_simpl_expr; eauto with compat. intros [tv2 [A B]].
+  exploit eval_simpl_expr; eauto with compat.  intros [tv2 [A B]].
   exploit sem_cast_inject; eauto. intros [tv [C D]].
   exploit me_vars; eauto. instantiate (1 := id). intros MV.
   inv H.
@@ -2090,7 +2068,7 @@ Proof.
 
 (* builtin *)
   exploit eval_simpl_exprlist; eauto with compat. intros [CASTED [tvargs [C D]]].
-  exploit external_call_mem_inject; eauto. apply match_globalenvs_preserves_globals; eauto with compat.
+  exploit external_call_mem_inject; eauto with compat.
   intros [j' [tvres [tm' [P [Q [R [S [T [U V]]]]]]]]].
   econstructor; split.
   apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
@@ -2250,7 +2228,7 @@ Proof.
 
 (* external function *)
   monadInv TRFD. inv FUNTY.
-  exploit external_call_mem_inject; eauto. apply match_globalenvs_preserves_globals.
+  exploit external_call_mem_inject; eauto.
   eapply match_cont_globalenv. eexact (MCONT VSet.empty).
   intros [j' [tvres [tm' [P [Q [R [S [T [U V]]]]]]]]].
   econstructor; split.
@@ -2285,14 +2263,8 @@ Proof.
   rewrite <- H3; apply type_of_fundef_preserved; auto.
   econstructor; eauto.
   intros. instantiate (1 := Mem.flat_inj (Mem.nextblock m0)).
-  econstructor. instantiate (1 := Mem.nextblock m0).
-  constructor; intros.
-  unfold Mem.flat_inj. apply pred_dec_true; auto.
-  unfold Mem.flat_inj in H. destruct (plt b1 (Mem.nextblock m0)); inv H. auto.
-  eapply Genv.find_symbol_not_fresh; eauto.
-  eapply Genv.find_funct_ptr_not_fresh; eauto.
-  eapply Genv.find_var_info_not_fresh; eauto.
-  extlia. extlia.
+  erewrite <- Genv.init_mem_genv_next by eauto.
+  constructor; auto using Genv.init_inject, Ple_refl.
   eapply Genv.initmem_inject; eauto.
   constructor.
 Qed.
diff --git a/common/Events.v b/common/Events.v
index 38cf6139d..a106c009a 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -444,30 +444,18 @@ End EVENTVAL_INV.
 
 Section EVENTVAL_INJECT.
 
-Variable f: block -> option (block * Z).
+Variable f: meminj.
 Variable ge1 ge2: Senv.t.
-
-Definition symbols_inject : Prop :=
-   (forall id, Senv.public_symbol ge2 id = Senv.public_symbol ge1 id)
-/\ (forall id b1 b2 delta,
-     f b1 = Some(b2, delta) -> Senv.find_symbol ge1 id = Some b1 ->
-     delta = 0 /\ Senv.find_symbol ge2 id = Some b2)
-/\ (forall id b1,
-     Senv.public_symbol ge1 id = true -> Senv.find_symbol ge1 id = Some b1 ->
-     exists b2, f b1 = Some(b2, 0) /\ Senv.find_symbol ge2 id = Some b2)
-/\ (forall b1 b2 delta,
-     f b1 = Some(b2, delta) ->
-     Senv.block_is_volatile ge2 b2 = Senv.block_is_volatile ge1 b1).
-
-Hypothesis symb_inj: symbols_inject.
+Hypothesis symb_inj: Senv.inject f ge1 ge2.
 
 Lemma eventval_match_inject:
   forall ev ty v1 v2,
   eventval_match ge1 ev ty v1 -> Val.inject f v1 v2 -> eventval_match ge2 ev ty v2.
 Proof.
   intros. inv H; inv H0; try constructor; auto.
-  destruct symb_inj as (A & B & C & D). exploit C; eauto. intros [b3 [EQ FS]]. rewrite H4 in EQ; inv EQ.
-  rewrite Ptrofs.add_zero. constructor; auto. rewrite A; auto.
+  exploit Senv.find_public_symbol_inject; eauto. intros [b3 [EQ FS]].
+  rewrite H4 in EQ; inv EQ. rewrite Ptrofs.add_zero.
+  constructor; auto. rewrite (Senv.public_symbol_inject symb_inj); auto.
 Qed.
 
 Lemma eventval_match_inject_2:
@@ -476,8 +464,9 @@ Lemma eventval_match_inject_2:
   exists v2, eventval_match ge2 ev ty v2 /\ Val.inject f v1 v2.
 Proof.
   intros. inv H; try (econstructor; split; eauto; constructor; fail).
-  destruct symb_inj as (A & B & C & D). exploit C; eauto. intros [b2 [EQ FS]].
-  exists (Vptr b2 ofs); split. econstructor; eauto.
+  exploit Senv.find_public_symbol_inject; eauto. intros [b2 [EQ FS]].
+  exists (Vptr b2 ofs); split. 
+  econstructor; eauto. rewrite (Senv.public_symbol_inject symb_inj); auto.
   econstructor; eauto. rewrite Ptrofs.add_zero; auto.
 Qed.
 
@@ -673,7 +662,7 @@ Record extcall_properties (sem: extcall_sem) (sg: signature) : Prop :=
   in the following sense. *)
   ec_mem_inject:
     forall ge1 ge2 vargs m1 t vres m2 f m1' vargs',
-    symbols_inject f ge1 ge2 ->
+    Senv.inject f ge1 ge2 ->
     sem ge1 vargs m1 t vres m2 ->
     Mem.inject f m1 m1' ->
     Val.inject_list f vargs vargs' ->
@@ -738,26 +727,26 @@ Qed.
 
 Lemma volatile_load_inject:
   forall ge1 ge2 f chunk m b ofs t v b' ofs' m',
-  symbols_inject f ge1 ge2 ->
+  Senv.inject f ge1 ge2 ->
   volatile_load ge1 chunk m b ofs t v ->
   Val.inject f (Vptr b ofs) (Vptr b' ofs') ->
   Mem.inject f m m' ->
   exists v', volatile_load ge2 chunk m' b' ofs' t v' /\ Val.inject f v v'.
 Proof.
-  intros until m'; intros SI VL VI MI. generalize SI; intros (A & B & C & D).
+  intros until m'; intros SI VL VI MI.
   inv VL.
 - (* volatile load *)
-  inv VI. exploit B; eauto. intros [U V]. subst delta.
+  inv VI. exploit Senv.find_symbol_inject; eauto. intros [U V]. subst delta.
   exploit eventval_match_inject_2; eauto. intros (v2 & X & Y).
   rewrite Ptrofs.add_zero. exists (Val.load_result chunk v2); split.
   constructor; auto.
-  erewrite D; eauto.
+  erewrite Senv.block_is_volatile_inject; eauto.
   apply Val.load_result_inject. auto.
 - (* normal load *)
   exploit Mem.loadv_inject; eauto. intros (v2 & X & Y).
   exists v2; split; auto.
   constructor; auto.
-  inv VI. erewrite D; eauto.
+  inv VI. erewrite Senv.block_is_volatile_inject; eauto.
 Qed.
 
 Lemma volatile_load_receptive:
@@ -889,7 +878,7 @@ Qed.
 
 Lemma volatile_store_inject:
   forall ge1 ge2 f chunk m1 b ofs v t m2 m1' b' ofs' v',
-  symbols_inject f ge1 ge2 ->
+  Senv.inject f ge1 ge2 ->
   volatile_store ge1 chunk m1 b ofs v t m2 ->
   Val.inject f (Vptr b ofs) (Vptr b' ofs') ->
   Val.inject f v v' ->
@@ -901,20 +890,19 @@ Lemma volatile_store_inject:
     /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2'.
 Proof.
   intros until v'; intros SI VS AI VI MI.
-  generalize SI; intros (P & Q & R & S).
   inv VS.
 - (* volatile store *)
-  inv AI. exploit Q; eauto. intros [A B]. subst delta.
+  inv AI. exploit Senv.find_symbol_inject; eauto. intros [A B]. subst delta.
   rewrite Ptrofs.add_zero. exists m1'; split.
-  constructor; auto. erewrite S; eauto.
+  constructor; auto. erewrite Senv.block_is_volatile_inject; eauto.
   eapply eventval_match_inject; eauto. apply Val.load_result_inject. auto.
   intuition auto with mem.
 - (* normal store *)
   inversion AI; subst.
   exploit Mem.storev_mapped_inject; eauto. intros [m2' [A B]].
   exists m2'; intuition auto.
-+ constructor; auto. erewrite S; eauto.
-+ eapply Mem.storev_unchanged_on; eauto.
+  constructor; auto. erewrite Senv.block_is_volatile_inject; eauto.
+  eapply Mem.storev_unchanged_on; eauto.
   unfold loc_unmapped; intros. inv AI; congruence.
 + eapply Mem.storev_unchanged_on; eauto.
   unfold loc_out_of_reach; intros. red; intros.
@@ -1595,14 +1583,9 @@ Qed.
 
 (** Special case of [external_call_mem_inject_gen] (for backward compatibility) *)
 
-Definition meminj_preserves_globals (F V: Type) (ge: Genv.t F V) (f: block -> option (block * Z)) : Prop :=
-     (forall id b, Genv.find_symbol ge id = Some b -> f b = Some(b, 0))
-  /\ (forall b gv, Genv.find_var_info ge b = Some gv -> f b = Some(b, 0))
-  /\ (forall b1 b2 delta gv, Genv.find_var_info ge b2 = Some gv -> f b1 = Some(b2, delta) -> b2 = b1).
-
 Lemma external_call_mem_inject:
   forall ef F V (ge: Genv.t F V) vargs m1 t vres m2 f m1' vargs',
-  meminj_preserves_globals ge f ->
+  Genv.inject f ge ->
   external_call ef ge vargs m1 t vres m2 ->
   Mem.inject f m1 m1' ->
   Val.inject_list f vargs vargs' ->
@@ -1615,16 +1598,7 @@ Lemma external_call_mem_inject:
     /\ inject_incr f f'
     /\ inject_separated f f' m1 m1'.
 Proof.
-  intros. destruct H as (A & B & C). eapply external_call_mem_inject_gen with (ge1 := ge); eauto.
-  repeat split; intros.
-  + simpl in H3. exploit A; eauto. intros EQ; rewrite EQ in H; inv H. auto.
-  + simpl in H3. exploit A; eauto. intros EQ; rewrite EQ in H; inv H. auto.
-  + simpl in H3. exists b1; split; eauto.
-  + simpl; unfold Genv.block_is_volatile.
-    destruct (Genv.find_var_info ge b1) as [gv1|] eqn:V1.
-    * exploit B; eauto. intros EQ; rewrite EQ in H; inv H. rewrite V1; auto.
-    * destruct (Genv.find_var_info ge b2) as [gv2|] eqn:V2; auto.
-      exploit C; eauto. intros EQ; subst b2. congruence.
+  intros. eapply external_call_mem_inject_gen with (ge1 := ge); eauto using Genv.senv_inject.
 Qed.
 
 (** Corollaries of [external_call_determ]. *)
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index c4a03c39d..1b130ff74 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -129,6 +129,22 @@ Definition equiv (se1 se2: t) : Prop :=
   /\ (forall id, public_symbol se2 id = public_symbol se1 id)
   /\ (forall b, block_is_volatile se2 b = block_is_volatile se1 b).
 
+(** Compatibility with a memory injection.  *)
+
+Record inject (f: meminj) (se1 se2: t) : Prop := {
+  public_symbol_inject: forall id,
+    Senv.public_symbol se2 id = Senv.public_symbol se1 id;
+  find_symbol_inject: forall id b1 b2 delta,
+     f b1 = Some(b2, delta) -> Senv.find_symbol se1 id = Some b1 ->
+     delta = 0 /\ Senv.find_symbol se2 id = Some b2;
+  find_public_symbol_inject: forall id b1,
+     Senv.public_symbol se1 id = true -> Senv.find_symbol se1 id = Some b1 ->
+     exists b2, f b1 = Some(b2, 0) /\ Senv.find_symbol se2 id = Some b2;
+  block_is_volatile_inject: forall b1 b2 delta,
+     f b1 = Some(b2, delta) ->
+     Senv.block_is_volatile se2 b2 = Senv.block_is_volatile se1 b1
+}.
+
 End Senv.
 
 Module Genv.
@@ -606,6 +622,78 @@ Definition to_senv (ge: t) : Senv.t :=
     ge.(genv_symb_range)
     (block_is_volatile_below ge).
 
+(** ** Compatibility with memory injections *)
+
+Definition inject (f: meminj) (ge: t) : Prop :=
+     (forall b, Plt b ge.(genv_next) -> f b = Some(b, 0))
+  /\ (forall b b' delta,
+        f b = Some(b', delta) -> Plt b' ge.(genv_next) -> b' = b /\ delta = 0).
+
+Lemma senv_inject: forall f ge,
+  inject f ge -> Senv.inject f (to_senv ge) (to_senv ge).
+Proof.
+  intros f ge [A B]. constructor; intros.
+- auto.
+- assert (f b1 = Some(b1, 0)). { apply ge.(genv_symb_range) in H0. auto. }
+  rewrite H in H1; inv H1. auto.
+- exists b1; split. 
+  apply ge.(genv_symb_range) in H0. auto.
+  auto.
+- simpl. destruct (block_is_volatile ge b1) eqn:V1; [ | destruct (block_is_volatile ge b2) eqn:V2 ]; auto.
+  + assert (f b1 = Some(b1, 0)). { apply block_is_volatile_below in V1. auto. }
+    congruence.
+  + exploit B; eauto using block_is_volatile_below.
+    intros [C D]. congruence.
+Qed.
+
+Lemma find_symbol_inject: forall f ge id b,
+  inject f ge -> find_symbol ge id = Some b -> f b = Some(b, 0).
+Proof.
+  intros until b; intros [A B] FIND.
+  apply ge.(genv_symb_range) in FIND. auto.
+Qed.
+
+Lemma symbol_address_inject: forall f ge id ofs,
+  inject f ge ->
+  Val.inject f (symbol_address ge id ofs) (symbol_address ge id ofs).
+Proof.
+  unfold symbol_address; intros. destruct (find_symbol ge id) eqn:FIND; auto.
+  econstructor. eapply find_symbol_inject; eauto. rewrite Ptrofs.add_zero; auto.
+Qed.
+
+Lemma find_funct_ptr_inject: forall f ge b fd,
+  inject f ge -> find_funct_ptr ge b = Some fd -> f b = Some(b, 0).
+Proof.
+  intros until fd; intros [A B] FIND. unfold find_funct_ptr, find_def in FIND.
+  destruct (ge.(genv_defs)!b) as [gd|] eqn: FIND'; try discriminate.
+  apply ge.(genv_defs_range) in FIND'. auto.
+Qed.
+
+Lemma find_funct_inject: forall f ge v v' fd,
+  inject f ge -> find_funct ge v = Some fd -> Val.inject f v v' -> v' = v.
+Proof.
+  intros. exploit find_funct_inv; eauto. intros (b & EQ). subst v.
+  rewrite find_funct_find_funct_ptr in H0.
+  exploit find_funct_ptr_inject; eauto. intros EQ'.
+  inv H1. rewrite EQ' in H4; inv H4. reflexivity.
+Qed.
+
+Lemma find_var_info_inject: forall f ge b vi,
+  inject f ge -> find_var_info ge b = Some vi -> f b = Some(b, 0).
+Proof.
+  intros until vi; intros [A B] FIND. unfold find_var_info, find_def in FIND.
+  destruct (ge.(genv_defs)!b) as [gd|] eqn: FIND'; try discriminate.
+  apply ge.(genv_defs_range) in FIND'. auto.
+Qed.
+
+Lemma init_inject: forall ge,
+  inject (Mem.flat_inj ge.(genv_next)) ge.
+Proof.
+  unfold Mem.flat_inj; intros; split; intros.
+- apply pred_dec_true; auto.
+- destruct plt in H; inv H. auto.
+Qed.
+
 (** * Construction of the initial memory state *)
 
 Section INITMEM.
@@ -1449,6 +1537,13 @@ Proof.
   apply Ple_refl.
 Qed.
 
+Theorem initmem_inject_genv: forall p m,
+  init_mem p = Some m ->
+  inject (Mem.flat_inj (Mem.nextblock m)) (globalenv p).
+Proof.
+  intros. apply init_mem_genv_next in H. rewrite <- H. apply init_inject.
+Qed.
+
 (** ** Sufficient and necessary conditions for the initial memory to exist. *)
 
 (** Alignment properties *)
diff --git a/common/Separation.v b/common/Separation.v
index 465adfa48..860132ae4 100644
--- a/common/Separation.v
+++ b/common/Separation.v
@@ -804,20 +804,12 @@ Qed.
 
 (** Preservation of a global environment by a memory injection *)
 
-Inductive globalenv_preserved {F V: Type} (ge: Genv.t F V) (j: meminj) (bound: block) : Prop :=
-  | globalenv_preserved_intro
-      (DOMAIN: forall b, Plt b bound -> j b = Some(b, 0))
-      (IMAGE: forall b1 b2 delta, j b1 = Some(b2, delta) -> Plt b2 bound -> b1 = b2)
-      (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> Plt b bound)
-      (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> Plt b bound)
-      (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> Plt b bound).
-
 Program Definition globalenv_inject {F V: Type} (ge: Genv.t F V) (j: meminj) : massert := {|
-  m_pred := fun m => exists bound, Ple bound (Mem.nextblock m) /\ globalenv_preserved ge j bound;
+  m_pred := fun m => Ple (Genv.genv_next ge) (Mem.nextblock m) /\ Genv.inject j ge;
   m_footprint := fun b ofs => False
 |}.
 Next Obligation.
-  rename H into bound. exists bound; split; auto. eapply Ple_trans; eauto. eapply Mem.unchanged_on_nextblock; eauto.
+  split; auto. eapply Ple_trans; eauto. eapply Mem.unchanged_on_nextblock; eauto.
 Qed.
 Next Obligation.
   tauto.
@@ -826,13 +818,9 @@ Qed.
 Lemma globalenv_inject_preserves_globals:
   forall (F V: Type) (ge: Genv.t F V) j m,
   m |= globalenv_inject ge j ->
-  meminj_preserves_globals ge j.
+  Genv.inject j ge.
 Proof.
-  intros. destruct H as (bound & A & B). destruct B.
-  split; [|split]; intros.
-- eauto.
-- eauto.
-- symmetry; eauto.
+  intros. destruct H as (A & B). auto.
 Qed.
 
 Lemma globalenv_inject_incr:
@@ -842,17 +830,14 @@ Lemma globalenv_inject_incr:
   m |= globalenv_inject ge j ** P ->
   m |= globalenv_inject ge j' ** P.
 Proof.
-  intros. destruct H1 as (A & B & C). destruct A as (bound & D & E).
+  intros. destruct H1 as ((D & E) & B & C).
   split; [|split]; auto.
-  exists bound; split; auto.
-  inv E; constructor; intros.
-- eauto.
-- destruct (j b1) as [[b0 delta0]|] eqn:JB1.
+  split; auto.
+  destruct E as [E1 E2]; split; intros.
+- apply H. auto.
+- destruct (j b) as [[b0 delta0]|] eqn:JB.
 + erewrite H in H1 by eauto. inv H1. eauto.
-+ exploit H0; eauto. intros (X & Y). elim Y. apply Pos.lt_le_trans with bound; auto.
-- eauto.
-- eauto.
-- eauto.
++ exploit H0; eauto. intros (X & Y). elim Y. apply Pos.lt_le_trans with (Genv.genv_next ge); auto.
 Qed.
 
 Lemma external_call_parallel_rule:
diff --git a/common/Values.v b/common/Values.v
index 59d851305..0dd8b1ec1 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -2355,6 +2355,12 @@ Qed.
 
 Global Hint Resolve inject_ptrofs : core.
 
+Lemma inject_ptr_flat:
+  forall (mi: meminj) b b' ofs, mi b = Some(b', 0) -> inject mi (Vptr b ofs) (Vptr b' ofs).
+Proof.
+  intros. econstructor; eauto. rewrite Ptrofs.add_zero; auto.
+Qed.
+
 Section VAL_INJ_OPS.
 
 Variable f: meminj.
diff --git a/powerpc/Op.v b/powerpc/Op.v
index c74ccd8b7..a0e4f1810 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -1131,20 +1131,12 @@ Section EVAL_INJECT.
 Variable F V: Type.
 Variable genv: Genv.t F V.
 Variable f: meminj.
-Hypothesis globals: meminj_preserves_globals genv f.
+Hypothesis globals: Genv.inject f genv.
 Variable sp1: block.
 Variable sp2: block.
 Variable delta: Z.
 Hypothesis sp_inj: f sp1 = Some(sp2, delta).
 
-Remark symbol_address_inject:
-  forall id ofs, Val.inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs).
-Proof.
-  intros. unfold Genv.symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto.
-  exploit (proj1 globals); eauto. intros.
-  econstructor; eauto. rewrite Ptrofs.add_zero; auto.
-Qed.
-
 Lemma eval_condition_inject:
   forall cond vl1 vl2 b m1 m2,
   Val.inject_list f vl1 vl2 ->
@@ -1169,8 +1161,7 @@ Lemma eval_addressing_inject:
 Proof.
   intros.
   rewrite eval_shift_stack_addressing.
-  eapply eval_addressing_inj with (sp1 := Vptr sp1 Ptrofs.zero); eauto.
-  intros. apply symbol_address_inject.
+  eapply eval_addressing_inj with (sp1 := Vptr sp1 Ptrofs.zero); eauto using Genv.symbol_address_inject.
   econstructor; eauto. rewrite Ptrofs.add_zero_l; auto.
 Qed.
 
@@ -1185,12 +1176,11 @@ Lemma eval_operation_inject:
 Proof.
   intros.
   rewrite eval_shift_stack_operation. simpl.
-  eapply eval_operation_inj with (sp1 := Vptr sp1 Ptrofs.zero) (m1 := m1); eauto.
+  eapply eval_operation_inj with (sp1 := Vptr sp1 Ptrofs.zero) (m1 := m1); eauto using Genv.symbol_address_inject.
   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.
   econstructor; eauto. rewrite Ptrofs.add_zero_l; auto.
 Qed.
 
diff --git a/riscV/Op.v b/riscV/Op.v
index 333d166c6..fdaba86c4 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -1299,20 +1299,12 @@ Section EVAL_INJECT.
 Variable F V: Type.
 Variable genv: Genv.t F V.
 Variable f: meminj.
-Hypothesis globals: meminj_preserves_globals genv f.
+Hypothesis globals: Genv.inject f genv.
 Variable sp1: block.
 Variable sp2: block.
 Variable delta: Z.
 Hypothesis sp_inj: f sp1 = Some(sp2, delta).
 
-Remark symbol_address_inject:
-  forall id ofs, Val.inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs).
-Proof.
-  intros. unfold Genv.symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto.
-  exploit (proj1 globals); eauto. intros.
-  econstructor; eauto. rewrite Ptrofs.add_zero; auto.
-Qed.
-
 Lemma eval_condition_inject:
   forall cond vl1 vl2 b m1 m2,
   Val.inject_list f vl1 vl2 ->
@@ -1337,8 +1329,7 @@ Lemma eval_addressing_inject:
 Proof.
   intros.
   rewrite eval_shift_stack_addressing.
-  eapply eval_addressing_inj with (sp1 := Vptr sp1 Ptrofs.zero); eauto.
-  intros. apply symbol_address_inject.
+  eapply eval_addressing_inj with (sp1 := Vptr sp1 Ptrofs.zero); eauto using Genv.symbol_address_inject.
   econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. 
 Qed.
 
@@ -1353,12 +1344,11 @@ Lemma eval_operation_inject:
 Proof.
   intros.
   rewrite eval_shift_stack_operation. simpl.
-  eapply eval_operation_inj with (sp1 := Vptr sp1 Ptrofs.zero) (m1 := m1); eauto.
+  eapply eval_operation_inj with (sp1 := Vptr sp1 Ptrofs.zero) (m1 := m1); eauto using Genv.symbol_address_inject.
   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.
   econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. 
 Qed.
 
diff --git a/x86/Op.v b/x86/Op.v
index fde078dc9..3c139f1a0 100644
--- a/x86/Op.v
+++ b/x86/Op.v
@@ -1470,20 +1470,12 @@ Section EVAL_INJECT.
 Variable F V: Type.
 Variable genv: Genv.t F V.
 Variable f: meminj.
-Hypothesis globals: meminj_preserves_globals genv f.
+Hypothesis globals: Genv.inject f genv.
 Variable sp1: block.
 Variable sp2: block.
 Variable delta: Z.
 Hypothesis sp_inj: f sp1 = Some(sp2, delta).
 
-Remark symbol_address_inject:
-  forall id ofs, Val.inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs).
-Proof.
-  intros. unfold Genv.symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto.
-  exploit (proj1 globals); eauto. intros.
-  econstructor; eauto. rewrite Ptrofs.add_zero; auto.
-Qed.
-
 Lemma eval_condition_inject:
   forall cond vl1 vl2 b m1 m2,
   Val.inject_list f vl1 vl2 ->
@@ -1508,8 +1500,7 @@ Lemma eval_addressing_inject:
 Proof.
   intros.
   rewrite eval_shift_stack_addressing.
-  eapply eval_addressing_inj with (sp1 := Vptr sp1 Ptrofs.zero); eauto.
-  intros. apply symbol_address_inject.
+  eapply eval_addressing_inj with (sp1 := Vptr sp1 Ptrofs.zero); eauto using Genv.symbol_address_inject.
   econstructor; eauto. rewrite Ptrofs.add_zero_l; auto.
 Qed.
 
@@ -1524,12 +1515,11 @@ Lemma eval_operation_inject:
 Proof.
   intros.
   rewrite eval_shift_stack_operation. simpl.
-  eapply eval_operation_inj with (sp1 := Vptr sp1 Ptrofs.zero) (m1 := m1); eauto.
+  eapply eval_operation_inj with (sp1 := Vptr sp1 Ptrofs.zero) (m1 := m1); eauto using Genv.symbol_address_inject.
   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.
   econstructor; eauto. rewrite Ptrofs.add_zero_l; auto.
 Qed.