diff --git a/Makefile b/Makefile
index 0247b6889e..394ba54000 100644
--- a/Makefile
+++ b/Makefile
@@ -63,7 +63,7 @@ VLIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \
 # Parts common to the front-ends and the back-end (in common/)
 
 COMMON=Errors.v AST.v Linking.v \
-  Events.v Globalenvs.v Memdata.v Memtype.v Memory.v \
+  Events.v Globalenvs.v Memdata.v Memtype.v Memory.v BlockNames.v \
   Values.v Smallstep.v Behaviors.v Switch.v Determinism.v Unityping.v \
   Separation.v
 
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v
index 199ac92262..fbf0cd4647 100644
--- a/backend/Deadcodeproof.v
+++ b/backend/Deadcodeproof.v
@@ -48,8 +48,8 @@ Record magree (m1 m2: mem) (P: locset) : Prop := mk_magree {
     forall b ofs,
     Mem.perm m1 b ofs Cur Readable ->
     P b ofs ->
-    memval_lessdef (ZMap.get ofs (PMap.get b (Mem.mem_contents m1)))
-                   (ZMap.get ofs (PMap.get b (Mem.mem_contents m2)));
+    memval_lessdef (ZMap.get ofs (BMap.get b (Mem.mem_contents m1)))
+                   (ZMap.get ofs (BMap.get b (Mem.mem_contents m2)));
   ma_nextblock:
     Mem.nextblock m2 = Mem.nextblock m1
 }.
@@ -165,7 +165,7 @@ Proof.
   intuition eauto using Mem.perm_storebytes_1, Mem.perm_storebytes_2.
 - rewrite (Mem.storebytes_mem_contents _ _ _ _ _ H0).
   rewrite (Mem.storebytes_mem_contents _ _ _ _ _ ST2).
-  rewrite ! PMap.gsspec. destruct (peq b0 b).
+  rewrite ! BMap.gsspec. destruct (BMap.elt_eq b0 b).
 + subst b0. apply SETN with (access := fun ofs => Mem.perm m1' b ofs Cur Readable /\ Q b ofs); auto.
   intros. destruct H5. eapply ma_memval; eauto.
   eapply Mem.perm_storebytes_2; eauto.
@@ -209,7 +209,7 @@ Proof.
 - exploit ma_perm_inv; eauto.
   intuition eauto using Mem.perm_storebytes_1, Mem.perm_storebytes_2.
 - rewrite (Mem.storebytes_mem_contents _ _ _ _ _ H0).
-  rewrite PMap.gsspec. destruct (peq b0 b).
+  rewrite BMap.gsspec. destruct (BMap.elt_eq b0 b).
 + subst b0. rewrite Mem.setN_outside. eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto.
   destruct (zlt ofs0 ofs); auto. destruct (zle (ofs + Z.of_nat (length bytes1)) ofs0); try omega.
   elim (H1 ofs0). omega. auto.
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index 2dcb895687..8483af6dc8 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -349,7 +349,7 @@ Proof.
   intros. red in SEP. destruct (F b) as [[sp1 delta1] |] eqn:?.
   exploit INCR; eauto. intros EQ; rewrite H0 in EQ; inv EQ.
   red; intros; eelim B; eauto. eapply PERM; eauto.
-  red. destruct (plt b (Mem.nextblock m1)); auto.
+  red. destruct (Block.lt_dec b (Mem.nextblock m1)); auto.
   exploit Mem.mi_freeblocks; eauto. congruence.
   exploit SEP; eauto. tauto.
 Qed.
@@ -358,11 +358,11 @@ Qed.
 
 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).
+      (DOMAIN: forall b, Block.lt b bound -> F b = Some(b, 0))
+      (IMAGE: forall b1 b2 delta, F b1 = Some(b2, delta) -> Block.lt b2 bound -> b1 = b2)
+      (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> Block.lt b bound)
+      (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> Block.lt b bound)
+      (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> Block.lt b bound).
 
 Lemma find_function_agree:
   forall ros rs fd F ctx rs' bound,
@@ -469,7 +469,7 @@ 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),
+        (BELOW: Block.le bound1 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')
@@ -481,7 +481,7 @@ Inductive match_stacks (F: meminj) (m m': mem):
         (SSZ1: 0 <= f'.(fn_stacksize) < Ptrofs.max_unsigned)
         (SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize))
         (RES: Ple res ctx.(mreg))
-        (BELOW: Plt sp' bound),
+        (BELOW: Block.lt sp' bound),
       match_stacks F m m'
                    (Stackframe res f (Vptr sp Ptrofs.zero) pc rs :: stk)
                    (Stackframe (sreg ctx res) f' (Vptr sp' Ptrofs.zero) (spc ctx pc) rs' :: stk')
@@ -492,7 +492,7 @@ Inductive match_stacks (F: meminj) (m m': mem):
         (SSZ1: 0 <= f'.(fn_stacksize) < Ptrofs.max_unsigned)
         (SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize))
         (RET: ctx.(retinfo) = Some (rpc, res))
-        (BELOW: Plt sp' bound),
+        (BELOW: Block.lt sp' bound),
       match_stacks F m m'
                    stk
                    (Stackframe res f' (Vptr sp' Ptrofs.zero) rpc rs' :: stk')
@@ -555,13 +555,13 @@ Qed.
 Lemma match_stacks_bound:
   forall stk stk' bound bound1,
   match_stacks F m m' stk stk' bound ->
-  Ple bound bound1 ->
+  Block.le bound bound1 ->
   match_stacks F m m' stk stk' bound1.
 Proof.
   intros. inv H.
-  apply match_stacks_nil with bound0. 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.
+  apply match_stacks_nil with bound0. auto. eapply Block.le_trans; eauto.
+  eapply match_stacks_cons; eauto. blomega.
+  eapply match_stacks_untailcall; eauto. blomega.
 Qed.
 
 Variable F1: meminj.
@@ -571,13 +571,13 @@ Hypothesis INCR: inject_incr F F1.
 Lemma match_stacks_invariant:
   forall stk stk' bound, match_stacks F m m' stk stk' bound ->
   forall (INJ: forall b1 b2 delta,
-               F1 b1 = Some(b2, delta) -> Plt b2 bound -> F b1 = Some(b2, delta))
+               F1 b1 = Some(b2, delta) -> Block.lt b2 bound -> F b1 = Some(b2, delta))
          (PERM1: forall b1 b2 delta ofs,
-               F1 b1 = Some(b2, delta) -> Plt b2 bound ->
+               F1 b1 = Some(b2, delta) -> Block.lt b2 bound ->
                Mem.perm m1 b1 ofs Max Nonempty -> Mem.perm m b1 ofs Max Nonempty)
-         (PERM2: forall b ofs, Plt b bound ->
+         (PERM2: forall b ofs, Block.lt b bound ->
                Mem.perm m' b ofs Cur Freeable -> Mem.perm m1' b ofs Cur Freeable)
-         (PERM3: forall b ofs k p, Plt b bound ->
+         (PERM3: forall b ofs k p, Block.lt b bound ->
                Mem.perm m1' b ofs k p -> Mem.perm m' b ofs k p),
   match_stacks F1 m1 m1' stk stk' bound
 
@@ -587,13 +587,13 @@ with match_stacks_inside_invariant:
   forall rs2
          (RS: forall r, Plt r ctx.(dreg) -> rs2#r = rs1#r)
          (INJ: forall b1 b2 delta,
-               F1 b1 = Some(b2, delta) -> Ple b2 sp' -> F b1 = Some(b2, delta))
+               F1 b1 = Some(b2, delta) -> Block.le b2 sp' -> F b1 = Some(b2, delta))
          (PERM1: forall b1 b2 delta ofs,
-               F1 b1 = Some(b2, delta) -> Ple b2 sp' ->
+               F1 b1 = Some(b2, delta) -> Block.le b2 sp' ->
                Mem.perm m1 b1 ofs Max Nonempty -> Mem.perm m b1 ofs Max Nonempty)
-         (PERM2: forall b ofs, Ple b sp' ->
+         (PERM2: forall b ofs, Block.le b sp' ->
                Mem.perm m' b ofs Cur Freeable -> Mem.perm m1' b ofs Cur Freeable)
-         (PERM3: forall b ofs k p, Ple b sp' ->
+         (PERM3: forall b ofs k p, Block.le b sp' ->
                Mem.perm m1' b ofs k p -> Mem.perm m' b ofs k p),
   match_stacks_inside F1 m1 m1' stk stk' f' ctx sp' rs2.
 
@@ -602,34 +602,22 @@ Proof.
   (* 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.
+  intros. apply IMAGE with delta. eapply INJ; eauto. blomega. blomega.
+  auto.
   (* cons *)
   apply match_stacks_cons with (fenv := fenv) (ctx := ctx); auto.
-  eapply match_stacks_inside_invariant; eauto.
-  intros; eapply INJ; eauto; xomega.
-  intros; eapply PERM1; eauto; xomega.
-  intros; eapply PERM2; eauto; xomega.
-  intros; eapply PERM3; eauto; xomega.
+  eapply match_stacks_inside_invariant; eauto; blomega.
   eapply agree_regs_incr; eauto.
   eapply range_private_invariant; eauto.
   (* untailcall *)
   apply match_stacks_untailcall with (ctx := ctx); auto.
-  eapply match_stacks_inside_invariant; eauto.
-  intros; eapply INJ; eauto; xomega.
-  intros; eapply PERM1; eauto; xomega.
-  intros; eapply PERM2; eauto; xomega.
-  intros; eapply PERM3; eauto; xomega.
+  eapply match_stacks_inside_invariant; eauto; blomega.
   eapply range_private_invariant; eauto.
 
   induction 1; intros.
   (* base *)
   eapply match_stacks_inside_base; eauto.
-  eapply match_stacks_invariant; eauto.
-  intros; eapply INJ; eauto; xomega.
-  intros; eapply PERM1; eauto; xomega.
-  intros; eapply PERM2; eauto; xomega.
-  intros; eapply PERM3; eauto; xomega.
+  eapply match_stacks_invariant; eauto; blomega.
   (* inlined *)
   apply match_stacks_inside_inlined with (fenv := fenv) (ctx' := ctx'); auto.
   apply IHmatch_stacks_inside; auto.
@@ -637,9 +625,7 @@ Proof.
   apply agree_regs_incr with F; auto.
   apply agree_regs_invariant with rs'; auto.
   intros. apply RS. red in BELOW. xomega.
-  eapply range_private_invariant; eauto.
-    intros. split. eapply INJ; eauto. xomega. eapply PERM1; eauto. xomega.
-    intros. eapply PERM2; eauto. xomega.
+  eapply range_private_invariant; eauto; blomega.
 Qed.
 
 Lemma match_stacks_empty:
@@ -711,10 +697,10 @@ Proof.
   eapply match_stacks_inside_base; eauto.
   eapply match_stacks_invariant; eauto.
   intros. destruct (eq_block b1 b).
-  subst b1. rewrite H1 in H4; inv H4. eelim Plt_strict; eauto.
+  subst b1. rewrite H1 in H4; inv H4. eelim Block.lt_strict; eauto.
   rewrite H2 in H4; auto.
   intros. exploit Mem.perm_alloc_inv; eauto. destruct (eq_block b1 b); intros; auto.
-  subst b1. rewrite H1 in H4. inv H4. eelim Plt_strict; eauto.
+  subst b1. rewrite H1 in H4. inv H4. eelim Block.lt_strict; eauto.
   (* inlined *)
   eapply match_stacks_inside_inlined; eauto.
   eapply IHmatch_stacks_inside; eauto. destruct SBELOW. omega.
@@ -744,7 +730,7 @@ Lemma match_stacks_free_right:
   match_stacks F m m1' stk stk' sp.
 Proof.
   intros. eapply match_stacks_invariant; eauto.
-  intros. eapply Mem.perm_free_1; eauto.
+  intros. eapply Mem.perm_free_1; eauto. blomega.
   intros. eapply Mem.perm_free_3; eauto.
 Qed.
 
@@ -790,12 +776,12 @@ Hypothesis SEP: inject_separated F1 F2 m1 m1'.
 Lemma match_stacks_extcall:
   forall stk stk' bound,
   match_stacks F1 m1 m1' stk stk' bound ->
-  Ple bound (Mem.nextblock m1') ->
+  Block.le bound (Mem.nextblock m1') ->
   match_stacks F2 m2 m2' stk stk' bound
 with match_stacks_inside_extcall:
   forall stk stk' f' ctx sp' rs',
   match_stacks_inside F1 m1 m1' stk stk' f' ctx sp' rs' ->
-  Plt sp' (Mem.nextblock m1') ->
+  Block.lt sp' (Mem.nextblock m1') ->
   match_stacks_inside F2 m2 m2' stk stk' f' ctx sp' rs'.
 Proof.
   induction 1; intros.
@@ -803,19 +789,19 @@ Proof.
     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.
-    exploit SEP; eauto. intros [A B]. elim B. red. xomega.
+    exploit SEP; eauto. intros [A B]. elim B. red. blomega.
   eapply match_stacks_cons; eauto.
-    eapply match_stacks_inside_extcall; eauto. xomega.
+    eapply match_stacks_inside_extcall; eauto. blomega.
     eapply agree_regs_incr; eauto.
-    eapply range_private_extcall; eauto. red; xomega.
-    intros. apply SSZ2; auto. apply MAXPERM'; auto. red; xomega.
+    eapply range_private_extcall; eauto. red. blomega.
+    intros. apply SSZ2; auto. apply MAXPERM'; auto. red. blomega.
   eapply match_stacks_untailcall; eauto.
-    eapply match_stacks_inside_extcall; eauto. xomega.
-    eapply range_private_extcall; eauto. red; xomega.
-    intros. apply SSZ2; auto. apply MAXPERM'; auto. red; xomega.
+    eapply match_stacks_inside_extcall; eauto. blomega.
+    eapply range_private_extcall; eauto. red. blomega.
+    intros. apply SSZ2; auto. apply MAXPERM'; auto. red. blomega.
   induction 1; intros.
   eapply match_stacks_inside_base; eauto.
-    eapply match_stacks_extcall; eauto. xomega.
+    eapply match_stacks_extcall; eauto. blomega.
   eapply match_stacks_inside_inlined; eauto.
     eapply agree_regs_incr; eauto.
     eapply range_private_extcall; eauto.
@@ -1043,9 +1029,9 @@ Proof.
   eapply match_stacks_bound with (bound := sp').
   eapply match_stacks_invariant; eauto.
     intros. eapply Mem.perm_free_3; eauto.
-    intros. eapply Mem.perm_free_1; eauto.
-    intros. eapply Mem.perm_free_3; eauto.
-  erewrite Mem.nextblock_free; eauto. red in VB; xomega.
+    intros. eapply Mem.perm_free_1; eauto; blomega.
+    intros. eapply Mem.perm_free_3; eauto. 
+  erewrite Mem.nextblock_free; eauto. blomega.
   eapply agree_val_regs; eauto.
   eapply Mem.free_right_inject; eauto. eapply Mem.free_left_inject; eauto.
   (* show that no valid location points into the stack block being freed *)
@@ -1135,9 +1121,9 @@ Proof.
   eapply match_stacks_bound with (bound := sp').
   eapply match_stacks_invariant; eauto.
     intros. eapply Mem.perm_free_3; eauto.
-    intros. eapply Mem.perm_free_1; eauto.
+    intros. eapply Mem.perm_free_1; eauto. blomega.
     intros. eapply Mem.perm_free_3; eauto.
-  erewrite Mem.nextblock_free; eauto. red in VB; xomega.
+  erewrite Mem.nextblock_free; eauto. blomega.
   destruct or; simpl. apply agree_val_reg; auto. auto.
   eapply Mem.free_right_inject; eauto. eapply Mem.free_left_inject; eauto.
   (* show that no valid location points into the stack block being freed *)
@@ -1175,15 +1161,15 @@ Proof.
   rewrite <- SP in MS0.
   eapply match_stacks_invariant; eauto.
     intros. destruct (eq_block b1 stk).
-    subst b1. rewrite D in H8; inv H8. eelim Plt_strict; eauto.
+    subst b1. rewrite D in H8; inv H8. eelim Block.lt_strict; eauto.
     rewrite E in H8; auto.
     intros. exploit Mem.perm_alloc_inv. eexact H. eauto.
     destruct (eq_block b1 stk); intros; auto.
-    subst b1. rewrite D in H8; inv H8. eelim Plt_strict; eauto.
+    subst b1. rewrite D in H8; inv H8. eelim Block.lt_strict; eauto.
     intros. eapply Mem.perm_alloc_1; eauto.
     intros. exploit Mem.perm_alloc_inv. eexact A. eauto.
     rewrite dec_eq_false; auto.
-  auto. auto. auto. eauto. auto.
+  blomega. auto. auto. eauto. auto.
   rewrite H5. apply agree_regs_init_regs. eauto. auto. inv H1; auto. congruence. auto.
   eapply Mem.valid_new_block; eauto.
   red; intros. split.
@@ -1245,7 +1231,7 @@ Proof.
     eapply match_stacks_extcall with (F1 := F) (F2 := F1) (m1 := m) (m1' := m'0); eauto.
     intros; eapply external_call_max_perm; eauto.
     intros; eapply external_call_max_perm; eauto.
-    xomega.
+    blomega.
     eapply external_call_nextblock; eauto.
     auto. auto.
 
@@ -1302,11 +1288,12 @@ Proof.
   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.
+    unfold Mem.flat_inj in H. destruct (Block.lt_dec 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.
+    blomega.
+  erewrite <- Genv.init_mem_genv_next; eauto.
   eapply Genv.initmem_inject; eauto.
 Qed.
 
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index ffd9b2278d..71f5529c82 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -2116,11 +2116,11 @@ Proof.
   constructor. red; intros. rewrite H3, loc_arguments_main in H. contradiction.
   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. erewrite <- Genv.init_mem_genv_next; eauto. eapply Genv.initmem_inject; eauto.
+  simpl. exists (Mem.nextblock m0); split. apply Block.le_refl.
   unfold j, Mem.flat_inj; constructor; intros.
     apply pred_dec_true; auto.
-    destruct (plt b1 (Mem.nextblock m0)); congruence.
+    destruct (Block.lt_dec 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.
diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v
index 7899a04cc9..5a9721f565 100644
--- a/backend/Unusedglobproof.v
+++ b/backend/Unusedglobproof.v
@@ -682,15 +682,15 @@ Inductive match_stacks (j: meminj):
         list stackframe -> list stackframe -> block -> block -> Prop :=
   | match_stacks_nil: forall bound tbound,
       meminj_preserves_globals j ->
-      Ple (Genv.genv_next ge) bound -> Ple (Genv.genv_next tge) tbound ->
+      Block.le Block.init bound -> Block.le Block.init tbound ->
       match_stacks j nil nil bound tbound
   | match_stacks_cons: forall res f sp pc rs s tsp trs ts bound tbound
          (STACKS: match_stacks j s ts sp tsp)
          (KEPT: forall id, ref_function f id -> kept id)
          (SPINJ: j sp = Some(tsp, 0))
          (REGINJ: regset_inject j rs trs)
-         (BELOW: Plt sp bound)
-         (TBELOW: Plt tsp tbound),
+         (BELOW: Block.lt sp bound)
+         (TBELOW: Block.lt tsp tbound),
       match_stacks j (Stackframe res f (Vptr sp Ptrofs.zero) pc rs :: s)
                      (Stackframe res f (Vptr tsp Ptrofs.zero) pc trs :: ts)
                      bound tbound.
@@ -707,22 +707,22 @@ Lemma match_stacks_incr:
   forall j j', inject_incr j j' ->
   forall s ts bound tbound, match_stacks j s ts bound tbound ->
   (forall b1 b2 delta,
-      j b1 = None -> j' b1 = Some(b2, delta) -> Ple bound b1 /\ Ple tbound b2) ->
+      j b1 = None -> j' b1 = Some(b2, delta) -> Block.le bound b1 /\ Block.le tbound b2) ->
   match_stacks j' s ts bound tbound.
 Proof.
   induction 2; intros.
-- assert (SAME: forall b b' delta, Plt b (Genv.genv_next ge) ->
+- assert (SAME: forall b b' delta, Block.lt b Block.init ->
                                    j' b = Some(b', delta) -> j b = Some(b', delta)).
   { intros. destruct (j b) as [[b1 delta1] | ] eqn: J.
     exploit H; eauto. congruence.
-    exploit H3; eauto. intros [A B]. elim (Plt_strict b).
-    eapply Plt_Ple_trans. eauto. eapply Ple_trans; eauto. }
-  assert (SAME': forall b b' delta, Plt b' (Genv.genv_next tge) ->
+    exploit H3; eauto. intros [A B]. elim (Block.lt_strict b).
+    eapply Block.lt_le_trans. eauto. eapply Block.le_trans. apply H1. eauto. }
+  assert (SAME': forall b b' delta, Block.lt b' Block.init ->
                                    j' b = Some(b', delta) -> j b = Some (b', delta)).
   { intros. destruct (j b) as [[b1 delta1] | ] eqn: J.
     exploit H; eauto. congruence.
-    exploit H3; eauto. intros [A B]. elim (Plt_strict b').
-    eapply Plt_Ple_trans. eauto. eapply Ple_trans; eauto. }
+    exploit H3; eauto. intros [A B]. elim (Block.lt_strict b').
+    eapply Block.lt_le_trans. eauto. eapply Block.le_trans; eauto. }
   constructor; auto.  constructor; intros.
   + exploit symbols_inject_1; eauto. apply SAME; auto.
     eapply Genv.genv_symb_range; eauto.
@@ -736,20 +736,20 @@ Proof.
     eapply Genv.genv_defs_range; eauto.
 - econstructor; eauto.
   apply IHmatch_stacks.
-  intros. exploit H1; eauto. intros [A B]. split; eapply Ple_trans; eauto.
-  apply Plt_Ple; auto. apply Plt_Ple; auto.
+  intros. exploit H1; eauto. intros [A B]. split; eapply Block.le_trans; eauto.
+  blomega. blomega.
   apply regset_inject_incr with j; auto.
 Qed.
 
 Lemma match_stacks_bound:
   forall j s ts bound tbound bound' tbound',
   match_stacks j s ts bound tbound ->
-  Ple bound bound' -> Ple tbound tbound' ->
+  Block.le bound bound' -> Block.le tbound tbound' ->
   match_stacks j s ts bound' tbound'.
 Proof.
   induction 1; intros.
-- constructor; auto. eapply Ple_trans; eauto. eapply Ple_trans; eauto.
-- econstructor; eauto. eapply Plt_Ple_trans; eauto. eapply Plt_Ple_trans; eauto.
+- constructor; auto. eapply Block.le_trans with bound; eauto. eapply Block.le_trans with tbound; eauto.
+- econstructor; eauto; blomega.
 Qed.
 
 Inductive match_states: state -> state -> Prop :=
@@ -961,9 +961,9 @@ Proof.
   eapply exec_Itailcall; eauto.
   econstructor; eauto.
   apply match_stacks_bound with stk tsp; auto.
-  apply Plt_Ple.
+  apply Block.lt_le.
   change (Mem.valid_block m' stk). eapply Mem.valid_block_inject_1; eauto.
-  apply Plt_Ple.
+  apply Block.lt_le.
   change (Mem.valid_block tm' tsp). eapply Mem.valid_block_inject_2; eauto.
   apply regs_inject; auto.
 
@@ -982,7 +982,9 @@ Proof.
   intros. exploit G; eauto. intros [U V].
   assert (Mem.valid_block m sp0) by (eapply Mem.valid_block_inject_1; eauto).
   assert (Mem.valid_block tm tsp) by (eapply Mem.valid_block_inject_2; eauto).
-  unfold Mem.valid_block in *; xomega.
+  unfold Mem.valid_block in *.
+  split; eapply Block.lt_le, Block.lt_le_trans; eauto.
+  apply Block.nlt_le; auto. apply Block.nlt_le; auto.
   apply set_res_inject; auto. apply regset_inject_incr with j; auto.
 
 - (* cond *)
@@ -1004,9 +1006,9 @@ Proof.
   eapply exec_Ireturn; eauto.
   econstructor; eauto.
   apply match_stacks_bound with stk tsp; auto.
-  apply Plt_Ple.
+  apply Block.lt_le.
   change (Mem.valid_block m' stk). eapply Mem.valid_block_inject_1; eauto.
-  apply Plt_Ple.
+  apply Block.lt_le.
   change (Mem.valid_block tm' tsp). eapply Mem.valid_block_inject_2; eauto.
   destruct or; simpl; auto.
 
@@ -1019,7 +1021,7 @@ Proof.
   { rewrite STK, TSTK.
     apply match_stacks_incr with j; auto.
     intros. destruct (eq_block b1 stk).
-    subst b1. rewrite F in H1; inv H1. split; apply Ple_refl.
+    subst b1. rewrite F in H1; inv H1. split; apply Block.le_refl.
     rewrite G in H1 by auto. congruence. }
   econstructor; split.
   eapply exec_function_internal; eauto.
@@ -1036,7 +1038,8 @@ Proof.
   apply match_stacks_bound with (Mem.nextblock m) (Mem.nextblock tm).
   apply match_stacks_incr with j; auto.
   intros. exploit G; eauto. intros [P Q].
-  unfold Mem.valid_block in *; xomega.
+  unfold Mem.valid_block in *.
+  split; apply Block.nlt_le; auto.
   eapply external_call_nextblock; eauto.
   eapply external_call_nextblock; eauto.
 
@@ -1051,17 +1054,17 @@ Qed.
 (*
 Remark genv_find_def_exists:
   forall (F V: Type) (p: AST.program F V) b,
-  Plt b (Genv.genv_next (Genv.globalenv p)) ->
+  Block.lt b (Genv.genv_next (Genv.globalenv p)) ->
   exists gd, Genv.find_def (Genv.globalenv p) b = Some gd.
 Proof.
   intros until b.
   set (P := fun (g: Genv.t F V) =>
-        Plt b (Genv.genv_next g) -> exists gd, (Genv.genv_defs g)!b = Some gd).
+        Block.lt b (Genv.genv_next g) -> exists gd, (Genv.genv_defs g)!b = Some gd).
   assert (forall l g, P g -> P (Genv.add_globals g l)).
   { induction l as [ | [id1 g1] l]; simpl; intros.
   - auto.
-  - apply IHl. unfold Genv.add_global, P; simpl. intros LT. apply Plt_succ_inv in LT. destruct LT.
-  + rewrite PTree.gso. apply H; auto. apply Plt_ne; auto.
+  - apply IHl. unfold Genv.add_global, P; simpl. intros LT. apply Block.lt_succ_inv in LT. destruct LT.
+  + rewrite PTree.gso. apply H; auto. apply Block.lt_ne; auto.
   + rewrite H0. rewrite PTree.gss. exists g1; auto. }
   apply H. red; simpl; intros. exfalso; xomega.
 Qed.
@@ -1241,8 +1244,8 @@ Proof.
   fold tge. erewrite match_prog_main by eauto. auto.
   econstructor; eauto.
   constructor. auto.
-  erewrite <- Genv.init_mem_genv_next by eauto. apply Ple_refl.
-  erewrite <- Genv.init_mem_genv_next by eauto. apply Ple_refl.
+  erewrite <- Genv.init_mem_genv_next by eauto. apply Block.le_refl.
+  erewrite <- Genv.init_mem_genv_next by eauto. apply Block.le_refl.
 Qed.
 
 Lemma transf_final_states:
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 1f80c293b1..bde80ea9a5 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -429,14 +429,14 @@ Theorem allocate_stack:
   /\ genv_match bc' ge
   /\ romatch bc' m' rm
   /\ mmatch bc' m' mfunction_entry
-  /\ (forall b, Plt b sp -> bc' b = bc b)
+  /\ (forall b, Block.lt b sp -> bc' b = bc b)
   /\ (forall v x, vmatch bc v x -> vmatch bc' v (Ifptr Nonstack)).
 Proof.
   intros until am; intros ALLOC GENV RO MM NOSTACK.
   exploit Mem.nextblock_alloc; eauto. intros NB.
   exploit Mem.alloc_result; eauto. intros SP.
   assert (SPINVALID: bc sp = BCinvalid).
-  { rewrite SP. eapply bc_below_invalid. apply Plt_strict. eapply mmatch_below; eauto. }
+  { rewrite SP. eapply bc_below_invalid. apply Block.lt_strict. eapply mmatch_below; eauto. }
 (* Part 1: constructing bc' *)
   set (f := fun b => if eq_block b sp then BCstack else bc b).
   assert (F_stack: forall b1 b2, f b1 = BCstack -> f b2 = BCstack -> b1 = b2).
@@ -501,10 +501,11 @@ Proof.
     eapply SM; auto. eapply mmatch_top; eauto.
   + (* below *)
     red; simpl; intros. rewrite NB. destruct (eq_block b sp).
-    subst b; rewrite SP; xomega.
-    exploit mmatch_below; eauto. xomega.
+    subst b; rewrite SP. apply Block.lt_succ.
+    exploit mmatch_below; eauto.
+    intro LT; eapply Blt_trans_succ; auto.
 - (* unchanged *)
-  simpl; intros. apply dec_eq_false. apply Plt_ne. auto.
+  simpl; intros. apply dec_eq_false. apply Blt_ne. auto.
 - (* values *)
   intros. apply vmatch_incr with bc; auto. eapply vmatch_no_stack; eauto.
 Qed.
@@ -686,10 +687,10 @@ Theorem return_from_public_call:
   bc_below caller bound ->
   callee sp = BCother ->
   caller sp = BCstack ->
-  (forall b, Plt b bound -> b <> sp -> caller b = callee b) ->
+  (forall b, Block.lt b bound -> b <> sp -> caller b = callee b) ->
   genv_match caller ge ->
   ematch caller e ae ->
-  Ple bound (Mem.nextblock m) ->
+  Block.le bound (Mem.nextblock m) ->
   vmatch callee v Vtop ->
   romatch callee m rm ->
   mmatch callee m mtop ->
@@ -702,7 +703,7 @@ Theorem return_from_public_call:
    /\ mmatch bc m mafter_public_call
    /\ genv_match bc ge
    /\ bc sp = BCstack
-   /\ (forall b, Plt b sp -> bc b = caller b).
+   /\ (forall b, Block.lt b sp -> bc b = caller b).
 Proof.
   intros until rm; intros BELOW SP1 SP2 SAME GE1 EM BOUND RESM RM MM GE2 NOSTACK.
 (* Constructing bc *)
@@ -777,7 +778,7 @@ Proof.
   simpl. apply dec_eq_true.
 - (* unchanged *)
   simpl; intros. destruct (eq_block b sp). congruence.
-  symmetry. apply SAME; auto. eapply Plt_trans. eauto. apply BELOW. congruence.
+  symmetry. apply SAME; auto. eapply Block.lt_trans. eauto. apply BELOW. congruence.
 Qed.
 
 (** Construction 5: restore the stack after a private call *)
@@ -787,11 +788,11 @@ Theorem return_from_private_call:
   bc_below caller bound ->
   callee sp = BCinvalid ->
   caller sp = BCstack ->
-  (forall b, Plt b bound -> b <> sp -> caller b = callee b) ->
+  (forall b, Block.lt b bound -> b <> sp -> caller b = callee b) ->
   genv_match caller ge ->
   ematch caller e ae ->
   bmatch caller m sp am.(am_stack) ->
-  Ple bound (Mem.nextblock m) ->
+  Block.le bound (Mem.nextblock m) ->
   vmatch callee v Vtop ->
   romatch callee m rm ->
   mmatch callee m mtop ->
@@ -804,7 +805,7 @@ Theorem return_from_private_call:
    /\ mmatch bc m (mafter_private_call am)
    /\ genv_match bc ge
    /\ bc sp = BCstack
-   /\ (forall b, Plt b sp -> bc b = caller b).
+   /\ (forall b, Block.lt b sp -> bc b = caller b).
 Proof.
   intros until am; intros BELOW SP1 SP2 SAME GE1 EM CONTENTS BOUND RESM RM MM GE2 NOSTACK.
 (* Constructing bc *)
@@ -876,7 +877,7 @@ Proof.
     apply smatch_ge with Nonstack. eapply SM. eapply mmatch_top; eauto. apply pge_lub_r.
   + (* below *)
     red; simpl; intros. destruct (eq_block b sp).
-    subst b. apply Pos.lt_le_trans with bound. apply BELOW. congruence. auto.
+    subst b. apply Block.lt_le_trans with bound. apply BELOW. congruence. auto.
     eapply mmatch_below; eauto.
 - (* genv *)
   eapply genv_match_exten; eauto.
@@ -886,7 +887,7 @@ Proof.
   simpl. apply dec_eq_true.
 - (* unchanged *)
   simpl; intros. destruct (eq_block b sp). congruence.
-  symmetry. apply SAME; auto. eapply Plt_trans. eauto. apply BELOW. congruence.
+  symmetry. apply SAME; auto. eapply Block.lt_trans. eauto. apply BELOW. congruence.
 Qed.
 
 (** Construction 6: external call *)
@@ -901,7 +902,7 @@ Theorem external_call_match:
   bc_nostack bc ->
   exists bc',
      bc_incr bc bc'
-  /\ (forall b, Plt b (Mem.nextblock m) -> bc' b = bc b)
+  /\ (forall b, Block.lt b (Mem.nextblock m) -> bc' b = bc b)
   /\ vmatch bc' vres Vtop
   /\ genv_match bc' ge
   /\ romatch bc' m' rm
@@ -919,7 +920,7 @@ Proof.
   induction vargs0; simpl; intros; constructor.
   eapply vmatch_inj; eauto. auto.
   intros (j' & vres' & m'' & EC' & IRES & IMEM & UNCH1 & UNCH2 & IINCR & ISEP).
-  assert (JBELOW: forall b, Plt b (Mem.nextblock m) -> j' b = inj_of_bc bc b).
+  assert (JBELOW: forall b, Block.lt b (Mem.nextblock m) -> j' b = inj_of_bc bc b).
   {
     intros. destruct (inj_of_bc bc b) as [[b' delta] | ] eqn:EQ.
     eapply IINCR; eauto.
@@ -927,19 +928,19 @@ Proof.
     exploit ISEP; eauto. tauto.
   }
   (* Part 2: constructing bc' from j' *)
-  set (f := fun b => if plt b (Mem.nextblock m)
+  set (f := fun b => if Block.lt_dec b (Mem.nextblock m)
                      then bc b
                      else match j' b with None => BCinvalid | Some _ => BCother end).
   assert (F_stack: forall b1 b2, f b1 = BCstack -> f b2 = BCstack -> b1 = b2).
   {
     assert (forall b, f b = BCstack -> bc b = BCstack).
-    { unfold f; intros. destruct (plt b (Mem.nextblock m)); auto. destruct (j' b); discriminate. }
+    { unfold f; intros. destruct (Block.lt_dec b (Mem.nextblock m)); auto. destruct (j' b); discriminate. }
     intros. apply (bc_stack bc); auto.
   }
   assert (F_glob: forall b1 b2 id, f b1 = BCglob id -> f b2 = BCglob id -> b1 = b2).
   {
     assert (forall b id, f b = BCglob id -> bc b = BCglob id).
-    { unfold f; intros. destruct (plt b (Mem.nextblock m)); auto. destruct (j' b); discriminate. }
+    { unfold f; intros. destruct (Block.lt_dec b (Mem.nextblock m)); auto. destruct (j' b); discriminate. }
     intros. eapply (bc_glob bc); eauto.
   }
   set (bc' := BC f F_stack F_glob). unfold f in bc'.
@@ -949,7 +950,7 @@ Proof.
   }
   assert (BC'INV: forall b, bc' b <> BCinvalid -> exists b' delta, j' b = Some(b', delta)).
   {
-    simpl; intros. destruct (plt b (Mem.nextblock m)).
+    simpl; intros. destruct (Block.lt_dec b (Mem.nextblock m)).
     exists b, 0. rewrite JBELOW by auto. apply inj_of_bc_valid; auto.
     destruct (j' b) as [[b' delta] | ].
     exists b', delta; auto.
@@ -960,7 +961,7 @@ Proof.
   assert (PMTOP: forall b b' delta ofs, j' b = Some (b', delta) -> pmatch bc' b ofs Ptop).
   {
     intros. constructor. simpl; unfold f.
-    destruct (plt b (Mem.nextblock m)).
+    destruct (Block.lt_dec b (Mem.nextblock m)).
     rewrite JBELOW in H by auto. eapply inj_of_bc_inv; eauto.
     rewrite H; congruence.
   }
@@ -990,10 +991,10 @@ Proof.
   apply genv_match_exten with bc; auto.
   simpl; intros; split; intros.
   rewrite pred_dec_true by (eapply mmatch_below; eauto with va). auto.
-  destruct (plt b (Mem.nextblock m)). auto. destruct (j' b); congruence.
+  destruct (Block.lt_dec b (Mem.nextblock m)). auto. destruct (j' b); congruence.
   simpl; intros. rewrite pred_dec_true by (eapply mmatch_below; eauto with va). auto.
 - (* romatch m' *)
-  red; simpl; intros. destruct (plt b (Mem.nextblock m)).
+  red; simpl; intros. destruct (Block.lt_dec b (Mem.nextblock m)).
   exploit RO; eauto. intros (R & P & Q).
   split; auto.
   split. apply bmatch_incr with bc; auto. apply bmatch_inv with m; auto.
@@ -1008,13 +1009,13 @@ Proof.
   + rewrite PTree.gempty in H0; discriminate.
   + apply SMTOP; auto.
   + apply SMTOP; auto.
-  + red; simpl; intros. destruct (plt b (Mem.nextblock m)).
-    eapply Pos.lt_le_trans. eauto. eapply external_call_nextblock; eauto.
+  + red; simpl; intros. destruct (Block.lt_dec b (Mem.nextblock m)).
+    eapply Block.lt_le_trans. eauto. eapply external_call_nextblock; eauto.
     destruct (j' b) as [[bx deltax] | ] eqn:J'.
     eapply Mem.valid_block_inject_1; eauto.
     congruence.
 - (* nostack *)
-  red; simpl; intros. destruct (plt b (Mem.nextblock m)).
+  red; simpl; intros. destruct (Block.lt_dec b (Mem.nextblock m)).
   apply NOSTACK; auto.
   destruct (j' b); congruence.
 - (* unmapped blocks are invariant *)
@@ -1037,11 +1038,11 @@ Inductive sound_stack: block_classification -> list stackframe -> mem -> block -
   | sound_stack_public_call:
       forall (bc: block_classification) res f sp pc e stk m bound bc' bound' ae
         (STK: sound_stack bc' stk m sp)
-        (INCR: Ple bound' bound)
+        (INCR: Block.le bound' bound)
         (BELOW: bc_below bc' bound')
         (SP: bc sp = BCother)
         (SP': bc' sp = BCstack)
-        (SAME: forall b, Plt b bound' -> b <> sp -> bc b = bc' b)
+        (SAME: forall b, Block.lt b bound' -> b <> sp -> bc b = bc' b)
         (GE: genv_match bc' ge)
         (AN: VA.ge (analyze rm f)!!pc (VA.State (AE.set res Vtop ae) mafter_public_call))
         (EM: ematch bc' e ae),
@@ -1049,11 +1050,11 @@ Inductive sound_stack: block_classification -> list stackframe -> mem -> block -
   | sound_stack_private_call:
      forall (bc: block_classification) res f sp pc e stk m bound bc' bound' ae am
         (STK: sound_stack bc' stk m sp)
-        (INCR: Ple bound' bound)
+        (INCR: Block.le bound' bound)
         (BELOW: bc_below bc' bound')
         (SP: bc sp = BCinvalid)
         (SP': bc' sp = BCstack)
-        (SAME: forall b, Plt b bound' -> b <> sp -> bc b = bc' b)
+        (SAME: forall b, Block.lt b bound' -> b <> sp -> bc b = bc' b)
         (GE: genv_match bc' ge)
         (AN: VA.ge (analyze rm f)!!pc (VA.State (AE.set res (Ifptr Nonstack) ae) (mafter_private_call am)))
         (EM: ematch bc' e ae)
@@ -1096,26 +1097,40 @@ Lemma sound_stack_ext:
   forall m' bc stk m bound,
   sound_stack bc stk m bound ->
   (forall b ofs n bytes,
-       Plt b bound -> bc b = BCinvalid -> n >= 0 ->
+       Block.lt b bound -> bc b = BCinvalid -> n >= 0 ->
        Mem.loadbytes m' b ofs n = Some bytes ->
        Mem.loadbytes m b ofs n = Some bytes) ->
   sound_stack bc stk m' bound.
 Proof.
   induction 1; intros INV.
 - constructor.
-- assert (Plt sp bound') by eauto with va.
+- assert (Block.lt sp bound') by eauto with va.
   eapply sound_stack_public_call; eauto. apply IHsound_stack; intros.
-  apply INV. xomega. rewrite SAME; auto. xomega. auto. auto.
-- assert (Plt sp bound') by eauto with va.
+  apply INV.
+  {
+    eapply Block.lt_trans. apply H1.
+    eapply Block.lt_le_trans; eauto.
+  }
+  rewrite SAME; auto.
+  eapply Block.lt_trans; eauto. blomega.
+  auto. auto.
+- assert (Block.lt sp bound') by eauto with va.
   eapply sound_stack_private_call; eauto. apply IHsound_stack; intros.
-  apply INV. xomega. rewrite SAME; auto. xomega. auto. auto.
-  apply bmatch_ext with m; auto. intros. apply INV. xomega. auto. auto. auto.
+  apply INV.
+  {
+    eapply Block.lt_trans. apply H1.
+    eapply Block.lt_le_trans; eauto.
+  }
+  rewrite SAME; eauto; blomega.
+  auto. auto.
+  apply bmatch_ext with m; auto. intros. apply INV. blomega.
+  auto. auto. auto.
 Qed.
 
 Lemma sound_stack_inv:
   forall m' bc stk m bound,
   sound_stack bc stk m bound ->
-  (forall b ofs n, Plt b bound -> bc b = BCinvalid -> n >= 0 -> Mem.loadbytes m' b ofs n = Mem.loadbytes m b ofs n) ->
+  (forall b ofs n, Block.lt b bound -> bc b = BCinvalid -> n >= 0 -> Mem.loadbytes m' b ofs n = Mem.loadbytes m b ofs n) ->
   sound_stack bc stk m' bound.
 Proof.
   intros. eapply sound_stack_ext; eauto. intros. rewrite <- H0; auto.
@@ -1163,31 +1178,31 @@ Qed.
 Lemma sound_stack_new_bound:
   forall bc stk m bound bound',
   sound_stack bc stk m bound ->
-  Ple bound bound' ->
+  Block.le bound bound' ->
   sound_stack bc stk m bound'.
 Proof.
   intros. inv H.
 - constructor.
-- eapply sound_stack_public_call with (bound' := bound'0); eauto. xomega.
-- eapply sound_stack_private_call with (bound' := bound'0); eauto. xomega.
+- eapply sound_stack_public_call with (bound' := bound'0); eauto; blomega.
+- eapply sound_stack_private_call with (bound' := bound'0); eauto; blomega.
 Qed.
 
 Lemma sound_stack_exten:
   forall bc stk m bound (bc1: block_classification),
   sound_stack bc stk m bound ->
-  (forall b, Plt b bound -> bc1 b = bc b) ->
+  (forall b, Block.lt b bound -> bc1 b = bc b) ->
   sound_stack bc1 stk m bound.
 Proof.
   intros. inv H.
 - constructor.
-- assert (Plt sp bound') by eauto with va.
+- assert (Block.lt sp bound') by eauto with va.
   eapply sound_stack_public_call; eauto.
-  rewrite H0; auto. xomega.
-  intros. rewrite H0; auto. xomega.
-- assert (Plt sp bound') by eauto with va.
+  rewrite H0; auto. eapply Block.lt_le_trans; eauto.
+  intros. rewrite H0; auto. eapply Block.lt_le_trans; eauto.
+- assert (Block.lt sp bound') by eauto with va.
   eapply sound_stack_private_call; eauto.
-  rewrite H0; auto. xomega.
-  intros. rewrite H0; auto. xomega.
+  rewrite H0; auto. eapply Block.lt_le_trans; eauto.
+  intros. rewrite H0; auto. eapply Block.lt_le_trans; eauto.
 Qed.
 
 (** ** Preservation of the semantic invariant by one step of execution *)
@@ -1251,7 +1266,7 @@ Proof.
   intros (bc' & A & B & C & D & E & F & G).
   apply sound_call_state with bc'; auto.
   * eapply sound_stack_private_call with (bound' := Mem.nextblock m) (bc' := bc); eauto.
-    apply Ple_refl.
+    blomega.
     eapply mmatch_below; eauto.
     eapply mmatch_stack; eauto.
   * intros. exploit list_in_map_inv; eauto. intros (r & P & Q). subst v.
@@ -1264,7 +1279,7 @@ Proof.
   exploit anonymize_stack; eauto. intros (bc' & A & B & C & D & E & F & G).
   apply sound_call_state with bc'; auto.
   * eapply sound_stack_public_call with (bound' := Mem.nextblock m) (bc' := bc); eauto.
-    apply Ple_refl.
+    blomega.
     eapply mmatch_below; eauto.
   * intros. exploit list_in_map_inv; eauto. intros (r & P & Q). subst v.
     apply D with (areg ae r). auto with va.
@@ -1276,15 +1291,15 @@ Proof.
   apply sound_stack_new_bound with stk.
   apply sound_stack_exten with bc.
   eapply sound_stack_free; eauto.
-  intros. apply C. apply Plt_ne; auto.
-  apply Plt_Ple. eapply mmatch_below; eauto. congruence.
+  intros. apply C. apply Blt_ne; auto.
+  apply Block.lt_le. eapply mmatch_below; eauto. congruence.
   intros. exploit list_in_map_inv; eauto. intros (r & P & Q). subst v.
   apply D with (areg ae r). auto with va.
   eapply romatch_free; eauto.
   eapply mmatch_free; eauto.
 
 - (* builtin *)
-  assert (SPVALID: Plt sp0 (Mem.nextblock m)) by (eapply mmatch_below; eauto with va).
+  assert (SPVALID: Block.lt sp0 (Mem.nextblock m)) by (eapply mmatch_below; eauto with va).
   assert (TR: transfer f rm pc ae am = transfer_builtin ae am rm ef args res).
   { unfold transfer; rewrite H; auto. }
   (* The default case *)
@@ -1318,8 +1333,9 @@ Proof.
   apply set_builtin_res_sound; auto.
   apply sound_stack_exten with bc.
   apply sound_stack_inv with m. auto.
-  intros. apply Q. red. eapply Plt_trans; eauto.
+  intros. apply Q. red. eapply Block.lt_trans; eauto.
   rewrite C; auto.
+  blomega.
   exact AA.
 * (* public builtin call *)
   exploit anonymize_stack; eauto.
@@ -1337,8 +1353,9 @@ Proof.
   apply set_builtin_res_sound; auto.
   apply sound_stack_exten with bc.
   apply sound_stack_inv with m. auto.
-  intros. apply Q. red. eapply Plt_trans; eauto.
+  intros. apply Q. red. eapply Block.lt_trans; eauto.
   rewrite C; auto.
+  blomega.
   exact AA.
   }
   unfold transfer_builtin in TR.
@@ -1412,8 +1429,8 @@ Proof.
   apply sound_stack_new_bound with stk.
   apply sound_stack_exten with bc.
   eapply sound_stack_free; eauto.
-  intros. apply C. apply Plt_ne; auto.
-  apply Plt_Ple. eapply mmatch_below; eauto with va.
+  intros. apply C. apply Blt_ne; auto.
+  apply Block.lt_le. eapply mmatch_below; eauto with va.
   destruct or; simpl. eapply D; eauto. constructor.
   eapply romatch_free; eauto.
   eapply mmatch_free; eauto.
@@ -1512,16 +1529,16 @@ Lemma initial_block_classification:
 Proof.
   intros.
   set (f := fun b =>
-              if plt b (Genv.genv_next ge) then
+              if Block.lt_dec b Block.init then
                 match Genv.invert_symbol ge b with None => BCother | Some id => BCglob id end
               else
                 BCinvalid).
   assert (F_glob: forall b1 b2 id, f b1 = BCglob id -> f b2 = BCglob id -> b1 = b2).
   {
     unfold f; intros.
-    destruct (plt b1 (Genv.genv_next ge)); try discriminate.
+    destruct (Block.lt_dec b1 Block.init); try discriminate.
     destruct (Genv.invert_symbol ge b1) as [id1|] eqn:I1; inv H0.
-    destruct (plt b2 (Genv.genv_next ge)); try discriminate.
+    destruct (Block.lt_dec b2 Block.init); try discriminate.
     destruct (Genv.invert_symbol ge b2) as [id2|] eqn:I2; inv H1.
     exploit Genv.invert_find_symbol. eexact I1.
     exploit Genv.invert_find_symbol. eexact I2.
@@ -1530,7 +1547,7 @@ Proof.
   assert (F_stack: forall b1 b2, f b1 = BCstack -> f b2 = BCstack -> b1 = b2).
   {
     unfold f; intros.
-    destruct (plt b1 (Genv.genv_next ge)); try discriminate.
+    destruct (Block.lt_dec b1 Block.init); try discriminate.
     destruct (Genv.invert_symbol ge b1); discriminate.
   }
   set (bc := BC f F_stack F_glob). unfold f in bc.
@@ -1540,17 +1557,17 @@ Proof.
     * rewrite pred_dec_true by (eapply Genv.genv_symb_range; eauto).
       erewrite Genv.find_invert_symbol; eauto.
     * apply Genv.invert_find_symbol.
-      destruct (plt b (Genv.genv_next ge)); try discriminate.
+      destruct (Block.lt_dec b Block.init); try discriminate.
       destruct (Genv.invert_symbol ge b); congruence.
   + rewrite ! pred_dec_true by assumption.
     destruct (Genv.invert_symbol); split; congruence.
-- red; simpl; intros. destruct (plt b (Genv.genv_next ge)); try congruence.
+- red; simpl; intros. destruct (Block.lt_dec b Block.init); try congruence.
   erewrite <- Genv.init_mem_genv_next by eauto. auto.
 - red; simpl; intros.
-  destruct (plt b (Genv.genv_next ge)).
+  destruct (Block.lt_dec b Block.init).
   destruct (Genv.invert_symbol ge b); congruence.
   congruence.
-- simpl; intros. destruct (plt b (Genv.genv_next ge)); try discriminate.
+- simpl; intros. destruct (Block.lt_dec b Block.init); try discriminate.
   destruct (Genv.invert_symbol ge b) as [id' | ] eqn:IS; inv H0.
   apply Genv.invert_find_symbol; auto.
 - intros; simpl. unfold ge; erewrite Genv.init_mem_genv_next by eauto.
@@ -1683,71 +1700,87 @@ Definition initial_mem_match (bc: block_classification) (m: mem) (g: genv) :=
 
 Lemma alloc_global_match:
   forall m g idg m',
-  Genv.genv_next g = Mem.nextblock m ->
   initial_mem_match bc m g ->
   Genv.alloc_global ge m idg = Some m' ->
   initial_mem_match bc m' (Genv.add_global g idg).
 Proof.
-  intros; red; intros. destruct idg as [id1 [fd | gv]]; simpl in *.
-- destruct (Mem.alloc m 0 1) as [m1 b1] eqn:ALLOC.
+  intros m g idg m' H0 H1.
+  red; intros id b v H2 H3 H4 H5.
+  destruct idg as [id1 [fd | gv]]; simpl in *.
+- set (b1 := Block.glob id1) in *.
+  set (m1 := Mem.alloc_at m b1 0 1) in *.
   unfold Genv.find_symbol in H2; simpl in H2.
   unfold Genv.find_var_info, Genv.find_def in H3; simpl in H3.
   rewrite PTree.gsspec in H2. destruct (peq id id1).
-  inv H2. rewrite PTree.gss in H3. discriminate.
-  assert (Plt b (Genv.genv_next g)) by (eapply Genv.genv_symb_range; eauto).
-  rewrite PTree.gso in H3 by (apply Plt_ne; auto).
-  assert (Mem.valid_block m b) by (red; rewrite <- H; auto).
-  assert (b <> b1) by (apply Mem.valid_not_valid_diff with m; eauto with mem).
+  inv H2. rewrite Block.ident_of_glob in H3. rewrite PTree.gss in H3. discriminate.
+  destruct (Block.ident_of b) eqn:Hb; try discriminate.
+  apply Block.ident_of_inv in Hb; subst.
+  destruct (Genv.genv_defs g) ! id eqn: DEF; try discriminate. inv H2.
+  apply Block.glob_inj in H6. subst.
+  rewrite PTree.gso in H3 by auto. rewrite DEF in H3.
+  destruct g0; inv H3.
   apply bmatch_inv with m.
   eapply H0; eauto.
-  intros. transitivity (Mem.loadbytes m1 b ofs n0).
-  eapply Mem.loadbytes_drop; eauto.
-  eapply Mem.loadbytes_alloc_unchanged; eauto.
+  unfold Genv.find_symbol. rewrite DEF; auto.
+  unfold Genv.find_var_info, Genv.find_def.
+  rewrite Block.ident_of_glob, DEF; auto.
+  intros. transitivity (Mem.loadbytes m1 (Block.glob i) ofs n0).
+  eapply Mem.loadbytes_drop; eauto. left. intro; subst. apply Block.glob_inj in H2. eauto.
+  eapply Mem.loadbytes_unchanged_on_1 with (P := fun b _ => b <> b1).
+  eapply Mem.alloc_at_unchanged_on. reflexivity. tauto.
+  eapply Block.lt_le_trans. apply Block.lt_glob_init. apply Mem.init_nextblock.
+  intros; intro; subst. apply Block.glob_inj in H3. auto.
 - set (sz := init_data_list_size (gvar_init gv)) in *.
-  destruct (Mem.alloc m 0 sz) as [m1 b1] eqn:ALLOC.
+  set (b1 := Block.glob id1) in *.
+  set (m1 := Mem.alloc_at m b1 0 sz) in *.
   destruct (store_zeros m1 b1 0 sz) as [m2 | ] eqn:STZ; try discriminate.
   destruct (Genv.store_init_data_list ge m2 b1 0 (gvar_init gv)) as [m3 | ] eqn:SIDL; try discriminate.
   unfold Genv.find_symbol in H2; simpl in H2.
   unfold Genv.find_var_info, Genv.find_def in H3; simpl in H3.
-  rewrite PTree.gsspec in H2. destruct (peq id id1).
+  destruct (Block.ident_of b) eqn:Hb; try discriminate.
+  apply Block.ident_of_inv in Hb; subst.
+  rewrite PTree.gsspec in H2, H3. destruct (peq id id1).
 + injection H2; clear H2; intro EQ.
-  rewrite EQ, PTree.gss in H3. injection H3; clear H3; intros EQ'; subst v.
-  assert (b = b1). { erewrite Mem.alloc_result by eauto. congruence. }
-  clear EQ. subst b.
+  apply Block.glob_inj in EQ. subst. rewrite peq_true in H3. inv H3.
   apply bmatch_inv with m3.
   eapply store_init_data_list_sound; eauto.
   apply ablock_init_sound.
   eapply store_zeros_same; eauto.
   split; intros.
-  exploit Mem.load_alloc_same; eauto. intros EQ; subst v; constructor.
-  exploit Mem.loadbytes_alloc_same; eauto with coqlib. congruence.
+  exploit Mem.load_alloc_at_same; eauto. apply Block.lt_glob_init. intros EQ; subst v0; constructor.
+  exploit Mem.loadbytes_alloc_at_same; eauto with coqlib. apply Block.lt_glob_init. congruence.
   intros. eapply Mem.loadbytes_drop; eauto.
   right; right; right. unfold Genv.perm_globvar. rewrite H4, H5. constructor.
-+ assert (Plt b (Genv.genv_next g)) by (eapply Genv.genv_symb_range; eauto).
-  rewrite PTree.gso in H3 by (apply Plt_ne; auto).
-  assert (Mem.valid_block m b) by (red; rewrite <- H; auto).
-  assert (b <> b1) by (apply Mem.valid_not_valid_diff with m; eauto with mem).
++ destruct (Genv.genv_defs g) ! id eqn: DEF; try discriminate. inv H2.
+  apply Block.glob_inj in H6; subst.
+  rewrite peq_false in H3; auto. rewrite DEF in H3. destruct g0; try discriminate. inv H3.
+  assert (Block.lt b1 Block.init) by (apply Block.lt_glob_init).
+  assert (Block.glob i <> b1). { intro EQ; apply Block.glob_inj in EQ; congruence. }
   apply bmatch_inv with m3.
   eapply store_init_data_list_other; eauto.
   eapply store_zeros_other; eauto.
   apply bmatch_inv with m.
   eapply H0; eauto.
-  intros. eapply Mem.loadbytes_alloc_unchanged; eauto.
+  unfold Genv.find_symbol. rewrite DEF; auto.
+  unfold Genv.find_var_info, Genv.find_def.
+  rewrite Block.ident_of_glob, DEF; auto.
+  intros; eapply Mem.loadbytes_unchanged_on_1 with (P := fun b _ => b <> b1).
+  eapply Mem.alloc_at_unchanged_on. reflexivity. tauto.
+  eapply Block.lt_le_trans. apply Block.lt_glob_init. apply Mem.init_nextblock.
+  intros; intro EQ; subst. apply Block.glob_inj in EQ. auto.
   intros. eapply Mem.loadbytes_drop; eauto.
 Qed.
 
 Lemma alloc_globals_match:
   forall gl m g m',
-  Genv.genv_next g = Mem.nextblock m ->
   initial_mem_match bc m g ->
   Genv.alloc_globals ge m gl = Some m' ->
   initial_mem_match bc m' (Genv.add_globals g gl).
 Proof.
   induction gl; simpl; intros.
-- inv H1; auto.
+- inv H0; auto.
 - destruct (Genv.alloc_global ge m a) as [m1|] eqn:AG; try discriminate.
   eapply IHgl; eauto.
-  erewrite Genv.alloc_global_nextblock; eauto. simpl. congruence.
   eapply alloc_global_match; eauto.
 Qed.
 
@@ -1854,9 +1887,10 @@ Proof.
 - apply RM; auto.
 - apply mmatch_inj_top with m0.
   replace (inj_of_bc bc) with (Mem.flat_inj (Mem.nextblock m0)).
+  erewrite <- Genv.init_mem_genv_next; eauto.
   eapply Genv.initmem_inject; eauto.
   symmetry; apply extensionality; unfold Mem.flat_inj; intros x.
-  destruct (plt x (Mem.nextblock m0)).
+  destruct (Block.lt_dec x (Mem.nextblock m0)).
   apply inj_of_bc_valid; auto.
   unfold inj_of_bc. erewrite bc_below_invalid; eauto.
 - exact GE.
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index e7e44e29eb..3db56d0e8b 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -34,10 +34,10 @@ Record block_classification : Type := BC {
 }.
 
 Definition bc_below (bc: block_classification) (bound: block) : Prop :=
-  forall b, bc b <> BCinvalid -> Plt b bound.
+  forall b, bc b <> BCinvalid -> Block.lt b bound.
 
 Lemma bc_below_invalid:
-  forall b bc bound, ~Plt b bound -> bc_below bc bound -> bc b = BCinvalid.
+  forall b bc bound, ~Block.lt b bound -> bc_below bc bound -> bc b = BCinvalid.
 Proof.
   intros. destruct (block_class_eq (bc b) BCinvalid); auto.
   elim H. apply H0; auto.
@@ -1115,7 +1115,7 @@ Qed.
 
 Definition genv_match (ge: genv) : Prop :=
   (forall id b, Genv.find_symbol ge id = Some b <-> bc b = BCglob id)
-/\(forall b, Plt b (Genv.genv_next ge) -> bc b <> BCinvalid /\ bc b <> BCstack).
+/\(forall b, Block.lt b Block.init -> bc b <> BCinvalid /\ bc b <> BCstack).
 
 Lemma symbol_address_sound:
   forall ge id ofs,
@@ -4058,7 +4058,7 @@ Lemma mmatch_ext:
   forall m am m',
   mmatch m am ->
   (forall b ofs n bytes, bc b <> BCinvalid -> n >= 0 -> Mem.loadbytes m' b ofs n = Some bytes -> Mem.loadbytes m b ofs n = Some bytes) ->
-  Ple (Mem.nextblock m) (Mem.nextblock m') ->
+  Block.le (Mem.nextblock m) (Mem.nextblock m') ->
   mmatch m' am.
 Proof.
   intros. inv H. constructor; intros.
@@ -4066,7 +4066,7 @@ Proof.
 - apply bmatch_ext with m; eauto with va.
 - apply smatch_ext with m; auto with va.
 - apply smatch_ext with m; auto with va.
-- red; intros. exploit mmatch_below0; eauto. xomega.
+- red; intros. exploit mmatch_below0; eauto; blomega.
 Qed.
 
 Lemma mmatch_free:
@@ -4077,7 +4077,7 @@ Lemma mmatch_free:
 Proof.
   intros. apply mmatch_ext with m; auto.
   intros. eapply Mem.loadbytes_free_2; eauto.
-  erewrite <- Mem.nextblock_free by eauto. xomega.
+  erewrite <- Mem.nextblock_free by eauto. apply Block.le_refl.
 Qed.
 
 Lemma mmatch_top':
@@ -4296,7 +4296,7 @@ Proof.
 - (* contents *)
   intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst.
   rewrite Z.add_0_r.
-  set (mv := ZMap.get ofs (PMap.get b1 (Mem.mem_contents m))).
+  set (mv := ZMap.get ofs (BMap.get b1 (Mem.mem_contents m))).
   assert (Mem.loadbytes m b1 ofs 1 = Some (mv :: nil)).
   {
     Local Transparent Mem.loadbytes.
@@ -4334,7 +4334,9 @@ 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.
+    rewrite Genv.find_var_info_iff in H. unfold Genv.find_def in H.
+    destruct (Block.ident_of b) eqn:Hb; try congruence.
+    apply Block.ident_of_inv in Hb; subst. apply Block.lt_glob_init.
   intros. exploit inj_of_bc_inv; eauto. intros (P & Q & R). auto.
 Qed.
 
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index ffafc5d242..9bacc59df7 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -210,12 +210,12 @@ Record match_env (f: meminj) (cenv: compilenv)
 
 (** [lo, hi] is a proper interval. *)
     me_low_high:
-      Ple lo hi;
+      Block.le lo hi;
 
 (** Every block appearing in the C#minor environment [e] must be
   in the range [lo, hi]. *)
     me_bounded:
-      forall id b sz, PTree.get id e = Some(b, sz) -> Ple lo b /\ Plt b hi;
+      forall id b sz, PTree.get id e = Some(b, sz) -> Block.le lo b /\ Block.lt b hi;
 
 (** All blocks mapped to sub-blocks of the Cminor stack data must be
     images of variables from the C#minor environment [e] *)
@@ -229,7 +229,7 @@ Record match_env (f: meminj) (cenv: compilenv)
   (i.e. allocated before the stack data for the current Cminor function). *)
     me_incr:
       forall b tb delta,
-      f b = Some(tb, delta) -> Plt b lo -> Plt tb sp
+      f b = Some(tb, delta) -> Block.lt b lo -> Block.lt tb sp
   }.
 
 Ltac geninv x :=
@@ -240,7 +240,7 @@ Lemma match_env_invariant:
   match_env f1 cenv e sp lo hi ->
   inject_incr f1 f2 ->
   (forall b delta, f2 b = Some(sp, delta) -> f1 b = Some(sp, delta)) ->
-  (forall b, Plt b lo -> f2 b = f1 b) ->
+  (forall b, Block.lt b lo -> f2 b = f1 b) ->
   match_env f2 cenv e sp lo hi.
 Proof.
   intros. destruct H. constructor; auto.
@@ -282,12 +282,12 @@ Lemma match_env_external_call:
   match_env f1 cenv e sp lo hi ->
   inject_incr f1 f2 ->
   inject_separated f1 f2 m1 m1' ->
-  Ple hi (Mem.nextblock m1) -> Plt sp (Mem.nextblock m1') ->
+  Block.le hi (Mem.nextblock m1) -> Block.lt sp (Mem.nextblock m1') ->
   match_env f2 cenv e sp lo hi.
 Proof.
   intros. apply match_env_invariant with f1; auto.
   intros. eapply inject_incr_separated_same'; eauto.
-  intros. eapply inject_incr_separated_same; eauto. red. destruct H. xomega.
+  intros. eapply inject_incr_separated_same; eauto. red. destruct H. blomega.
 Qed.
 
 (** [match_env] and allocations *)
@@ -317,18 +317,18 @@ Proof.
   constructor; eauto.
   constructor.
 (* low-high *)
-  rewrite NEXTBLOCK; xomega.
+  rewrite NEXTBLOCK; blomega.
 (* bounded *)
   intros. rewrite PTree.gsspec in H. destruct (peq id0 id).
-  inv H. rewrite NEXTBLOCK; xomega.
-  exploit me_bounded0; eauto. rewrite NEXTBLOCK; xomega.
+  inv H. rewrite NEXTBLOCK; blomega.
+  exploit me_bounded0; eauto. rewrite NEXTBLOCK; intuition blomega.
 (* inv *)
   intros. destruct (eq_block b (Mem.nextblock m1)).
   subst b. rewrite SAME in H; inv H. exists id; exists sz. apply PTree.gss.
   rewrite OTHER in H; auto. exploit me_inv0; eauto.
   intros [id1 [sz1 EQ]]. exists id1; exists sz1. rewrite PTree.gso; auto. congruence.
 (* incr *)
-  intros. rewrite OTHER in H. eauto. unfold block in *; xomega.
+  intros. rewrite OTHER in H. eauto. unfold block in *; blomega.
 Qed.
 
 (** The sizes of blocks appearing in [e] are respected. *)
@@ -368,7 +368,7 @@ Lemma padding_freeable_invariant:
   padding_freeable f1 e tm1 sp sz ->
   match_env f1 cenv e sp lo hi ->
   (forall ofs, Mem.perm tm1 sp ofs Cur Freeable -> Mem.perm tm2 sp ofs Cur Freeable) ->
-  (forall b, Plt b hi -> f2 b = f1 b) ->
+  (forall b, Block.lt b hi -> f2 b = f1 b) ->
   padding_freeable f2 e tm2 sp sz.
 Proof.
   intros; red; intros.
@@ -423,11 +423,11 @@ Qed.
 
 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).
+      (DOMAIN: forall b, Block.lt b bound -> f b = Some(b, 0))
+      (IMAGE: forall b1 b2 delta, f b1 = Some(b2, delta) -> Block.lt b2 bound -> b1 = b2)
+      (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> Block.lt b bound)
+      (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> Block.lt b bound)
+      (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> Block.lt b bound).
 
 Remark inj_preserves_globals:
   forall f hi,
@@ -473,12 +473,12 @@ Inductive match_callstack (f: meminj) (m: mem) (tm: mem):
   | mcs_nil:
       forall hi bound tbound,
       match_globalenvs f hi ->
-      Ple hi bound -> Ple hi tbound ->
+      Block.le hi bound -> Block.le hi tbound ->
       match_callstack f m tm nil bound tbound
   | mcs_cons:
       forall cenv tf e le te sp lo hi cs bound tbound
-        (BOUND: Ple hi bound)
-        (TBOUND: Plt sp tbound)
+        (BOUND: Block.le hi bound)
+        (TBOUND: Block.lt sp tbound)
         (MTMP: match_temps f le te)
         (MENV: match_env f cenv e sp lo hi)
         (BOUND: match_bounds e m)
@@ -502,44 +502,44 @@ Lemma match_callstack_invariant:
   forall f1 m1 tm1 f2 m2 tm2 cs bound tbound,
   match_callstack f1 m1 tm1 cs bound tbound ->
   inject_incr f1 f2 ->
-  (forall b ofs p, Plt b bound -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) ->
-  (forall sp ofs, Plt sp tbound -> Mem.perm tm1 sp ofs Cur Freeable -> Mem.perm tm2 sp ofs Cur Freeable) ->
-  (forall b, Plt b bound -> f2 b = f1 b) ->
-  (forall b b' delta, f2 b = Some(b', delta) -> Plt b' tbound -> f1 b = Some(b', delta)) ->
+  (forall b ofs p, Block.lt b bound -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) ->
+  (forall sp ofs, Block.lt sp tbound -> Mem.perm tm1 sp ofs Cur Freeable -> Mem.perm tm2 sp ofs Cur Freeable) ->
+  (forall b, Block.lt b bound -> f2 b = f1 b) ->
+  (forall b b' delta, f2 b = Some(b', delta) -> Block.lt b' tbound -> f1 b = Some(b', delta)) ->
   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. xomega.
+  eapply IMAGE; eauto. eapply H6; eauto. blomega.
   (* inductive case *)
-  assert (Ple lo hi) by (eapply me_low_high; eauto).
+  assert (Block.le lo hi) by (eapply me_low_high; eauto).
   econstructor; eauto.
   eapply match_temps_invariant; eauto.
   eapply match_env_invariant; eauto.
-    intros. apply H3. xomega.
+    intros. apply H3. blomega.
   eapply match_bounds_invariant; eauto.
     intros. eapply H1; eauto.
-    exploit me_bounded; eauto. xomega.
+    exploit me_bounded; eauto. intuition blomega.
   eapply padding_freeable_invariant; eauto.
-    intros. apply H3. xomega.
+    intros. apply H3. blomega.
   eapply IHmatch_callstack; eauto.
-    intros. eapply H1; eauto. xomega.
-    intros. eapply H2; eauto. xomega.
-    intros. eapply H3; eauto. xomega.
-    intros. eapply H4; eauto. xomega.
+    intros. eapply H1; eauto. blomega.
+    intros. eapply H2; eauto. blomega.
+    intros. eapply H3; eauto. blomega.
+    intros. eapply H4; eauto. blomega.
 Qed.
 
 Lemma match_callstack_incr_bound:
   forall f m tm cs bound tbound bound' tbound',
   match_callstack f m tm cs bound tbound ->
-  Ple bound bound' -> Ple tbound tbound' ->
+  Block.le bound bound' -> Block.le tbound tbound' ->
   match_callstack f m tm cs bound' tbound'.
 Proof.
   intros. inv H.
-  econstructor; eauto. xomega. xomega.
-  constructor; auto. xomega. xomega.
+  econstructor; eauto. blomega. blomega.
+  constructor; auto. blomega. blomega.
 Qed.
 
 (** Assigning a temporary variable. *)
@@ -606,7 +606,7 @@ Proof.
   apply match_callstack_incr_bound with lo sp; try omega.
   apply match_callstack_invariant with f m tm; auto.
   intros. eapply perm_freelist; eauto.
-  intros. eapply Mem.perm_free_1; eauto. left; unfold block; xomega. xomega. xomega.
+  intros. eapply Mem.perm_free_1; eauto. left; unfold block; blomega. blomega. blomega.
   eapply Mem.free_inject; eauto.
   intros. exploit me_inv0; eauto. intros [id [sz A]].
   exists 0; exists sz; split.
@@ -625,7 +625,7 @@ Lemma match_callstack_external_call:
   (forall b ofs p, Mem.valid_block m1 b -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) ->
   forall cs bound tbound,
   match_callstack f1 m1 m1' cs bound tbound ->
-  Ple bound (Mem.nextblock m1) -> Ple tbound (Mem.nextblock m1') ->
+  Block.le bound (Mem.nextblock m1) -> Block.le tbound (Mem.nextblock m1') ->
   match_callstack f2 m2 m2' cs bound tbound.
 Proof.
   intros until m2'.
@@ -636,21 +636,21 @@ Proof.
   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. xomega.
+  intro EQ. exploit SEPARATED; eauto. intros [A B]. elim B. red. blomega.
 (* inductive case *)
   constructor. auto. auto.
   eapply match_temps_invariant; eauto.
   eapply match_env_invariant; eauto.
   red in SEPARATED. intros. destruct (f1 b) as [[b' delta']|] eqn:?.
   exploit INCR; eauto. congruence.
-  exploit SEPARATED; eauto. intros [A B]. elim B. red. xomega.
-  intros. assert (Ple lo hi) by (eapply me_low_high; eauto).
+  exploit SEPARATED; eauto. intros [A B]. elim B. red. blomega.
+  intros. assert (Block.le lo hi) by (eapply me_low_high; eauto).
   destruct (f1 b) as [[b' delta']|] eqn:?.
   apply INCR; auto.
   destruct (f2 b) as [[b' delta']|] eqn:?; auto.
-  exploit SEPARATED; eauto. intros [A B]. elim A. red. xomega.
+  exploit SEPARATED; eauto. intros [A B]. elim A. red. blomega.
   eapply match_bounds_invariant; eauto.
-  intros. eapply MAXPERMS; eauto. red. exploit me_bounded; eauto. xomega.
+  intros. eapply MAXPERMS; eauto. red. exploit me_bounded; eauto. intuition blomega.
   (* padding-freeable *)
   red; intros.
   destruct (is_reachable_from_env_dec f1 e sp ofs).
@@ -663,7 +663,7 @@ Proof.
   apply is_reachable_intro with id b0 lv delta; auto; omega.
   eauto with mem.
   (* induction *)
-  eapply IHmatch_callstack; eauto. inv MENV; xomega. xomega.
+  eapply IHmatch_callstack; eauto. inv MENV; blomega. blomega.
 Qed.
 
 (** [match_callstack] and allocations *)
@@ -683,12 +683,12 @@ Proof.
   exploit Mem.nextblock_alloc; eauto. intros NEXTBLOCK.
   exploit Mem.alloc_result; eauto. intros RES.
   constructor.
-  xomega.
-  unfold block in *; xomega.
+  blomega.
+  rewrite NEXTBLOCK, RES. intuition blomega.
   auto.
   constructor; intros.
     rewrite H3. rewrite PTree.gempty. constructor.
-    xomega.
+    blomega.
     rewrite PTree.gempty in H4; discriminate.
     eelim Mem.fresh_block_alloc; eauto. eapply Mem.valid_block_inject_2; eauto.
     rewrite RES. change (Mem.valid_block tm tb). eapply Mem.valid_block_inject_2; eauto.
@@ -717,25 +717,25 @@ Proof.
   intros. inv H.
   exploit Mem.nextblock_alloc; eauto. intros NEXTBLOCK.
   exploit Mem.alloc_result; eauto. intros RES.
-  assert (LO: Ple lo (Mem.nextblock m1)) by (eapply me_low_high; eauto).
+  assert (LO: Block.le lo (Mem.nextblock m1)) by (eapply me_low_high; eauto).
   constructor.
-  xomega.
+  blomega.
   auto.
   eapply match_temps_invariant; eauto.
   eapply match_env_alloc; eauto.
   red; intros. rewrite PTree.gsspec in H. destruct (peq id0 id).
   inversion H. subst b0 sz0 id0. eapply Mem.perm_alloc_3; eauto.
   eapply BOUND0; eauto. eapply Mem.perm_alloc_4; eauto.
-  exploit me_bounded; eauto. unfold block in *; xomega.
+  exploit me_bounded; eauto. intuition subst. apply Blt_ne in H10. congruence.
   red; intros. exploit PERM; eauto. intros [A|A]. auto. right.
   inv A. apply is_reachable_intro with id0 b0 sz0 delta; auto.
   rewrite PTree.gso. auto. congruence.
   eapply match_callstack_invariant with (m1 := m1); eauto.
   intros. eapply Mem.perm_alloc_4; eauto.
-  unfold block in *; xomega.
-  intros. apply H4. unfold block in *; xomega.
+  eapply Blt_ne. subst; blomega.
+  intros. apply H4. eapply Blt_ne. subst; blomega.
   intros. destruct (eq_block b0 b).
-  subst b0. rewrite H3 in H. inv H. xomegaContradiction.
+  subst b0. rewrite H3 in H. inv H. apply Block.lt_strict in H6; easy.
   rewrite H4 in H; auto.
 Qed.
 
@@ -2039,7 +2039,7 @@ Proof.
     apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm).
     eapply match_callstack_external_call; eauto.
     intros. eapply external_call_max_perm; eauto.
-    xomega. xomega.
+    blomega. blomega.
     eapply external_call_nextblock; eauto.
     eapply external_call_nextblock; eauto.
   econstructor; eauto.
@@ -2191,7 +2191,7 @@ Opaque PTree.set.
   apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm).
   eapply match_callstack_external_call; eauto.
   intros. eapply external_call_max_perm; eauto.
-  xomega. xomega.
+  blomega. blomega.
   eapply external_call_nextblock; eauto.
   eapply external_call_nextblock; eauto.
 
@@ -2211,7 +2211,7 @@ 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.
+  destruct (Block.lt_dec 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.
@@ -2234,8 +2234,9 @@ Proof.
   rewrite <- H2. apply sig_preserved; auto.
   eapply match_callstate with (f := Mem.flat_inj (Mem.nextblock m0)) (cs := @nil frame) (cenv := PTree.empty Z).
   auto.
+  erewrite <- Genv.init_mem_genv_next; eauto.
   eapply Genv.initmem_inject; eauto.
-  apply mcs_nil with (Mem.nextblock m0). apply match_globalenvs_init; auto. xomega. xomega.
+  apply mcs_nil with (Mem.nextblock m0). apply match_globalenvs_init; auto. blomega. blomega.
   constructor. red; auto.
   constructor.
 Qed.
diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index 77d6cfea85..c93aeaf163 100644
--- a/cfrontend/Initializers.v
+++ b/cfrontend/Initializers.v
@@ -110,7 +110,7 @@ Fixpoint constval (ce: composite_env) (a: expr) : res val :=
   | Ecomma r1 r2 ty =>
       do v1 <- constval ce r1; constval ce r2
   | Evar x ty =>
-      OK(Vptr x Ptrofs.zero)
+      OK(Vptr (Block.glob x) Ptrofs.zero)
   | Ederef r ty =>
       constval ce r
   | Efield l f ty =>
@@ -152,6 +152,12 @@ with initializer_list :=
 (** Translate an initializing expression [a] for a scalar variable
   of type [ty].  Return the corresponding initialization datum. *)
 
+Definition transl_init_ptr (b: block) (ofs: ptrofs) :=
+  match Block.ident_of b with
+    | Some id => OK (Init_addrof id ofs)
+    | None => Error (msg "non-global pointer in initializer")
+  end.
+
 Definition transl_init_single (ce: composite_env) (ty: type) (a: expr) : res init_data :=
   do v <- constval_cast ce a ty;
   match v, ty with
@@ -163,9 +169,9 @@ Definition transl_init_single (ce: composite_env) (ty: type) (a: expr) : res ini
   | Vlong n, Tpointer _ _ => assertion (Archi.ptr64); OK(Init_int64 n)
   | Vsingle f, Tfloat F32 _ => OK(Init_float32 f)
   | Vfloat f, Tfloat F64 _ => OK(Init_float64 f)
-  | Vptr id ofs, Tint I32 sg _ => assertion (negb Archi.ptr64); OK(Init_addrof id ofs)
-  | Vptr id ofs, Tlong _ _ => assertion (Archi.ptr64); OK(Init_addrof id ofs)
-  | Vptr id ofs, Tpointer _ _ => OK(Init_addrof id ofs)
+  | Vptr b ofs, Tint I32 sg _ => assertion (negb Archi.ptr64); transl_init_ptr b ofs
+  | Vptr b ofs, Tlong _ _ => assertion (Archi.ptr64); transl_init_ptr b ofs
+  | Vptr b ofs, Tpointer _ _ => transl_init_ptr b ofs
   | Vundef, _ => Error(msg "undefined operation in initializer")
   | _, _ => Error (msg "type mismatch in initializer")
   end.
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index 272b929f1a..cd37962268 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -323,9 +323,13 @@ Qed.
   [Vptr b ofs] where [Genv.find_symbol ge id = Some b]. *)
 
 Definition inj (b: block) :=
-  match Genv.find_symbol ge b with
-  | Some b' => Some (b', 0)
-  | None => None
+  match Block.ident_of b with
+    Some i =>
+    match Genv.find_symbol ge i with
+    | Some b' => Some (b', 0)
+    | None => None
+    end
+  | _ => None
   end.
 
 Lemma mem_empty_not_valid_pointer:
@@ -440,7 +444,7 @@ Proof.
   (* var local *)
   unfold empty_env in H. rewrite PTree.gempty in H. congruence.
   (* var_global *)
-  econstructor. unfold inj. rewrite H0. eauto. auto.
+  econstructor. unfold inj. rewrite Block.ident_of_glob, H0. eauto. auto.
   (* deref *)
   eauto.
   (* field struct *)
@@ -626,14 +630,17 @@ Proof.
   destruct ty; try discriminate.
   destruct f1; inv EQ0; simpl in H2; inv H2; assumption.
 - (* pointer *)
+  unfold transl_init_ptr in *.
   unfold inj in H.
-  assert (data = Init_addrof b1 ofs1 /\ chunk = Mptr).
+  destruct (Block.ident_of b1) eqn:Hb; try discriminate.
+  assert (data = Init_addrof i ofs1 /\ chunk = Mptr).
   { remember Archi.ptr64 as ptr64.
+    unfold transl_init_ptr in *.
     destruct ty; inversion EQ0.
-    destruct i; inv H5. unfold Mptr. destruct Archi.ptr64; inv H6; inv H2; auto.
+    destruct i0; inv H5. unfold Mptr. destruct Archi.ptr64; inv H6; inv H2; auto.
     subst ptr64. unfold Mptr. destruct Archi.ptr64; inv H5; inv H2; auto.
     inv H2. auto. }
-  destruct H4; subst. destruct (Genv.find_symbol ge b1); inv H.
+  destruct H4; subst. destruct (Genv.find_symbol ge i); inv H.
   rewrite Ptrofs.add_zero in H3. auto.
 - (* undef *)
   discriminate.
@@ -659,11 +666,17 @@ Local Transparent sizeof.
   destruct f0; inv EQ0; auto.
 - destruct ty; try discriminate.
   destruct f0; inv EQ0; auto.
-- destruct ty; try discriminate.
+- unfold transl_init_ptr in *.
+  destruct ty; try discriminate.
   destruct i0; inv EQ0; auto.
-  destruct Archi.ptr64 eqn:SF; inv H0. simpl. rewrite SF; auto.
-  destruct ptr64; inv EQ0. simpl. rewrite <- Heqptr64; auto.
-  inv EQ0. unfold init_data_size, sizeof. auto.
+  destruct Archi.ptr64 eqn:SF; inv H0.
+  destruct (Block.ident_of b) eqn:Hb; inv H1.
+  simpl. rewrite SF; auto.
+  destruct ptr64; inv EQ0.
+  destruct (Block.ident_of b) eqn:Hb; inv H0.
+  simpl. rewrite <- Heqptr64; auto.
+  destruct (Block.ident_of b) eqn:Hb; inv EQ0.
+  unfold init_data_size, sizeof. auto.
 Qed.
 
 Notation idlsize := init_data_list_size.
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 26d3d347cf..f4d9ec713e 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -113,9 +113,9 @@ Record match_envs (f: meminj) (cenv: compilenv)
     me_inj:
       forall id1 b1 ty1 id2 b2 ty2, e!id1 = Some(b1, ty1) -> e!id2 = Some(b2, ty2) -> id1 <> id2 -> b1 <> b2;
     me_range:
-      forall id b ty, e!id = Some(b, ty) -> Ple lo b /\ Plt b hi;
+      forall id b ty, e!id = Some(b, ty) -> Block.le lo b /\ Block.lt b hi;
     me_trange:
-      forall id b ty, te!id = Some(b, ty) -> Ple tlo b /\ Plt b thi;
+      forall id b ty, te!id = Some(b, ty) -> Block.le tlo b /\ Block.lt b thi;
     me_mapped:
       forall id b' ty,
       te!id = Some(b', ty) -> exists b, f b = Some(b', 0) /\ e!id = Some(b, ty);
@@ -123,9 +123,9 @@ Record match_envs (f: meminj) (cenv: compilenv)
       forall id b' ty b delta,
       te!id = Some(b', ty) -> f b = Some(b', delta) -> e!id = Some(b, ty) /\ delta = 0;
     me_incr:
-      Ple lo hi;
+      Block.le lo hi;
     me_tincr:
-      Ple tlo thi
+      Block.le tlo thi
   }.
 
 (** Invariance by change of memory and injection *)
@@ -134,10 +134,10 @@ Lemma match_envs_invariant:
   forall f cenv e le m lo hi te tle tlo thi f' m',
   match_envs f cenv e le m lo hi te tle tlo thi ->
   (forall b chunk v,
-    f b = None -> Ple lo b /\ Plt b hi -> Mem.load chunk m b 0 = Some v -> Mem.load chunk m' b 0 = Some v) ->
+    f b = None -> Block.le lo b /\ Block.lt b hi -> Mem.load chunk m b 0 = Some v -> Mem.load chunk m' b 0 = Some v) ->
   inject_incr f f' ->
-  (forall b, Ple lo b /\ Plt b hi -> f' b = f b) ->
-  (forall b b' delta, f' b = Some(b', delta) -> Ple tlo b' /\ Plt b' thi -> f' b = f b) ->
+  (forall b, Block.le lo b /\ Block.lt b hi -> f' b = f b) ->
+  (forall b b' delta, f' b = Some(b', delta) -> Block.le tlo b' /\ Block.lt b' thi -> f' b = f b) ->
   match_envs f' cenv e le m' lo hi te tle tlo thi.
 Proof.
   intros until m'; intros ME LD INCR INV1 INV2.
@@ -164,7 +164,7 @@ Lemma match_envs_extcall:
   Mem.unchanged_on (loc_unmapped f) m m' ->
   inject_incr f f' ->
   inject_separated f f' m tm ->
-  Ple hi (Mem.nextblock m) -> Ple thi (Mem.nextblock tm) ->
+  Block.le hi (Mem.nextblock m) -> Block.le thi (Mem.nextblock tm) ->
   match_envs f' cenv e le m' lo hi te tle tlo thi.
 Proof.
   intros. eapply match_envs_invariant; eauto.
@@ -173,10 +173,10 @@ Proof.
   eapply H1; eauto.
   destruct (f' b) as [[b' delta]|] eqn:?; auto.
   exploit H2; eauto. unfold Mem.valid_block. intros [A B].
-  xomegaContradiction.
+  exfalso; intuition blomega.
   intros. destruct (f b) as [[b'' delta']|] eqn:?. eauto.
   exploit H2; eauto. unfold Mem.valid_block. intros [A B].
-  xomegaContradiction.
+  exfalso; intuition blomega.
 Qed.
 
 (** Properties of values resulting from a cast *)
@@ -586,17 +586,18 @@ Hint Resolve compat_cenv_union_l compat_cenv_union_r compat_cenv_empty: compat.
 
 Lemma alloc_variables_nextblock:
   forall ge e m vars e' m',
-  alloc_variables ge e m vars e' m' -> Ple (Mem.nextblock m) (Mem.nextblock m').
+  alloc_variables ge e m vars e' m' -> Block.le (Mem.nextblock m) (Mem.nextblock m').
 Proof.
   induction 1.
-  apply Ple_refl.
-  eapply Ple_trans; eauto. exploit Mem.nextblock_alloc; eauto. intros EQ; rewrite EQ. apply Ple_succ.
+  apply Block.le_refl.
+  eapply Block.le_trans; eauto. exploit Mem.nextblock_alloc; eauto. intros EQ; rewrite EQ.
+  blomega.
 Qed.
 
 Lemma alloc_variables_range:
   forall ge id b ty e m vars e' m',
   alloc_variables ge e m vars e' m' ->
-  e'!id = Some(b, ty) -> e!id = Some(b, ty) \/ Ple (Mem.nextblock m) b /\ Plt b (Mem.nextblock m').
+  e'!id = Some(b, ty) -> e!id = Some(b, ty) \/ Block.le (Mem.nextblock m) b /\ Block.lt b (Mem.nextblock m').
 Proof.
   induction 1; intros.
   auto.
@@ -604,16 +605,16 @@ Proof.
   destruct (peq id id0). inv A.
   right. exploit Mem.alloc_result; eauto. exploit Mem.nextblock_alloc; eauto.
   generalize (alloc_variables_nextblock _ _ _ _ _ _ H0). intros A B C.
-  subst b. split. apply Ple_refl. eapply Pos.lt_le_trans; eauto. rewrite B. apply Plt_succ.
+  subst b. split. blomega. eapply Block.lt_le_trans; eauto. rewrite B. blomega.
   auto.
-  right. exploit Mem.nextblock_alloc; eauto. intros B. rewrite B in A. xomega.
+  right. exploit Mem.nextblock_alloc; eauto. intros B. rewrite B in A. intuition blomega.
 Qed.
 
 Lemma alloc_variables_injective:
   forall ge id1 b1 ty1 id2 b2 ty2 e m vars e' m',
   alloc_variables ge e m vars e' m' ->
   (e!id1 = Some(b1, ty1) -> e!id2 = Some(b2, ty2) -> id1 <> id2 -> b1 <> b2) ->
-  (forall id b ty, e!id = Some(b, ty) -> Plt b (Mem.nextblock m)) ->
+  (forall id b ty, e!id = Some(b, ty) -> Block.lt b (Mem.nextblock m)) ->
   (e'!id1 = Some(b1, ty1) -> e'!id2 = Some(b2, ty2) -> id1 <> id2 -> b1 <> b2).
 Proof.
   induction 1; intros.
@@ -622,12 +623,13 @@ Proof.
   repeat rewrite PTree.gsspec; intros.
   destruct (peq id1 id); destruct (peq id2 id).
   congruence.
-  inv H6. exploit Mem.alloc_result; eauto. exploit H2; eauto. unfold block; xomega.
-  inv H7. exploit Mem.alloc_result; eauto. exploit H2; eauto. unfold block; xomega.
+  inv H6. exploit Mem.alloc_result; eauto. intros ->. exploit H2; eauto.
+  intros; apply not_eq_sym; blomega.
+  inv H7. exploit Mem.alloc_result; eauto. intros ->. exploit H2; eauto. blomega.
   eauto.
   intros. rewrite PTree.gsspec in H6. destruct (peq id0 id). inv H6.
-  exploit Mem.alloc_result; eauto. exploit Mem.nextblock_alloc; eauto. unfold block; xomega.
-  exploit H2; eauto. exploit Mem.nextblock_alloc; eauto. unfold block; xomega.
+  exploit Mem.alloc_result; eauto. exploit Mem.nextblock_alloc; eauto. intros -> ->. blomega.
+  exploit H2; eauto. exploit Mem.nextblock_alloc; eauto. intros ->. blomega.
 Qed.
 
 Lemma match_alloc_variables:
@@ -719,7 +721,8 @@ Proof.
     eapply Mem.valid_new_block; eauto.
     eapply Q; eauto. unfold Mem.valid_block in *.
     exploit Mem.nextblock_alloc. eexact A. exploit Mem.alloc_result. eexact A.
-    unfold block; xomega.
+    intros; subst. rewrite H7. intro LT; apply H3. apply Block.lt_succ_inv in LT.
+    destruct LT; try congruence.
   split. intros. destruct (ident_eq id0 id).
     (* same var *)
     subst id0.
@@ -985,7 +988,8 @@ Proof.
   (* flat *)
   exploit alloc_variables_range. eexact A. eauto.
   rewrite PTree.gempty. intros [P|P]. congruence.
-  exploit K; eauto. unfold Mem.valid_block. xomega.
+  exploit K; eauto. unfold Mem.valid_block.
+  intro LT; elim (Block.lt_strict b'). intuition blomega.
   intros [id0 [ty0 [U [V W]]]]. split; auto.
   destruct (ident_eq id id0). congruence.
   assert (b' <> b').
@@ -1350,11 +1354,11 @@ Qed.
 
 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).
+      (DOMAIN: forall b, Block.lt b bound -> f b = Some(b, 0))
+      (IMAGE: forall b1 b2 delta, f b1 = Some(b2, delta) -> Block.lt b2 bound -> b1 = b2)
+      (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> Block.lt b bound)
+      (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> Block.lt b bound)
+      (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> Block.lt b bound).
 
 Lemma match_globalenvs_preserves_globals:
   forall f,
@@ -1531,7 +1535,7 @@ End EVAL_EXPR.
 
 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_globalenvs f hi -> Block.le hi bound -> Block.le hi 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 ->
@@ -1558,7 +1562,7 @@ Inductive match_cont (f: meminj): compilenv -> cont -> cont -> mem -> block -> b
       match_envs f (cenv_for fn) e le m lo hi te tle tlo thi ->
       match_cont f (cenv_for fn) k tk m lo tlo ->
       check_opttemp (cenv_for fn) optid = OK x ->
-      Ple hi bound -> Ple thi tbound ->
+      Block.le hi bound -> Block.le thi tbound ->
       match_cont f cenv (Kcall optid fn e le k)
                         (Kcall optid tfn te tle tk) m bound tbound.
 
@@ -1568,26 +1572,26 @@ Lemma match_cont_invariant:
   forall f' m' f cenv k tk m bound tbound,
   match_cont f cenv k tk m bound tbound ->
   (forall b chunk v,
-    f b = None -> Plt b bound -> Mem.load chunk m b 0 = Some v -> Mem.load chunk m' b 0 = Some v) ->
+    f b = None -> Block.lt b bound -> Mem.load chunk m b 0 = Some v -> Mem.load chunk m' b 0 = Some v) ->
   inject_incr f f' ->
-  (forall b, Plt b bound -> f' b = f b) ->
-  (forall b b' delta, f' b = Some(b', delta) -> Plt b' tbound -> f' b = f b) ->
+  (forall b, Block.lt b bound -> f' b = f b) ->
+  (forall b b' delta, f' b = Some(b', delta) -> Block.lt b' tbound -> f' b = f b) ->
   match_cont f' cenv k tk m' bound tbound.
 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. xomega.
+  assert (f b1 = Some (b2, delta)). rewrite <- H; symmetry; eapply INJ2; eauto. blomega.
   eapply IMAGE; eauto.
 (* call *)
   eapply match_envs_invariant; eauto.
-  intros. apply LOAD; auto. xomega.
-  intros. apply INJ1; auto; xomega.
-  intros. eapply INJ2; eauto; xomega.
+  intros. apply LOAD; auto. intuition blomega.
+  intros. apply INJ1; auto; intuition blomega.
+  intros. eapply INJ2; eauto; intuition blomega.
   eapply IHmatch_cont; eauto.
-  intros; apply LOAD; auto. inv H0; xomega.
-  intros; apply INJ1. inv H0; xomega.
-  intros; eapply INJ2; eauto. inv H0; xomega.
+  intros; apply LOAD; auto. inv H0; intuition blomega.
+  intros; apply INJ1. inv H0; intuition blomega.
+  intros; eapply INJ2; eauto. inv H0; intuition blomega.
 Qed.
 
 (** Invariance by assignment to location "above" *)
@@ -1596,15 +1600,15 @@ Lemma match_cont_assign_loc:
   forall f cenv k tk m bound tbound ty loc ofs v m',
   match_cont f cenv k tk m bound tbound ->
   assign_loc ge ty m loc ofs v m' ->
-  Ple bound loc ->
+  Block.le bound loc ->
   match_cont f cenv k tk m' bound tbound.
 Proof.
   intros. eapply match_cont_invariant; eauto.
   intros. rewrite <- H4. inv H0.
   (* scalar *)
-  simpl in H6. eapply Mem.load_store_other; eauto. left. unfold block; xomega.
+  simpl in H6. eapply Mem.load_store_other; eauto. left. unfold block; blomega.
   (* block copy *)
-  eapply Mem.load_storebytes_other; eauto. left. unfold block; xomega.
+  eapply Mem.load_storebytes_other; eauto. left. unfold block; blomega.
 Qed.
 
 (** Invariance by external calls *)
@@ -1615,16 +1619,16 @@ Lemma match_cont_extcall:
   Mem.unchanged_on (loc_unmapped f) m m' ->
   inject_incr f f' ->
   inject_separated f f' m tm ->
-  Ple bound (Mem.nextblock m) -> Ple tbound (Mem.nextblock tm) ->
+  Block.le bound (Mem.nextblock m) -> Block.le tbound (Mem.nextblock tm) ->
   match_cont f' cenv k tk m' bound tbound.
 Proof.
   intros. eapply match_cont_invariant; eauto.
   intros. eapply Mem.load_unchanged_on; eauto.
   red in H2. intros. destruct (f b) as [[b' delta] | ] eqn:?. auto.
   destruct (f' b) as [[b' delta] | ] eqn:?; auto.
-  exploit H2; eauto. unfold Mem.valid_block. intros [A B]. xomegaContradiction.
+  exploit H2; eauto. unfold Mem.valid_block. intros [A B]. exfalso; intuition blomega.
   red in H2. intros. destruct (f b) as [[b'' delta''] | ] eqn:?. auto.
-  exploit H2; eauto. unfold Mem.valid_block. intros [A B]. xomegaContradiction.
+  exploit H2; eauto. unfold Mem.valid_block. intros [A B]. exfalso; intuition blomega.
 Qed.
 
 (** Invariance by change of bounds *)
@@ -1633,10 +1637,10 @@ Lemma match_cont_incr_bounds:
   forall f cenv k tk m bound tbound,
   match_cont f cenv k tk m bound tbound ->
   forall bound' tbound',
-  Ple bound bound' -> Ple tbound tbound' ->
+  Block.le bound bound' -> Block.le tbound tbound' ->
   match_cont f cenv k tk m bound' tbound'.
 Proof.
-  induction 1; intros; econstructor; eauto; xomega.
+  induction 1; intros; econstructor; eauto; blomega.
 Qed.
 
 (** [match_cont] and call continuations. *)
@@ -1683,22 +1687,22 @@ Qed.
 Remark free_list_load:
   forall chunk b' l m m',
   Mem.free_list m l = Some m' ->
-  (forall b lo hi, In (b, lo, hi) l -> Plt b' b) ->
+  (forall b lo hi, In (b, lo, hi) l -> Block.lt b' b) ->
   Mem.load chunk m' b' 0 = Mem.load chunk m b' 0.
 Proof.
   induction l; simpl; intros.
   inv H; auto.
   destruct a. destruct p. destruct (Mem.free m b z0 z) as [m1|] eqn:?; try discriminate.
   transitivity (Mem.load chunk m1 b' 0). eauto.
-  eapply Mem.load_free. eauto. left. assert (Plt b' b) by eauto. unfold block; xomega.
+  eapply Mem.load_free. eauto. left. assert (Block.lt b' b) by eauto. unfold block; blomega.
 Qed.
 
 Lemma match_cont_free_env:
   forall f cenv e le m lo hi te tle tm tlo thi k tk m' tm',
   match_envs f cenv e le m lo hi te tle tlo thi ->
   match_cont f cenv k tk m lo tlo ->
-  Ple hi (Mem.nextblock m) ->
-  Ple thi (Mem.nextblock tm) ->
+  Block.le hi (Mem.nextblock m) ->
+  Block.le thi (Mem.nextblock tm) ->
   Mem.free_list m (blocks_of_env ge e) = Some m' ->
   Mem.free_list tm (blocks_of_env tge te) = Some tm' ->
   match_cont f cenv k tk m' (Mem.nextblock m') (Mem.nextblock tm').
@@ -1708,9 +1712,9 @@ Proof.
   intros. rewrite <- H7. eapply free_list_load; eauto.
   unfold blocks_of_env; intros. exploit list_in_map_inv; eauto.
   intros [[id [b1 ty]] [P Q]]. simpl in P. inv P.
-  exploit me_range; eauto. eapply PTree.elements_complete; eauto. xomega.
-  rewrite (free_list_nextblock _ _ _ H3). inv H; xomega.
-  rewrite (free_list_nextblock _ _ _ H4). inv H; xomega.
+  exploit me_range; eauto. eapply PTree.elements_complete; eauto. intuition blomega.
+  rewrite (free_list_nextblock _ _ _ H3). inv H; blomega.
+  rewrite (free_list_nextblock _ _ _ H4). inv H; blomega.
 Qed.
 
 (** Matching of global environments *)
@@ -1752,8 +1756,8 @@ Inductive match_states: state -> state -> Prop :=
         (MCONT: match_cont j (cenv_for f) k tk m lo tlo)
         (MINJ: Mem.inject j m tm)
         (COMPAT: compat_cenv (addr_taken_stmt s) (cenv_for f))
-        (BOUND: Ple hi (Mem.nextblock m))
-        (TBOUND: Ple thi (Mem.nextblock tm)),
+        (BOUND: Block.le hi (Mem.nextblock m))
+        (TBOUND: Block.le thi (Mem.nextblock tm)),
       match_states (State f s k e le m)
                    (State tf ts tk te tle tm)
   | match_call_state:
@@ -2018,7 +2022,7 @@ Proof.
   eapply step_Sset_debug. eauto. rewrite typeof_simpl_expr. eauto.
   econstructor; eauto with compat.
   eapply match_envs_assign_lifted; eauto. eapply cast_val_is_casted; eauto.
-  eapply match_cont_assign_loc; eauto. exploit me_range; eauto. xomega.
+  eapply match_cont_assign_loc; eauto. exploit me_range; eauto. intuition blomega.
   inv MV; try congruence. inv H2; try congruence. unfold Mem.storev in H3.
   eapply Mem.store_unmapped_inject; eauto. congruence.
   erewrite assign_loc_nextblock; eauto.
@@ -2068,9 +2072,9 @@ Proof.
   eapply match_envs_set_opttemp; eauto.
   eapply match_envs_extcall; eauto.
   eapply match_cont_extcall; eauto.
-  inv MENV; xomega. inv MENV; xomega.
-  eapply Ple_trans; eauto. eapply external_call_nextblock; eauto.
-  eapply Ple_trans; eauto. eapply external_call_nextblock; eauto.
+  inv MENV; blomega. inv MENV; blomega.
+  eapply Block.le_trans; eauto. eapply external_call_nextblock; eauto.
+  eapply Block.le_trans; eauto. eapply external_call_nextblock; eauto.
 
 (* sequence *)
   econstructor; split. apply plus_one. econstructor.
@@ -2212,11 +2216,11 @@ Proof.
   eapply bind_parameters_load; eauto. intros.
   exploit alloc_variables_range. eexact H1. eauto.
   unfold empty_env. rewrite PTree.gempty. intros [?|?]. congruence.
-  red; intros; subst b'. xomega.
+  red; intros; subst b'. elim (Block.lt_strict b); intuition blomega.
   eapply alloc_variables_load; eauto.
   apply compat_cenv_for.
-  rewrite (bind_parameters_nextblock _ _ _ _ _ _ H2). xomega.
-  rewrite T; xomega.
+  rewrite (bind_parameters_nextblock _ _ _ _ _ _ H2). blomega.
+  rewrite T; blomega.
 
 (* external function *)
   monadInv TRFD. inv FUNTY.
@@ -2227,7 +2231,7 @@ Proof.
   apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   econstructor; eauto.
   intros. apply match_cont_incr_bounds with (Mem.nextblock m) (Mem.nextblock tm).
-  eapply match_cont_extcall; eauto. xomega. xomega.
+  eapply match_cont_extcall; eauto. blomega. blomega.
   eapply external_call_nextblock; eauto.
   eapply external_call_nextblock; eauto.
 
@@ -2258,11 +2262,12 @@ Proof.
   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.
+  unfold Mem.flat_inj in H. destruct (Block.lt_dec 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.
-  xomega. xomega.
+  blomega. blomega.
+  erewrite <- Genv.init_mem_genv_next; eauto.
   eapply Genv.initmem_inject; eauto.
   constructor.
 Qed.
diff --git a/common/AST.v b/common/AST.v
index 145f49190a..d84f4b62b2 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -31,6 +31,8 @@ Definition ident := positive.
 
 Definition ident_eq := peq.
 
+Parameter string_of_ident: ident -> string.
+
 (** The intermediate languages are weakly typed, using the following types: *)
 
 Inductive typ : Type :=
diff --git a/common/BlockNames.v b/common/BlockNames.v
new file mode 100644
index 0000000000..63e5463fa9
--- /dev/null
+++ b/common/BlockNames.v
@@ -0,0 +1,312 @@
+Require Import DecidableClass.
+Require Import Coqlib.
+Require Import AST.
+Require Import Maps.
+Require Import String.
+
+(** * Interface *)
+
+(** This is the interface of the memory block namespace. There should
+  be an embedding [glob] of global identifiers into the type of memory
+  blocks (which can be inverted with the [ident_of] operation).
+  It should also be possible to dynamically allocate block names,
+  starting with [init], then by applying [succ] whenever a new block
+  name is needed.
+
+  The space of block names must be equipped with a total order
+  ([le], [lt]), such that global blocks are considered smaller than
+  dynamically allocated blocks, and that dynamic blocks are allocated
+  in increasing order.
+
+  Finally, it should be possible to print out a string representation
+  for each block name ([to_string]), and there should be an injective
+  mapping into [positive], so that we can use an efficient [IMap]
+  implementation for block-indexed finite maps. *)
+
+Module Type BlockType <: INDEXED_TYPE.
+  Parameter t : Type.
+  Parameter eq : forall b1 b2 : t, {b1 = b2} + {b1 <> b2}.
+
+  Parameter glob : ident -> t.  (* block associated to a global identifier *)
+  Parameter init : t.           (* initial dynamic block id *)
+  Parameter succ : t -> t.
+  Parameter ident_of: t -> option ident.
+  Parameter to_string: t -> string.
+
+  Parameter lt : t -> t -> Prop.
+  Parameter le : t -> t -> Prop.
+  Parameter lt_dec : forall b1 b2, {lt b1 b2} + {~ lt b1 b2}.
+
+  Axiom lt_glob_init : forall i, lt (glob i) init.
+  Axiom lt_succ : forall b, lt b (succ b).
+  Axiom lt_trans : forall x y z, lt x y -> lt y z -> lt x z.
+  Axiom lt_strict : forall b, ~ lt b b.
+  Axiom lt_succ_inv: forall x y, lt x (succ y) -> lt x y \/ x = y.
+  Axiom lt_le: forall x y, lt x y -> le x y.
+  Axiom nlt_le: forall x y, ~ lt y x -> le x y.
+  Axiom le_refl: forall b, le b b.
+  Axiom le_trans: forall x y z, le x y -> le y z -> le x z.
+  Axiom lt_le_trans: forall x y z, lt x y -> le y z -> lt x z.
+  Axiom le_lt_trans: forall x y z, le x y -> lt y z -> lt x z.
+
+  Axiom glob_inj: forall i j, glob i = glob j -> i = j.
+
+  Axiom ident_of_glob: forall i, ident_of (glob i) = Some i.
+  Axiom ident_of_inv: forall b i, ident_of b = Some i -> b = glob i.
+
+  Parameter index: t -> positive.
+  Axiom index_inj: forall (x y: t), index x = index y -> x = y.
+End BlockType.
+
+(** * Implementation *)
+
+(** We get some help from the Ocaml code to convert dynamic block
+  identifiers into strings. *)
+
+Parameter string_of_pos: positive -> string.
+
+(** Block names are implemented as the disjoint union of [AST.ident]
+  and dynamically allocated [positive]. *)
+
+Module Block : BlockType.
+  Inductive t_def :=
+    | glob_def : ident -> t_def
+    | dyn : positive -> t_def.
+
+  Definition t := t_def.
+
+  Definition eq (b1 b2 : t):
+    {b1 = b2} + {b1 <> b2}.
+  Proof.
+    decide equality.
+    apply peq.
+    apply peq.
+  Defined.
+
+  Definition glob := glob_def.
+  Definition init := dyn 1%positive.
+
+  Definition succ (b: t) :=
+    match b with
+      | glob_def i => glob (Pos.succ i)
+      | dyn n => dyn (Pos.succ n)
+    end.
+
+  Inductive lt_def : t -> t -> Prop :=
+    | glob_dyn_lt i n:
+        lt_def (glob i) (dyn n)
+    | glob_lt m n:
+        Pos.lt m n ->
+        lt_def (glob m) (glob n)
+    | dyn_lt m n:
+        Pos.lt m n ->
+        lt_def (dyn m) (dyn n).
+
+  Definition lt := lt_def.
+
+  Definition le b1 b2 :=
+    lt b1 b2 \/ b1 = b2.
+
+  Definition lt_dec b1 b2:
+    {lt b1 b2} + {~ lt b1 b2}.
+  Proof.
+    destruct b1 as [i1|n1], b2 as [i2|n2].
+    - destruct (plt i1 i2).
+      + left. abstract (constructor; eauto).
+      + right. abstract (inversion 1; eauto).
+    - left. abstract constructor.
+    - right. abstract (inversion 1).
+    - destruct (plt n1 n2).
+      + left. abstract (constructor; eauto).
+      + right. abstract (inversion 1; eauto).
+  Defined.
+
+  Lemma lt_glob_init i:
+    lt (glob i) init.
+  Proof.
+    constructor.
+  Qed.
+
+  Lemma lt_succ b:
+    lt b (succ b).
+  Proof.
+    destruct b; constructor; xomega.
+  Qed.
+
+  Lemma lt_trans x y z:
+    lt x y -> lt y z -> lt x z.
+  Proof.
+    intros Hxy Hyz.
+    destruct Hyz; inv Hxy; constructor; xomega.
+  Qed.
+
+  Lemma lt_strict b:
+    ~ lt b b.
+  Proof.
+    inversion 1; eapply Plt_strict; eauto.
+  Qed.
+
+  Lemma lt_succ_inv x y:
+    lt x (succ y) -> lt x y \/ x = y.
+  Proof.
+    destruct y; simpl; inversion 1; subst.
+    - destruct (Plt_succ_inv m i) as [H1|H1]; auto.
+      left; constructor; auto.
+      right; subst; reflexivity.
+    - left; constructor.
+    - destruct (Plt_succ_inv m p) as [H1|H1]; auto.
+      left; constructor; auto.
+      right; subst; reflexivity.
+  Qed.
+
+  Lemma lt_le x y:
+    lt x y -> le x y.
+  Proof.
+    firstorder.
+  Qed.
+
+  Lemma nlt_le x y:
+    ~ lt y x -> le x y.
+  Proof.
+    unfold le.
+    destruct x as [i1|n1], y as [i2|n2].
+    - destruct (peq i1 i2).
+      + right. congruence.
+      + left. constructor.
+        destruct (plt i1 i2); auto. elim H; constructor; xomega.
+    - left. constructor.
+    - intro. elim H. constructor.
+    - destruct (peq n1 n2).
+      + right. congruence.
+      + left. constructor.
+        destruct (plt n1 n2); auto. elim H; constructor; xomega.
+  Qed.
+
+  Lemma le_refl b:
+    le b b.
+  Proof.
+    firstorder.
+  Qed.
+
+  Lemma le_trans x y z:
+    le x y -> le y z -> le x z.
+  Proof.
+    unfold le. intros H1 H2.
+    destruct H1; try congruence. left.
+    destruct H2; try congruence. eauto using lt_trans.
+  Qed.
+
+  Lemma lt_le_trans x y z:
+    lt x y -> le y z -> lt x z.
+  Proof.
+    intros Hxy Hyz.
+    destruct Hyz; try congruence.
+    eapply lt_trans; eauto.
+  Qed.
+
+  Lemma le_lt_trans x y z:
+    le x y -> lt y z -> lt x z.
+  Proof.
+    intros Hxy Hyz.
+    destruct Hxy; try congruence.
+    eapply lt_trans; eauto.
+  Qed.
+
+  Definition ident_of b :=
+    match b with
+      glob_def i => Some i
+    | dyn i => None
+    end.
+
+  Definition to_string (b: t): string :=
+    match b with
+    | glob_def i => append "glob:" (string_of_ident i)
+    | dyn b => append "dyn:" (string_of_pos b)
+    end.
+
+  Lemma ident_of_glob i:
+    ident_of (glob i) = Some i.
+  Proof.
+    reflexivity.
+  Qed.
+
+  Lemma ident_of_inv b i:
+    ident_of b = Some i -> b = glob i.
+  Proof.
+    unfold ident_of. destruct b; inversion 1; reflexivity.
+  Qed.
+
+  Lemma glob_inj i j:
+    glob i = glob j -> i = j.
+  Proof.
+    inversion 1; auto.
+  Qed.
+
+  Definition index (b: t): positive :=
+    match b with
+    | glob_def i => i~0
+    | dyn p => p~1
+    end.
+
+  Lemma index_inj (x y: t):
+    index x = index y -> x = y.
+  Proof.
+    destruct x, y; inversion 1; simpl in *; congruence.
+  Qed.
+End Block.
+
+Module BMap : MAP
+    with Definition elt := Block.t
+    with Definition elt_eq := Block.eq :=
+  IMap Block.
+
+(** * Complements *)
+
+(** ** Properties *)
+
+Lemma Blt_trans_succ b1 b2:
+  Block.lt b1 b2 -> Block.lt b1 (Block.succ b2).
+Proof.
+  intros H.
+  eapply Block.lt_trans; eauto.
+  apply Block.lt_succ.
+Qed.
+
+Lemma Blt_ne x y:
+  Block.lt x y -> x <> y.
+Proof.
+  intros LT EQ; subst; apply Block.lt_strict in LT; auto.
+Qed.
+
+(** ** Derived definitions *)
+
+Program Instance Decidable_eq_block (x y: Block.t): Decidable (x = y) :=
+  {
+    Decidable_witness := if Block.eq x y then true else false;
+  }.
+Next Obligation.
+  destruct Block.eq; firstorder.
+Qed.
+
+Definition block_compare (b1 b2: Block.t) :=
+  if Block.lt_dec b1 b2
+  then (-1)%Z
+  else if Block.eq b1 b2
+       then 0%Z
+       else 1%Z.
+
+(** ** Tactics *)
+
+(** This tactic is used to discharge inequalities involving block names. *)
+
+Hint Resolve
+  Block.lt_le_trans
+  Block.le_lt_trans
+  Block.le_trans
+  Block.lt_le
+  Blt_ne
+  Block.le_refl
+  Block.lt_succ
+  : blocknames.
+
+Ltac blomega := eauto with blocknames.
diff --git a/common/Events.v b/common/Events.v
index b2335b9600..1e7f419a34 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -1460,12 +1460,12 @@ Definition external_call_determ ef := ec_determ (external_call_spec ef).
 Lemma external_call_nextblock:
   forall ef ge vargs m1 t vres m2,
   external_call ef ge vargs m1 t vres m2 ->
-  Ple (Mem.nextblock m1) (Mem.nextblock m2).
+  Block.le (Mem.nextblock m1) (Mem.nextblock m2).
 Proof.
-  intros. destruct (plt (Mem.nextblock m2) (Mem.nextblock m1)).
+  intros. destruct (Block.lt_dec (Mem.nextblock m2) (Mem.nextblock m1)).
   exploit external_call_valid_block; eauto. intros.
-  eelim Plt_strict; eauto.
-  unfold Plt, Ple in *; zify; omega.
+  eelim Block.lt_strict; eauto.
+  apply Block.nlt_le; eauto.
 Qed.
 
 (** Special case of [external_call_mem_inject_gen] (for backward compatibility) *)
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index d37fbd4637..287d2879ca 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -77,7 +77,6 @@ Record t: Type := mksenv {
   public_symbol: ident -> bool;
   invert_symbol: block -> option ident;
   block_is_volatile: block -> bool;
-  nextblock: block;
   (** Properties *)
   find_symbol_injective:
     forall id1 id2 b, find_symbol id1 = Some b -> find_symbol id2 = Some b -> id1 = id2;
@@ -88,9 +87,9 @@ Record t: Type := mksenv {
   public_symbol_exists:
     forall id, public_symbol id = true -> exists b, find_symbol id = Some b;
   find_symbol_below:
-    forall id b, find_symbol id = Some b -> Plt b nextblock;
+    forall id b, find_symbol id = Some b -> Block.lt b Block.init;
   block_is_volatile_below:
-    forall b, block_is_volatile b = true -> Plt b nextblock
+    forall b, block_is_volatile b = true -> Block.lt b Block.init;
 }.
 
 Definition symbol_address (ge: t) (id: ident) (ofs: ptrofs) : val :=
@@ -146,13 +145,7 @@ Variable V: Type.  (**r The type of information attached to variables *)
 
 Record t: Type := mkgenv {
   genv_public: list ident;              (**r which symbol names are public *)
-  genv_symb: PTree.t block;             (**r mapping symbol -> block *)
-  genv_defs: PTree.t (globdef F V);     (**r mapping block -> definition *)
-  genv_next: block;                     (**r next symbol pointer *)
-  genv_symb_range: forall id b, PTree.get id genv_symb = Some b -> Plt b genv_next;
-  genv_defs_range: forall b g, PTree.get b genv_defs = Some g -> Plt b genv_next;
-  genv_vars_inj: forall id1 id2 b,
-    PTree.get id1 genv_symb = Some b -> PTree.get id2 genv_symb = Some b -> id1 = id2
+  genv_defs: PTree.t (globdef F V);     (**r mapping ident -> definition *)
 }.
 
 (** ** Lookup functions *)
@@ -160,7 +153,36 @@ Record t: Type := mkgenv {
 (** [find_symbol ge id] returns the block associated with the given name, if any *)
 
 Definition find_symbol (ge: t) (id: ident) : option block :=
-  PTree.get id ge.(genv_symb).
+  match ge.(genv_defs) ! id with
+  | Some _ => Some (Block.glob id)
+  | None => None
+  end.
+
+Theorem genv_symb_range:
+  forall ge id b,
+  find_symbol ge id = Some b ->
+  Block.lt b Block.init.
+Proof.
+  intros until b.
+  unfold find_symbol.
+  destruct (_ ! id); try discriminate.
+  inversion 1.
+  apply Block.lt_glob_init.
+Qed.
+
+Theorem genv_vars_inj:
+  forall ge id1 id2 b,
+  find_symbol ge id1 = Some b ->
+  find_symbol ge id2 = Some b ->
+  id1 = id2.
+Proof.
+  unfold find_symbol.
+  intros.
+  destruct (_ ! id1); try discriminate.
+  destruct (_ ! id2); try discriminate.
+  apply Block.glob_inj.
+  congruence.
+Qed.
 
 (** [symbol_address ge id ofs] returns a pointer into the block associated
   with [id], at byte offset [ofs].  [Vundef] is returned if no block is associated
@@ -183,7 +205,23 @@ Definition public_symbol (ge: t) (id: ident) : bool :=
 (** [find_def ge b] returns the global definition associated with the given address. *)
 
 Definition find_def (ge: t) (b: block) : option (globdef F V) :=
-  PTree.get b ge.(genv_defs).
+  match Block.ident_of b with
+    Some i => PTree.get i ge.(genv_defs)
+  | None => None
+  end.
+
+Theorem genv_defs_range:
+  forall ge id b,
+  find_def ge id = Some b ->
+  Block.lt id Block.init.
+Proof.
+  intros until b.
+  unfold find_def.
+  destruct (Block.ident_of id) eqn:Hb; try discriminate.
+  intros _.
+  apply Block.ident_of_inv in Hb; subst.
+  apply Block.lt_glob_init.
+Qed.
 
 (** [find_funct_ptr ge b] returns the function description associated with
     the given address. *)
@@ -203,9 +241,10 @@ Definition find_funct (ge: t) (v: val) : option F :=
 (** [invert_symbol ge b] returns the name associated with the given block, if any *)
 
 Definition invert_symbol (ge: t) (b: block) : option ident :=
-  PTree.fold
-    (fun res id b' => if eq_block b b' then Some id else res)
-    ge.(genv_symb) None.
+  match Block.ident_of b with
+  | Some i => if ge.(genv_defs) ! i then Some i else None
+  | None => None
+  end.
 
 (** [find_var_info ge b] returns the information attached to the variable
    at address [b]. *)
@@ -224,33 +263,10 @@ Definition block_is_volatile (ge: t) (b: block) : bool :=
 
 (** ** Constructing the global environment *)
 
-Program Definition add_global (ge: t) (idg: ident * globdef F V) : t :=
+Definition add_global (ge: t) (idg: ident * globdef F V) : t :=
   @mkgenv
     ge.(genv_public)
-    (PTree.set idg#1 ge.(genv_next) ge.(genv_symb))
-    (PTree.set ge.(genv_next) idg#2 ge.(genv_defs))
-    (Pos.succ ge.(genv_next))
-    _ _ _.
-Next Obligation.
-  destruct ge; simpl in *.
-  rewrite PTree.gsspec in H. destruct (peq id i). inv H. apply Plt_succ.
-  apply Plt_trans_succ; eauto.
-Qed.
-Next Obligation.
-  destruct ge; simpl in *.
-  rewrite PTree.gsspec in H. destruct (peq b genv_next0).
-  inv H. apply Plt_succ.
-  apply Plt_trans_succ; eauto.
-Qed.
-Next Obligation.
-  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.
-  inv H0. eelim Plt_strict. eapply genv_symb_range0; eauto.
-  eauto.
-Qed.
+    (PTree.set idg#1 idg#2 ge.(genv_defs)).
 
 Definition add_globals (ge: t) (gl: list (ident * globdef F V)) : t :=
   List.fold_left add_global gl ge.
@@ -262,17 +278,8 @@ Proof.
   intros. apply fold_left_app.
 Qed.
 
-Program Definition empty_genv (pub: list ident): t :=
-  @mkgenv pub (PTree.empty _) (PTree.empty _) 1%positive _ _ _.
-Next Obligation.
-  rewrite PTree.gempty in H. discriminate.
-Qed.
-Next Obligation.
-  rewrite PTree.gempty in H. discriminate.
-Qed.
-Next Obligation.
-  rewrite PTree.gempty in H. discriminate.
-Qed.
+Definition empty_genv (pub: list ident): t :=
+  @mkgenv pub (PTree.empty _).
 
 Definition globalenv (p: program F V) :=
   add_globals (empty_genv p.(prog_public)) p.(prog_defs).
@@ -421,7 +428,7 @@ Theorem find_def_symbol:
   (prog_defmap p)!id = Some g <-> exists b, find_symbol (globalenv p) id = Some b /\ find_def (globalenv p) b = Some g.
 Proof.
   intros.
-  set (P := fun m ge => m!id = Some g <-> exists b, find_symbol ge id = Some b /\ find_def ge b = Some g).
+  set (P := fun m ge => m!id = ge.(genv_defs)!id).
   assert (REC: forall l m ge,
             P m ge ->
             P (fold_left (fun m idg => PTree.set idg#1 idg#2 m) l m)
@@ -429,20 +436,17 @@ Proof.
   { induction l as [ | [id1 g1] l]; intros; simpl.
   - auto.
   - apply IHl. unfold P, add_global, find_symbol, find_def; simpl.
-    rewrite ! PTree.gsspec. destruct (peq id id1).
-    + subst id1. split; intros.
-      inv H0. exists (genv_next ge); split; auto. apply PTree.gss.
-      destruct H0 as (b & A & B). inv A. rewrite PTree.gss in B. auto.
-    + red in H; rewrite H. split.
-      intros (b & A & B). exists b; split; auto. rewrite PTree.gso; auto.
-      apply Plt_ne. eapply genv_symb_range; eauto.
-      intros (b & A & B). rewrite PTree.gso in B. exists b; auto.
-      apply Plt_ne. eapply genv_symb_range; eauto.
+    rewrite ! PTree.gsspec. destruct (peq id id1); auto.
   }
-  apply REC. unfold P, find_symbol, find_def; simpl.
-  rewrite ! PTree.gempty. split.
-  congruence.
-  intros (b & A & B); congruence.
+  setoid_rewrite REC. instantiate (1 := empty_genv (prog_public p)).
+  - unfold globalenv, find_symbol, find_def. clear.
+    split.
+    + exists (Block.glob id). rewrite Block.ident_of_glob.
+      destruct PTree.get; eauto. discriminate.
+    + intros (b & Hb & Hg).
+      destruct PTree.get eqn:H; try discriminate.
+      inv Hb. rewrite Block.ident_of_glob in Hg. congruence.
+  - unfold P. rewrite !PTree.gempty. reflexivity.
 Qed.
 
 Theorem find_symbol_exists:
@@ -480,11 +484,14 @@ Proof.
   intros until g. unfold globalenv. apply add_globals_preserves.
 (* preserves *)
   unfold find_def; simpl; intros.
-  rewrite PTree.gsspec in H1. destruct (peq b (genv_next ge)).
+  destruct (Block.ident_of b) eqn:Hb; try congruence.
+  rewrite PTree.gsspec in H1. destruct (peq i id).
   inv H1. exists id; auto.
   auto.
 (* base *)
-  unfold find_def; simpl; intros. rewrite PTree.gempty in H. discriminate.
+  unfold find_def; simpl; intros.
+  destruct (Block.ident_of b) eqn: Hb; try congruence.
+  rewrite PTree.gempty in H. discriminate.
 Qed.
 
 Corollary find_funct_ptr_inversion:
@@ -530,7 +537,12 @@ 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.
+  unfold find_symbol in *.
+  destruct (_ ! id1); try discriminate.
+  destruct (_ ! id2); try discriminate.
+  apply Block.glob_inj.
+  congruence.
 Qed.
 
 Theorem invert_find_symbol:
@@ -538,44 +550,20 @@ Theorem invert_find_symbol:
   invert_symbol ge b = Some id -> find_symbol ge id = Some b.
 Proof.
   intros until b; unfold find_symbol, invert_symbol.
-  apply PTree_Properties.fold_rec.
-  intros. rewrite H in H0; auto.
-  congruence.
-  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.
+  destruct (Block.ident_of b) eqn:Hb; try discriminate.
+  apply Block.ident_of_inv in Hb; subst.
+  destruct (_ ! i) eqn:Hi; try discriminate.
+  inversion 1. subst. rewrite Hi. reflexivity.
 Qed.
 
 Theorem find_invert_symbol:
   forall ge id b,
   find_symbol ge id = Some b -> invert_symbol ge b = Some id.
 Proof.
-  intros until b.
-  assert (find_symbol ge id = Some b -> exists id', invert_symbol ge b = Some id').
-  unfold find_symbol, invert_symbol.
-  apply PTree_Properties.fold_rec.
-  intros. rewrite H in H0; auto.
-  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.
-
-  intros; exploit H; eauto. intros [id' A].
-  assert (id = id'). eapply genv_vars_inj; eauto. apply invert_find_symbol; auto.
-  congruence.
-Qed.
-
-Definition advance_next (gl: list (ident * globdef F V)) (x: positive) :=
-  List.fold_left (fun n g => Pos.succ n) gl x.
-
-Remark genv_next_add_globals:
-  forall gl ge,
-  genv_next (add_globals ge gl) = advance_next gl (genv_next ge).
-Proof.
-  induction gl; simpl; intros.
-  auto.
-  rewrite IHgl. auto.
+  intros until b; unfold find_symbol, invert_symbol.
+  destruct (_ ! id) eqn:Hid; try discriminate.
+  intros H. inv H. rewrite Block.ident_of_glob.
+  rewrite Hid. reflexivity.
 Qed.
 
 Remark genv_public_add_globals:
@@ -594,10 +582,12 @@ Proof.
 Qed.
 
 Theorem block_is_volatile_below:
-  forall ge b, block_is_volatile ge b = true ->  Plt b ge.(genv_next).
+  forall ge b, block_is_volatile ge b = true -> Block.lt b Block.init.
 Proof.
   unfold block_is_volatile; intros. destruct (find_var_info ge b) as [gv|] eqn:FV.
-  rewrite find_var_info_iff in FV. eapply genv_defs_range; eauto.
+  rewrite find_var_info_iff in FV.
+  unfold find_def in FV. destruct (Block.ident_of b) eqn:Hb; try discriminate.
+  apply Block.ident_of_inv in Hb; subst. apply Block.lt_glob_init.
   discriminate.
 Qed.
 
@@ -609,7 +599,6 @@ Definition to_senv (ge: t) : Senv.t :=
     (public_symbol ge)
     (invert_symbol ge)
     (block_is_volatile ge)
-    ge.(genv_next)
     ge.(genv_vars_inj)
     (invert_find_symbol ge)
     (find_invert_symbol ge)
@@ -658,12 +647,14 @@ Definition perm_globvar (gv: globvar V) : permission :=
 Definition alloc_global (m: mem) (idg: ident * globdef F V): option mem :=
   match idg with
   | (id, Gfun f) =>
-      let (m1, b) := Mem.alloc m 0 1 in
+      let b := Block.glob id in
+      let m1 := Mem.alloc_at m b 0 1 in
       Mem.drop_perm m1 b 0 1 Nonempty
   | (id, Gvar v) =>
       let init := v.(gvar_init) in
       let sz := init_data_list_size init in
-      let (m1, b) := Mem.alloc m 0 sz in
+      let b := Block.glob id in
+      let m1 := Mem.alloc_at m b 0 sz in
       match store_zeros m1 b 0 sz with
       | None => None
       | Some m2 =>
@@ -722,34 +713,34 @@ Qed.
 Remark alloc_global_nextblock:
   forall g m m',
   alloc_global m g = Some m' ->
-  Mem.nextblock m' = Pos.succ(Mem.nextblock m).
+  Mem.nextblock m' = Mem.nextblock m.
 Proof.
   unfold alloc_global. intros.
   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.
+  apply Mem.nextblock_drop in H. rewrite H. eapply Mem.nextblock_alloc_at; auto.
   (* variable *)
   set (init := gvar_init v) in *.
   set (sz := init_data_list_size init) in *.
-  destruct (Mem.alloc m 0 sz) as [m1 b] eqn:?.
+  set (b := Block.glob id) in *.
+  set (m1 := Mem.alloc_at m b 0 sz) in *.
   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.
-  erewrite Mem.nextblock_drop; eauto.
-  erewrite store_init_data_list_nextblock; eauto.
-  erewrite store_zeros_nextblock; eauto.
-  erewrite Mem.nextblock_alloc; eauto.
+  apply Mem.nextblock_drop in H. rewrite H.
+  apply store_init_data_list_nextblock in Heqo0. rewrite Heqo0.
+  apply store_zeros_nextblock in Heqo. rewrite Heqo.
+  unfold m1; erewrite Mem.nextblock_alloc_at; eauto.
 Qed.
 
 Remark alloc_globals_nextblock:
   forall gl m m',
   alloc_globals m gl = Some m' ->
-  Mem.nextblock m' = advance_next gl (Mem.nextblock m).
+  Mem.nextblock m' = Mem.nextblock m.
 Proof.
   induction gl; simpl; intros.
   congruence.
   destruct (alloc_global m a) as [m1|] eqn:?; try discriminate.
-  erewrite IHgl; eauto. erewrite alloc_global_nextblock; eauto.
+  erewrite (IHgl m1 m'); eauto. erewrite alloc_global_nextblock; eauto.
 Qed.
 
 (** Permissions *)
@@ -793,51 +784,6 @@ Proof.
   eapply IHidl; eauto.
 Qed.
 
-Remark alloc_global_perm:
-  forall k prm b' q idg m m',
-  alloc_global m idg = Some m' ->
-  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.
-  (* function *)
-  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.
-  (* variable *)
-  set (init := gvar_init v) in *.
-  set (sz := init_data_list_size init) in *.
-  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.
-  assert (b' <> b). apply Mem.valid_not_valid_diff with m; eauto with mem.
-  split; intros.
-  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_4; eauto.
-  erewrite store_zeros_perm; [idtac|eauto].
-  erewrite store_init_data_list_perm; [idtac|eauto].
-  eapply Mem.perm_drop_4; eauto.
-Qed.
-
-Remark alloc_globals_perm:
-  forall k prm b' q gl m m',
-  alloc_globals m gl = Some m' ->
-  Mem.valid_block m b' ->
-  (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm).
-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.
-  unfold Mem.valid_block in *. erewrite alloc_global_nextblock; eauto.
-  apply Plt_trans_succ; auto.
-Qed.
-
 (** Data preservation properties *)
 
 Remark store_zeros_unchanged:
@@ -1109,47 +1055,36 @@ Qed.
 Remark alloc_global_unchanged:
   forall (P: block -> Z -> Prop) m id g m',
   alloc_global m (id, g) = Some m' ->
+  (forall ofs, ~ P (Block.glob id) ofs) ->
   Mem.unchanged_on P m m'.
 Proof.
   intros. destruct g as [f|v]; simpl in H.
 - (* function *)
-  destruct (Mem.alloc m 0 1) as [m1 b] eqn:?.
+  set (b := Block.glob id) in *.
+  set (m1 := Mem.alloc_at m b 0 1) in *.
   set (Q := fun b' (ofs: Z) => b' <> b).
   apply Mem.unchanged_on_implies with Q.
   apply Mem.unchanged_on_trans with m1.
-  eapply Mem.alloc_unchanged_on; eauto.
+  eapply Mem.alloc_at_unchanged_on; eauto. reflexivity.
   eapply Mem.drop_perm_unchanged_on; eauto.
-  intros; red. apply Mem.valid_not_valid_diff with m; eauto with mem.
+  intros; red. intro; subst; eapply H0; eauto.
 - (* variable *)
   set (init := gvar_init v) in *.
   set (sz := init_data_list_size init) in *.
-  destruct (Mem.alloc m 0 sz) as [m1 b] eqn:?.
+  set (b := Block.glob id) in *.
+  set (m1 := Mem.alloc_at m b 0 sz) in *.
   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.
   set (Q := fun b' (ofs: Z) => b' <> b).
   apply Mem.unchanged_on_implies with Q.
   apply Mem.unchanged_on_trans with m1.
-  eapply Mem.alloc_unchanged_on; eauto.
+  eapply Mem.alloc_at_unchanged_on; eauto. reflexivity.
   apply Mem.unchanged_on_trans with m2.
   eapply store_zeros_unchanged; eauto.
   apply Mem.unchanged_on_trans with m3.
   eapply store_init_data_list_unchanged; eauto.
   eapply Mem.drop_perm_unchanged_on; eauto.
-  intros; red. apply Mem.valid_not_valid_diff with m; eauto with mem.
-Qed.
-
-Remark alloc_globals_unchanged:
-  forall (P: block -> Z -> Prop) gl m m',
-  alloc_globals m gl = Some m' ->
-  Mem.unchanged_on P m m'.
-Proof.
-  induction gl; simpl; intros.
-- inv H. apply Mem.unchanged_on_refl.
-- destruct (alloc_global m a) as [m''|] eqn:?; try discriminate.
-  destruct a as [id g].
-  apply Mem.unchanged_on_trans with m''.
-  eapply alloc_global_unchanged; eauto.
-  apply IHgl; auto.
+  intros; red. intro; subst; eapply H0; eauto.
 Qed.
 
 Remark load_store_init_data_invariant:
@@ -1180,37 +1115,35 @@ Definition globals_initialized (g: t) (m: mem) :=
 
 Lemma alloc_global_initialized:
   forall g m id gd m',
-  genv_next g = Mem.nextblock m ->
   alloc_global m (id, gd) = Some m' ->
   globals_initialized g m ->
-     globals_initialized (add_global g (id, gd)) m'
-  /\ genv_next (add_global g (id, gd)) = Mem.nextblock m'.
+  globals_initialized (add_global g (id, gd)) m'.
 Proof.
-  intros.
-  exploit alloc_global_nextblock; eauto. intros NB. split.
+  intros g m id gd m' AG GI.
 - (* globals-initialized *)
-  red; intros. unfold find_def in H2; simpl in H2.
-  rewrite PTree.gsspec in H2. destruct (peq b (genv_next g)).
-+ inv H2. destruct gd0 as [f|v]; simpl in H0.
-* destruct (Mem.alloc m 0 1) as [m1 b] eqn:ALLOC.
-  exploit Mem.alloc_result; eauto. intros RES.
-  rewrite H, <- RES. split.
+  red; intros b gd0 FD.
+  unfold find_def in FD; simpl in FD.
+  destruct (Block.ident_of b) eqn: Hb; try congruence.
+  rewrite PTree.gsspec in FD. destruct (peq i id).
++ inv FD. destruct gd0 as [f|v]; simpl in AG.
+* apply Block.ident_of_inv in Hb; subst.
+  split.
   eapply Mem.perm_drop_1; eauto. omega.
-  intros.
-  assert (0 <= ofs < 1). { eapply Mem.perm_alloc_3; eauto. eapply Mem.perm_drop_4; eauto. }
+  intros ofs k p PERM.
+  assert (0 <= ofs < 1). { eapply Mem.perm_alloc_at_3; eauto. eapply Mem.perm_drop_4; eauto. }
   exploit Mem.perm_drop_2; eauto. intros ORD.
   split. omega. inv ORD; auto.
-* set (init := gvar_init v) in *.
+* apply Block.ident_of_inv in Hb; subst.
+  set (b := Block.glob id) in *.
+  set (init := gvar_init v) in *.
   set (sz := init_data_list_size init) in *.
-  destruct (Mem.alloc m 0 sz) as [m1 b] eqn:?.
+  set (m1 := Mem.alloc_at m b 0 sz) in *.
   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.
-  replace (genv_next g) 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.
+  { eapply Mem.perm_alloc_at_3; eauto.
     erewrite store_zeros_perm by eauto.
     erewrite store_init_data_list_perm by eauto.
     eapply Mem.perm_drop_4; eauto. }
@@ -1227,35 +1160,41 @@ Proof.
   unfold perm_globvar. rewrite NOTVOL. destruct (gvar_readonly v); auto with mem.
   eapply store_init_data_list_loadbytes; eauto.
   eapply store_zeros_loadbytes; eauto.
-+ assert (U: Mem.unchanged_on (fun _ _ => True) m m') by (eapply alloc_global_unchanged; eauto).
++ assert (U: Mem.unchanged_on (fun b' _ => Block.glob id <> b') m m')
+    by (eapply alloc_global_unchanged; eauto).
   assert (VALID: Mem.valid_block m b).
-  { red. rewrite <- H. eapply genv_defs_range; eauto. }
-  exploit H1; eauto.
+  { red. apply Block.ident_of_inv in Hb; subst.
+    eapply Block.lt_le_trans. apply Block.lt_glob_init.
+    apply Mem.init_nextblock. }
+  exploit GI; eauto. unfold find_def. rewrite Hb; eauto.
+  assert (DIFF: b <> Block.glob id).
+  {
+    apply Block.ident_of_inv in Hb; subst.
+    intro GlobEq; apply Block.glob_inj in GlobEq; congruence.
+  }
   destruct gd0 as [f|v].
 * intros [A B]; split; intros.
-  eapply Mem.perm_unchanged_on; eauto. exact I.
-  eapply B. eapply Mem.perm_unchanged_on_2; eauto. exact I.
+  eapply Mem.perm_unchanged_on; eauto. congruence.
+  eapply B. eapply Mem.perm_unchanged_on_2; eauto. congruence.
 * intros (A & B & C & D). split; [| split; [| split]].
-  red; intros. eapply Mem.perm_unchanged_on; eauto. exact I.
-  intros. eapply B. eapply Mem.perm_unchanged_on_2; eauto. exact I.
+  red; intros. eapply Mem.perm_unchanged_on; eauto. congruence.
+  intros. eapply B. eapply Mem.perm_unchanged_on_2; eauto. congruence.
   intros. apply load_store_init_data_invariant with m; auto.
-  intros. eapply Mem.load_unchanged_on_1; eauto. intros; exact I.
-  intros. eapply Mem.loadbytes_unchanged_on; eauto. intros; exact I.
-- simpl. congruence.
+  intros. eapply Mem.load_unchanged_on_1; eauto. congruence.
+  intros. eapply Mem.loadbytes_unchanged_on; eauto. congruence.
 Qed.
 
 Lemma alloc_globals_initialized:
   forall gl ge m m',
   alloc_globals m gl = Some m' ->
-  genv_next ge = Mem.nextblock m ->
   globals_initialized ge m ->
   globals_initialized (add_globals ge gl) m'.
 Proof.
   induction gl; simpl; intros.
 - inv H; 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].
-  eapply IHgl; eauto.
+  eapply IHgl. eauto.
+  eapply alloc_global_initialized; eauto.
 Qed.
 
 End INITMEM.
@@ -1265,12 +1204,10 @@ Definition init_mem (p: program F V) :=
 
 Lemma init_mem_genv_next: forall p m,
   init_mem p = Some m ->
-  genv_next (globalenv p) = Mem.nextblock m.
+  Block.init = 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))).
-  fold (globalenv p). simpl genv_next. intros. congruence.
+  exploit alloc_globals_nextblock; eauto.
 Qed.
 
 Theorem find_symbol_not_fresh:
@@ -1288,7 +1225,8 @@ Theorem find_def_not_fresh:
   find_def (globalenv p) b = Some g -> Mem.valid_block m b.
 Proof.
   intros. red. erewrite <- init_mem_genv_next; eauto.
-  eapply genv_defs_range; eauto.
+  unfold find_def in H0. destruct (Block.ident_of b) eqn: Hb; try congruence.
+  apply Block.ident_of_inv in Hb; subst; apply Block.lt_glob_init.
 Qed.
 
 Theorem find_funct_ptr_not_fresh:
@@ -1314,8 +1252,9 @@ Lemma init_mem_characterization_gen:
 Proof.
   intros. apply alloc_globals_initialized with Mem.empty.
   auto.
-  rewrite Mem.nextblock_empty. auto.
-  red; intros. unfold find_def in H0; simpl in H0; rewrite PTree.gempty in H0; discriminate.
+  red; intros. unfold find_def in H0.
+  destruct (Block.ident_of b) eqn: Hb; try congruence.
+  simpl in H0; rewrite PTree.gempty in H0; discriminate.
 Qed.
 
 Theorem init_mem_characterization:
@@ -1350,15 +1289,13 @@ Qed.
 Section INITMEM_INJ.
 
 Variable ge: t.
-Variable thr: block.
-Hypothesis symb_inject: forall id b, find_symbol ge id = Some b -> Plt b thr.
 
 Lemma store_zeros_neutral:
   forall m b p n m',
-  Mem.inject_neutral thr m ->
-  Plt b thr ->
+  Mem.inject_neutral m ->
+  Block.lt b Block.init ->
   store_zeros m b p n = Some m' ->
-  Mem.inject_neutral thr m'.
+  Mem.inject_neutral m'.
 Proof.
   intros until n. functional induction (store_zeros m b p n); intros.
   inv H1; auto.
@@ -1368,26 +1305,28 @@ Qed.
 
 Lemma store_init_data_neutral:
   forall m b p id m',
-  Mem.inject_neutral thr m ->
-  Plt b thr ->
+  Mem.inject_neutral m ->
+  Block.lt b Block.init ->
   store_init_data ge m b p id = Some m' ->
-  Mem.inject_neutral thr m'.
+  Mem.inject_neutral m'.
 Proof.
   intros.
   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.
+  econstructor. unfold Mem.flat_inj. apply pred_dec_true; auto.
+  unfold find_symbol in E. destruct (_ ! i); try discriminate. inv E.
+  apply Block.lt_glob_init.
   rewrite Ptrofs.add_zero. auto.
 Qed.
 
 Lemma store_init_data_list_neutral:
   forall b idl m p m',
-  Mem.inject_neutral thr m ->
-  Plt b thr ->
+  Mem.inject_neutral m ->
+  Block.lt b Block.init ->
   store_init_data_list ge m b p idl = Some m' ->
-  Mem.inject_neutral thr m'.
+  Mem.inject_neutral m'.
 Proof.
   induction idl; simpl; intros.
   congruence.
@@ -1398,51 +1337,40 @@ Qed.
 Lemma alloc_global_neutral:
   forall idg m m',
   alloc_global ge m idg = Some m' ->
-  Mem.inject_neutral thr m ->
-  Plt (Mem.nextblock m) thr ->
-  Mem.inject_neutral thr m'.
+  Mem.inject_neutral m ->
+  Mem.inject_neutral m'.
 Proof.
   intros. destruct idg as [id [f|v]]; simpl in H.
-  (* function *)
-  destruct (Mem.alloc m 0 1) as [m1 b] eqn:?.
-  assert (Plt b thr). rewrite (Mem.alloc_result _ _ _ _ _ Heqp). auto.
+  - (* function *)
+  set (b := Block.glob id) in *.
+  assert (LT: Block.lt b Block.init) by (apply Block.lt_glob_init).
   eapply Mem.drop_inject_neutral; eauto.
-  eapply Mem.alloc_inject_neutral; eauto.
-  (* variable *)
+  eapply Mem.alloc_at_inject_neutral; eauto.
+  - (* variable *)
   set (init := gvar_init v) in *.
   set (sz := init_data_list_size init) in *.
-  destruct (Mem.alloc m 0 sz) as [m1 b] eqn:?.
+  set (b := Block.glob id) in *.
+  set (m1 := Mem.alloc_at m b 0 sz) in *.
   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.
+  assert (Block.lt b Block.init). apply Block.lt_glob_init.
   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 Mem.alloc_inject_neutral; eauto.
-Qed.
-
-Remark advance_next_le: forall gl x, Ple x (advance_next gl x).
-Proof.
-  induction gl; simpl; intros.
-  apply Ple_refl.
-  apply Ple_trans with (Pos.succ x). apply Ple_succ. eauto.
+  eapply Mem.alloc_at_inject_neutral; eauto.
 Qed.
 
 Lemma alloc_globals_neutral:
   forall gl m m',
   alloc_globals ge m gl = Some m' ->
-  Mem.inject_neutral thr m ->
-  Ple (Mem.nextblock m') thr ->
-  Mem.inject_neutral thr m'.
+  Mem.inject_neutral m ->
+  Mem.inject_neutral m'.
 Proof.
   induction gl; intros.
   simpl in *. congruence.
   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 (Pos.succ (Mem.nextblock m)) (Mem.nextblock m')).
-  { rewrite EQ. apply advance_next_le. }
-  unfold Plt, Ple in *; zify; omega.
 Qed.
 
 End INITMEM_INJ.
@@ -1450,14 +1378,12 @@ End INITMEM_INJ.
 Theorem initmem_inject:
   forall p m,
   init_mem p = Some m ->
-  Mem.inject (Mem.flat_inj (Mem.nextblock m)) m m.
+  Mem.inject (Mem.flat_inj Block.init) m m.
 Proof.
   unfold init_mem; intros.
   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.
 
 (** ** Sufficient and necessary conditions for the initial memory to exist. *)
@@ -1545,7 +1471,8 @@ Proof.
   destruct H0.
 + subst idg1; simpl in A.
   set (il := gvar_init v) in *. set (sz := init_data_list_size il) in *.
-  destruct (Mem.alloc m 0 sz) as [m1 b].
+  set (b := Block.glob id) in *.
+  set (m1 := Mem.alloc_at m b 0 sz) in *.
   destruct (store_zeros m1 b 0 sz) as [m2|]; try discriminate.
   destruct (store_init_data_list ge m2 b 0 il) as [m3|] eqn:B; try discriminate.
   split. eapply store_init_data_list_aligned; eauto. intros; eapply store_init_data_list_free_idents; eauto.
@@ -1582,8 +1509,9 @@ Proof.
           init_data_size i = size_chunk chunk ->
           init_data_alignment i = align_chunk chunk ->
           exists m', Mem.store chunk m b p v = Some m').
-  { intros. destruct (Mem.valid_access_store m chunk b p v) as (m' & STORE).
-    split. rewrite <- H2; auto. rewrite <- H3; auto.
+  { intros chunk v SZ ALI.
+    destruct (Mem.valid_access_store m chunk b p v) as (m' & STORE).
+    split. rewrite <- SZ; auto. rewrite <- ALI; auto.
     exists m'; auto. }
   destruct i; eauto.
   simpl. exists m; auto.
@@ -1620,14 +1548,19 @@ Lemma alloc_global_exists:
   exists m', alloc_global ge m idg = Some m'.
 Proof.
   intros m [id [f|v]]; intros; simpl.
-- destruct (Mem.alloc m 0 1) as [m1 b] eqn:ALLOC.
+- set (b := Block.glob id) in *.
+  set (m1 := Mem.alloc_at m b 0 1) in *.
   destruct (Mem.range_perm_drop_2 m1 b 0 1 Nonempty) as [m2 DROP].
-  red; intros; eapply Mem.perm_alloc_2; eauto.
+  red; intros; eapply Mem.perm_alloc_at_2; eauto. reflexivity.
+  red. eapply Block.lt_le_trans. apply Block.lt_glob_init. apply Mem.init_nextblock.
   exists m2; auto.
 - destruct H as [P Q].
   set (sz := init_data_list_size (gvar_init v)).
-  destruct (Mem.alloc m 0 sz) as [m1 b] eqn:ALLOC.
-  assert (P1: Mem.range_perm m1 b 0 sz Cur Freeable) by (red; intros; eapply Mem.perm_alloc_2; eauto).
+  set (b := Block.glob id) in *.
+  set (m1 := Mem.alloc_at m b 0 sz) in *.
+  assert (P1: Mem.range_perm m1 b 0 sz Cur Freeable).
+  red; intros; eapply Mem.perm_alloc_at_2; eauto. reflexivity.
+  red. eapply Block.lt_le_trans. apply Block.lt_glob_init. apply Mem.init_nextblock.
   destruct (@store_zeros_exists m1 b 0 sz) as [m2 ZEROS].
   red; intros. apply Mem.perm_implies with Freeable; auto with mem.
   rewrite ZEROS.
@@ -1669,10 +1602,6 @@ Section MATCH_GENVS.
 Context {A B V W: Type} (R: globdef A V -> globdef B W -> Prop).
 
 Record match_genvs (ge1: t A V) (ge2: t B W): Prop := {
-  mge_next:
-    genv_next ge2 = genv_next ge1;
-  mge_symb:
-    forall id, PTree.get id (genv_symb ge2) = PTree.get id (genv_symb ge1);
   mge_defs:
     forall b, option_rel R (PTree.get b (genv_defs ge1)) (PTree.get b (genv_defs ge2))
 }.
@@ -1684,11 +1613,9 @@ Lemma add_global_match:
   match_genvs (add_global ge1 (id, g1)) (add_global ge2 (id, g2)).
 Proof.
   intros. destruct H. constructor; simpl; intros.
-- congruence.
-- rewrite mge_next0, ! PTree.gsspec. destruct (peq id0 id); auto.
-- rewrite mge_next0, ! PTree.gsspec. destruct (peq b (genv_next ge1)).
+  rewrite ! PTree.gsspec.
+  destruct (peq b id); auto.
   constructor; auto.
-  auto.
 Qed.
 
 Lemma add_globals_match:
@@ -1725,7 +1652,12 @@ Qed.
 Theorem find_def_match_2:
   forall b, option_rel (match_globdef match_fundef match_varinfo ctx)
                        (find_def (globalenv p) b) (find_def (globalenv tp) b).
-Proof (mge_defs globalenvs_match).
+Proof.
+  intros b.
+  unfold find_def.
+  destruct (Block.ident_of b) eqn:Hb; try constructor.
+  apply (mge_defs globalenvs_match).
+Qed.
 
 Theorem find_def_match:
   forall b g,
@@ -1775,7 +1707,8 @@ Theorem find_symbol_match:
   forall (s : ident),
   find_symbol (globalenv tp) s = find_symbol (globalenv p) s.
 Proof.
-  intros. destruct globalenvs_match. apply mge_symb0.
+  unfold find_symbol.
+  intros. destruct globalenvs_match. destruct (mge_defs0 s); reflexivity.
 Qed.
 
 Theorem senv_match:
@@ -1787,9 +1720,11 @@ Proof.
   rewrite ! globalenv_public.
   destruct progmatch as (P & Q & R). rewrite R. auto.
 - intros. unfold block_is_volatile.
-  destruct globalenvs_match as [P Q R]. specialize (R b).
+  destruct globalenvs_match as [P].
   unfold find_var_info, find_def.
-  inv R; auto.
+  destruct (Block.ident_of b) eqn:Hb; auto.
+  specialize (P i).
+  inv P; auto.
   inv H1; auto.
   inv H2; auto.
 Qed.
@@ -1822,7 +1757,8 @@ Proof.
   - auto.
   - inv H; simpl in *.
     set (sz := init_data_list_size init) in *.
-    destruct (Mem.alloc m 0 sz) as [m2 b] eqn:?.
+    set (b := Block.glob id1) in *.
+    set (m2 := Mem.alloc_at m b 0 sz) in *.
     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.
diff --git a/common/Memory.v b/common/Memory.v
index 2cf1c3ab3b..48495f5a50 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -43,7 +43,7 @@ Require Export Memtype.
 Local Unset Elimination Schemes.
 Local Unset Case Analysis Schemes.
 
-Local Notation "a # b" := (PMap.get b a) (at level 1).
+Local Notation "a # b" := (BMap.get b a) (at level 1).
 
 Module Mem <: MEM.
 
@@ -61,24 +61,28 @@ Definition perm_order'' (po1 po2: option permission) :=
  end.
 
 Record mem' : Type := mkmem {
-  mem_contents: PMap.t (ZMap.t memval);  (**r [block -> offset -> memval] *)
-  mem_access: PMap.t (Z -> perm_kind -> option permission);
+  mem_contents: BMap.t (ZMap.t memval);  (**r [block -> offset -> memval] *)
+  mem_access: BMap.t (Z -> perm_kind -> option permission);
                                          (**r [block -> offset -> kind -> option permission] *)
   nextblock: block;
   access_max:
     forall b ofs, perm_order'' (mem_access#b ofs Max) (mem_access#b ofs Cur);
+  init_nextblock:
+    Block.le Block.init nextblock;
   nextblock_noaccess:
-    forall b ofs k, ~(Plt b nextblock) -> mem_access#b ofs k = None;
+    forall b ofs k, ~(Block.lt b nextblock) -> mem_access#b ofs k = None;
   contents_default:
     forall b, fst mem_contents#b = Undef
 }.
 
+Local Hint Resolve init_nextblock.
+
 Definition mem := mem'.
 
 Lemma mkmem_ext:
- forall cont1 cont2 acc1 acc2 next1 next2 a1 a2 b1 b2 c1 c2,
+ forall cont1 cont2 acc1 acc2 next1 next2 a1 a2 b1 b2 c1 c2 d1 d2,
   cont1=cont2 -> acc1=acc2 -> next1=next2 ->
-  mkmem cont1 acc1 next1 a1 b1 c1 = mkmem cont2 acc2 next2 a2 b2 c2.
+  mkmem cont1 acc1 next1 a1 b1 c1 d1 = mkmem cont2 acc2 next2 a2 b2 c2 d2.
 Proof.
   intros. subst. f_equal; apply proof_irr.
 Qed.
@@ -88,7 +92,7 @@ Qed.
 (** A block address is valid if it was previously allocated. It remains valid
   even after being freed. *)
 
-Definition valid_block (m: mem) (b: block) := Plt b (nextblock m).
+Definition valid_block (m: mem) (b: block) := Block.lt b (nextblock m).
 
 Theorem valid_not_valid_diff:
   forall m b b', valid_block m b -> ~(valid_block m b') -> b <> b'.
@@ -144,7 +148,7 @@ Theorem perm_valid_block:
   forall m b ofs k p, perm m b ofs k p -> valid_block m b.
 Proof.
   unfold perm; intros.
-  destruct (plt b m.(nextblock)).
+  destruct (Block.lt_dec b m.(nextblock)).
   auto.
   assert (m.(mem_access)#b ofs k = None).
   eapply nextblock_noaccess; eauto.
@@ -342,17 +346,45 @@ Qed.
 (** The initial store *)
 
 Program Definition empty: mem :=
-  mkmem (PMap.init (ZMap.init Undef))
-        (PMap.init (fun ofs k => None))
-        1%positive _ _ _.
+  mkmem (BMap.init (ZMap.init Undef))
+        (BMap.init (fun ofs k => None))
+        Block.init _ _ _ _.
+Next Obligation.
+  repeat rewrite BMap.gi. red; auto.
+Qed.
 Next Obligation.
-  repeat rewrite PMap.gi. red; auto.
+  blomega.
 Qed.
 Next Obligation.
-  rewrite PMap.gi. auto.
+  rewrite BMap.gi. auto.
 Qed.
 Next Obligation.
-  rewrite PMap.gi. auto.
+  rewrite BMap.gi. auto.
+Qed.
+
+Program Definition alloc_at (m: mem) (b: block) (lo hi: Z): mem :=
+  if Block.lt_dec b m.(nextblock)
+  then mkmem (BMap.set b
+                       (ZMap.init Undef)
+                       m.(mem_contents))
+             (BMap.set b
+                       (fun ofs k => if zle lo ofs && zlt ofs hi then Some Freeable else None)
+                       m.(mem_access))
+             m.(nextblock)
+                 _ _ _ _
+  else m.
+Next Obligation.
+  repeat rewrite BMap.gsspec. destruct (BMap.elt_eq b0 b).
+  subst b. destruct (zle lo ofs && zlt ofs hi); red; auto with mem.
+  apply access_max.
+Qed.
+Next Obligation.
+  rewrite BMap.gsspec. destruct (BMap.elt_eq b0 b).
+  subst b. contradiction.
+  apply nextblock_noaccess. assumption.
+Qed.
+Next Obligation.
+  rewrite BMap.gsspec. destruct (BMap.elt_eq b0 b). auto. apply contents_default.
 Qed.
 
 (** Allocation of a fresh block with the given bounds.  Return an updated
@@ -361,28 +393,32 @@ Qed.
   infinite memory. *)
 
 Program Definition alloc (m: mem) (lo hi: Z) :=
-  (mkmem (PMap.set m.(nextblock)
+  (mkmem (BMap.set m.(nextblock)
                    (ZMap.init Undef)
                    m.(mem_contents))
-         (PMap.set m.(nextblock)
+         (BMap.set m.(nextblock)
                    (fun ofs k => if zle lo ofs && zlt ofs hi then Some Freeable else None)
                    m.(mem_access))
-         (Pos.succ m.(nextblock))
-         _ _ _,
+         (Block.succ m.(nextblock))
+         _ _ _ _,
    m.(nextblock)).
 Next Obligation.
-  repeat rewrite PMap.gsspec. destruct (peq b (nextblock m)).
+  repeat rewrite BMap.gsspec. destruct (BMap.elt_eq b (nextblock m)).
   subst b. destruct (zle lo ofs && zlt ofs hi); red; auto with mem.
   apply access_max.
 Qed.
 Next Obligation.
-  rewrite PMap.gsspec. destruct (peq b (nextblock m)).
-  subst b. elim H. apply Plt_succ.
+  eapply Block.le_trans. apply init_nextblock.
+  apply Block.lt_le, Block.lt_succ.
+Qed.
+Next Obligation.
+  rewrite BMap.gsspec. destruct (BMap.elt_eq b (nextblock m)).
+  subst b. elim H. apply Block.lt_succ.
   apply nextblock_noaccess. red; intros; elim H.
-  apply Plt_trans_succ; auto.
+  apply Blt_trans_succ; auto.
 Qed.
 Next Obligation.
-  rewrite PMap.gsspec. destruct (peq b (nextblock m)). auto. apply contents_default.
+  rewrite BMap.gsspec. destruct (BMap.elt_eq b (nextblock m)). auto. apply contents_default.
 Qed.
 
 (** Freeing a block between the given bounds.
@@ -392,17 +428,17 @@ Qed.
 
 Program Definition unchecked_free (m: mem) (b: block) (lo hi: Z): mem :=
   mkmem m.(mem_contents)
-        (PMap.set b
+        (BMap.set b
                 (fun ofs k => if zle lo ofs && zlt ofs hi then None else m.(mem_access)#b ofs k)
                 m.(mem_access))
-        m.(nextblock) _ _ _.
+        m.(nextblock) _ _ _ _.
 Next Obligation.
-  repeat rewrite PMap.gsspec. destruct (peq b0 b).
+  repeat rewrite BMap.gsspec. destruct (BMap.elt_eq b0 b).
   destruct (zle lo ofs && zlt ofs hi). red; auto. apply access_max.
   apply access_max.
 Qed.
 Next Obligation.
-  repeat rewrite PMap.gsspec. destruct (peq b0 b). subst.
+  repeat rewrite BMap.gsspec. destruct (BMap.elt_eq b0 b). subst.
   destruct (zle lo ofs && zlt ofs hi). auto. apply nextblock_noaccess; auto.
   apply nextblock_noaccess; auto.
 Qed.
@@ -532,6 +568,14 @@ Proof.
   intros. apply getN_setN_disjoint. apply Intv.disjoint_range. auto.
 Qed.
 
+Lemma getN_undef:
+  forall n o,
+    getN n o (ZMap.init Undef) = list_repeat n Undef.
+Proof.
+  induction n; simpl; intros; eauto.
+  rewrite IHn, ZMap.gi; reflexivity.
+Qed.
+
 Remark setN_default:
   forall vl q c, fst (setN vl q c) = fst c.
 Proof.
@@ -545,18 +589,18 @@ Qed.
 
 Program Definition store (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z) (v: val): option mem :=
   if valid_access_dec m chunk b ofs Writable then
-    Some (mkmem (PMap.set b
+    Some (mkmem (BMap.set b
                           (setN (encode_val chunk v) ofs (m.(mem_contents)#b))
                           m.(mem_contents))
                 m.(mem_access)
                 m.(nextblock)
-                _ _ _)
+                _ _ _ _)
   else
     None.
 Next Obligation. apply access_max. Qed.
 Next Obligation. apply nextblock_noaccess; auto. Qed.
 Next Obligation.
-  rewrite PMap.gsspec. destruct (peq b0 b).
+  rewrite BMap.gsspec. destruct (BMap.elt_eq b0 b).
   rewrite setN_default. apply contents_default.
   apply contents_default.
 Qed.
@@ -577,16 +621,16 @@ Definition storev (chunk: memory_chunk) (m: mem) (addr v: val) : option mem :=
 Program Definition storebytes (m: mem) (b: block) (ofs: Z) (bytes: list memval) : option mem :=
   if range_perm_dec m b ofs (ofs + Z.of_nat (length bytes)) Cur Writable then
     Some (mkmem
-             (PMap.set b (setN bytes ofs (m.(mem_contents)#b)) m.(mem_contents))
+             (BMap.set b (setN bytes ofs (m.(mem_contents)#b)) m.(mem_contents))
              m.(mem_access)
              m.(nextblock)
-             _ _ _)
+             _ _ _ _)
   else
     None.
 Next Obligation. apply access_max. Qed.
 Next Obligation. apply nextblock_noaccess; auto. Qed.
 Next Obligation.
-  rewrite PMap.gsspec. destruct (peq b0 b).
+  rewrite BMap.gsspec. destruct (BMap.elt_eq b0 b).
   rewrite setN_default. apply contents_default.
   apply contents_default.
 Qed.
@@ -599,19 +643,19 @@ Qed.
 Program Definition drop_perm (m: mem) (b: block) (lo hi: Z) (p: permission): option mem :=
   if range_perm_dec m b lo hi Cur Freeable then
     Some (mkmem m.(mem_contents)
-                (PMap.set b
+                (BMap.set b
                         (fun ofs k => if zle lo ofs && zlt ofs hi then Some p else m.(mem_access)#b ofs k)
                         m.(mem_access))
-                m.(nextblock) _ _ _)
+                m.(nextblock) _ _ _ _)
   else None.
 Next Obligation.
-  repeat rewrite PMap.gsspec. destruct (peq b0 b). subst b0.
+  repeat rewrite BMap.gsspec. destruct (BMap.elt_eq b0 b). subst b0.
   destruct (zle lo ofs && zlt ofs hi). red; auto with mem. apply access_max.
   apply access_max.
 Qed.
 Next Obligation.
   specialize (nextblock_noaccess m b0 ofs k H0). intros.
-  rewrite PMap.gsspec. destruct (peq b0 b). subst b0.
+  rewrite BMap.gsspec. destruct (BMap.elt_eq b0 b). subst b0.
   destruct (zle lo ofs). destruct (zlt ofs hi).
   assert (perm m b ofs k Freeable). apply perm_cur. apply H; auto.
   unfold perm in H2. rewrite H1 in H2. contradiction.
@@ -625,12 +669,12 @@ Qed.
 
 (** Properties of the empty store. *)
 
-Theorem nextblock_empty: nextblock empty = 1%positive.
+Theorem nextblock_empty: nextblock empty = Block.init.
 Proof. reflexivity. Qed.
 
 Theorem perm_empty: forall b ofs k p, ~perm empty b ofs k p.
 Proof.
-  intros. unfold perm, empty; simpl. rewrite PMap.gi. simpl. tauto.
+  intros. unfold perm, empty; simpl. rewrite BMap.gi. simpl. tauto.
 Qed.
 
 Theorem valid_access_empty: forall chunk b ofs p, ~valid_access empty chunk b ofs p.
@@ -975,7 +1019,7 @@ Proof.
 Qed.
 
 Lemma store_mem_contents:
-  mem_contents m2 = PMap.set b (setN (encode_val chunk v) ofs m1.(mem_contents)#b) m1.(mem_contents).
+  mem_contents m2 = BMap.set b (setN (encode_val chunk v) ofs m1.(mem_contents)#b) m1.(mem_contents).
 Proof.
   unfold store in STORE. destruct (valid_access_dec m1 chunk b ofs Writable); inv STORE.
   auto.
@@ -1055,7 +1099,7 @@ Proof.
   exists v'; split; auto.
   exploit load_result; eauto. intros B.
   rewrite B. rewrite store_mem_contents; simpl.
-  rewrite PMap.gss.
+  rewrite BMap.gss.
   replace (size_chunk_nat chunk') with (length (encode_val chunk v)).
   rewrite getN_setN_same. apply decode_encode_val_general.
   rewrite encode_val_length. repeat rewrite size_chunk_conv in H.
@@ -1090,7 +1134,7 @@ Proof.
   destruct (valid_access_dec m1 chunk' b' ofs' Readable).
   rewrite pred_dec_true.
   decEq. decEq. rewrite store_mem_contents; simpl.
-  rewrite PMap.gsspec. destruct (peq b' b). subst b'.
+  rewrite BMap.gsspec. destruct (BMap.elt_eq b' b). subst b'.
   apply getN_setN_outside. rewrite encode_val_length. repeat rewrite <- size_chunk_conv.
   intuition.
   auto.
@@ -1105,7 +1149,7 @@ Proof.
   intros.
   assert (valid_access m2 chunk b ofs Readable) by eauto with mem.
   unfold loadbytes. rewrite pred_dec_true. rewrite store_mem_contents; simpl.
-  rewrite PMap.gss.
+  rewrite BMap.gss.
   replace (nat_of_Z (size_chunk chunk)) with (length (encode_val chunk v)).
   rewrite getN_setN_same. auto.
   rewrite encode_val_length. auto.
@@ -1124,7 +1168,7 @@ Proof.
   destruct (range_perm_dec m1 b' ofs' (ofs' + n) Cur Readable).
   rewrite pred_dec_true.
   decEq. rewrite store_mem_contents; simpl.
-  rewrite PMap.gsspec. destruct (peq b' b). subst b'.
+  rewrite BMap.gsspec. destruct (BMap.elt_eq b' b). subst b'.
   destruct H. congruence.
   destruct (zle n 0) as [z | n0].
   rewrite (nat_of_Z_neg _ z). auto.
@@ -1184,7 +1228,7 @@ Lemma load_store_overlap:
 Proof.
   intros.
   exploit load_result; eauto. erewrite store_mem_contents by eauto; simpl.
-  rewrite PMap.gss.
+  rewrite BMap.gss.
   set (c := (mem_contents m1)#b). intros V'.
   destruct (size_chunk_nat_pos chunk) as [sz SIZE].
   destruct (size_chunk_nat_pos chunk') as [sz' SIZE'].
@@ -1246,7 +1290,7 @@ Theorem load_pointer_store:
   \/ (b' <> b \/ ofs' + size_chunk chunk' <= ofs \/ ofs + size_chunk chunk <= ofs').
 Proof.
   intros.
-  destruct (peq b' b); auto. subst b'.
+  destruct (BMap.elt_eq b' b); auto. subst b'.
   destruct (zle (ofs' + size_chunk chunk') ofs); auto.
   destruct (zle (ofs + size_chunk chunk) ofs'); auto.
   exploit load_store_overlap; eauto.
@@ -1444,7 +1488,7 @@ Proof.
 Qed.
 
 Lemma storebytes_mem_contents:
-   mem_contents m2 = PMap.set b (setN bytes ofs m1.(mem_contents)#b) m1.(mem_contents).
+   mem_contents m2 = BMap.set b (setN bytes ofs m1.(mem_contents)#b) m1.(mem_contents).
 Proof.
   unfold storebytes in STORE.
   destruct (range_perm_dec m1 b ofs (ofs + Z.of_nat (length bytes)) Cur Writable);
@@ -1523,7 +1567,7 @@ Proof.
   destruct (range_perm_dec m1 b ofs (ofs + Z.of_nat (length bytes)) Cur Writable);
   try discriminate.
   rewrite pred_dec_true.
-  decEq. inv STORE2; simpl. rewrite PMap.gss. rewrite nat_of_Z_of_nat.
+  decEq. inv STORE2; simpl. rewrite BMap.gss. rewrite nat_of_Z_of_nat.
   apply getN_setN_same.
   red; eauto with mem.
 Qed.
@@ -1538,7 +1582,7 @@ Proof.
   destruct (range_perm_dec m1 b' ofs' (ofs' + len) Cur Readable).
   rewrite pred_dec_true.
   rewrite storebytes_mem_contents. decEq.
-  rewrite PMap.gsspec. destruct (peq b' b). subst b'.
+  rewrite BMap.gsspec. destruct (BMap.elt_eq b' b). subst b'.
   apply getN_setN_disjoint. rewrite nat_of_Z_eq; auto. intuition congruence.
   auto.
   red; auto with mem.
@@ -1569,7 +1613,7 @@ Proof.
   destruct (valid_access_dec m1 chunk b' ofs' Readable).
   rewrite pred_dec_true.
   rewrite storebytes_mem_contents. decEq.
-  rewrite PMap.gsspec. destruct (peq b' b). subst b'.
+  rewrite BMap.gsspec. destruct (BMap.elt_eq b' b). subst b'.
   rewrite getN_setN_outside. auto. rewrite <- size_chunk_conv. intuition congruence.
   auto.
   destruct v; split; auto. red; auto with mem.
@@ -1600,7 +1644,7 @@ Proof.
   destruct (range_perm_dec m1 b (ofs + Z.of_nat(length bytes1)) (ofs + Z.of_nat(length bytes1) + Z.of_nat(length bytes2)) Cur Writable); try congruence.
   destruct (range_perm_dec m b ofs (ofs + Z.of_nat (length (bytes1 ++ bytes2))) Cur Writable).
   inv ST1; inv ST2; simpl. decEq. apply mkmem_ext; auto.
-  rewrite PMap.gss.  rewrite setN_concat. symmetry. apply PMap.set2.
+  rewrite BMap.gss.  rewrite setN_concat. symmetry. apply BMap.set2.
   elim n.
   rewrite app_length. rewrite Nat2Z.inj_add. red; intros.
   destruct (zlt ofs0 (ofs + Z.of_nat(length bytes1))).
@@ -1665,6 +1709,106 @@ Proof.
   exploit store_valid_access_3. eexact H2. intros [P Q]. exact Q.
 Qed.
 
+(** ** Properties related to [alloc_at]. *)
+
+Section ALLOCAT.
+
+Variable m1: mem.
+Variable b: block.
+Variables lo hi: Z.
+Variable m2: mem.
+
+Hypothesis ALLOCAT: alloc_at m1 b lo hi = m2.
+
+Theorem nextblock_alloc_at:
+  nextblock m2 = nextblock m1.
+Proof.
+  subst. unfold alloc_at.
+  destruct (Block.lt_dec _ _); reflexivity.
+Qed.
+
+Theorem perm_alloc_at_1:
+  forall b' ofs k p, b' <> b -> perm m1 b' ofs k p -> perm m2 b' ofs k p.
+Proof.
+  unfold perm; intros b' ofs k p Hdiff PERM.
+  unfold alloc_at in ALLOCAT; destruct Block.lt_dec; subst; auto.
+  simpl.
+  rewrite BMap.gso; auto.
+Qed.
+
+Theorem perm_alloc_at_2:
+  valid_block m1 b ->
+  forall ofs k, lo <= ofs < hi -> perm m2 b ofs k Freeable.
+Proof.
+  unfold perm; intros VB ofs k.
+  unfold alloc_at in ALLOCAT.
+  destruct (Block.lt_dec _ _); try contradiction. subst. cbn.
+  intro RNG.
+  rewrite BMap.gss. unfold proj_sumbool. rewrite zle_true.
+  rewrite zlt_true. simpl. auto with mem. omega. omega.
+Qed.
+
+Theorem perm_alloc_at_inv:
+  forall b' ofs k p,
+  perm m2 b' ofs k p ->
+  if eq_block b' b then lo <= ofs < hi else perm m1 b' ofs k p.
+Proof.
+  intros until p; unfold perm. unfold alloc_at in ALLOCAT.
+  destruct (Block.lt_dec _ _).
+  - subst. simpl.
+    rewrite BMap.gsspec. change eq_block with BMap.elt_eq.
+    destruct (BMap.elt_eq b' b); intros.
+    destruct (zle lo ofs); try contradiction. destruct (zlt ofs hi); try contradiction.
+    split; auto.
+    auto.
+  - intro PERM.
+    destruct (eq_block _ _).
+    + subst.
+      apply perm_valid_block in PERM; contradiction.
+    + congruence.
+Qed.
+
+Theorem perm_alloc_at_3:
+  forall ofs k p, perm m2 b ofs k p -> lo <= ofs < hi.
+Proof.
+  intros. exploit perm_alloc_at_inv; eauto. rewrite dec_eq_true; auto.
+Qed.
+
+Lemma load_alloc_at_same:
+  Block.lt b Block.init ->
+  forall chunk ofs v,
+    load chunk m2 b ofs = Some v ->
+    v = Vundef.
+Proof.
+  unfold alloc_at in ALLOCAT.
+  intros VALID chunk ofs v LOAD.
+  destruct Block.lt_dec; subst.
+  - apply load_result in LOAD. simpl in LOAD. subst.
+    rewrite BMap.gss, getN_undef.
+    generalize (size_chunk_nat_pos chunk). intros (n & EQ); rewrite EQ. simpl.
+    apply decode_val_undef.
+  - elim n. eapply Block.lt_le_trans; eauto.
+Qed.
+
+Lemma loadbytes_alloc_at_same:
+  Block.lt b Block.init ->
+  forall n ofs bytes byte,
+    loadbytes m2 b ofs n = Some bytes ->
+    In byte bytes ->
+    byte = Undef.
+Proof.
+  unfold alloc_at in ALLOCAT.
+  intros VALID n ofs bytes byte LOADBYTES.
+  destruct Block.lt_dec; subst.
+  - unfold loadbytes in LOADBYTES. simpl in LOADBYTES.
+    destruct (range_perm_dec) in LOADBYTES; try discriminate. inv LOADBYTES.
+    rewrite BMap.gss. rewrite getN_undef.
+    apply in_list_repeat.
+  - elim n0. eapply Block.lt_le_trans; eauto.
+Qed.
+
+End ALLOCAT.
+
 (** ** Properties related to [alloc]. *)
 
 Section ALLOC.
@@ -1676,7 +1820,7 @@ Variable b: block.
 Hypothesis ALLOC: alloc m1 lo hi = (m2, b).
 
 Theorem nextblock_alloc:
-  nextblock m2 = Pos.succ (nextblock m1).
+  nextblock m2 = Block.succ (nextblock m1).
 Proof.
   injection ALLOC; intros. rewrite <- H0; auto.
 Qed.
@@ -1691,19 +1835,19 @@ Theorem valid_block_alloc:
   forall b', valid_block m1 b' -> valid_block m2 b'.
 Proof.
   unfold valid_block; intros. rewrite nextblock_alloc.
-  apply Plt_trans_succ; auto.
+  apply Blt_trans_succ; auto.
 Qed.
 
 Theorem fresh_block_alloc:
   ~(valid_block m1 b).
 Proof.
-  unfold valid_block. rewrite alloc_result. apply Plt_strict.
+  unfold valid_block. rewrite alloc_result. apply Block.lt_strict.
 Qed.
 
 Theorem valid_new_block:
   valid_block m2 b.
 Proof.
-  unfold valid_block. rewrite alloc_result. rewrite nextblock_alloc. apply Plt_succ.
+  unfold valid_block. rewrite alloc_result. rewrite nextblock_alloc. apply Block.lt_succ.
 Qed.
 
 Local Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem.
@@ -1713,22 +1857,22 @@ Theorem valid_block_alloc_inv:
 Proof.
   unfold valid_block; intros.
   rewrite nextblock_alloc in H. rewrite alloc_result.
-  exploit Plt_succ_inv; eauto. tauto.
+  exploit Block.lt_succ_inv; eauto. tauto.
 Qed.
 
 Theorem perm_alloc_1:
   forall b' ofs k p, perm m1 b' ofs k p -> perm m2 b' ofs k p.
 Proof.
   unfold perm; intros. injection ALLOC; intros. rewrite <- H1; simpl.
-  subst b. rewrite PMap.gsspec. destruct (peq b' (nextblock m1)); auto.
-  rewrite nextblock_noaccess in H. contradiction. subst b'. apply Plt_strict.
+  subst b. rewrite BMap.gsspec. destruct (BMap.elt_eq b' (nextblock m1)); auto.
+  rewrite nextblock_noaccess in H. contradiction. subst b'. apply Block.lt_strict.
 Qed.
 
 Theorem perm_alloc_2:
   forall ofs k, lo <= ofs < hi -> perm m2 b ofs k Freeable.
 Proof.
   unfold perm; intros. injection ALLOC; intros. rewrite <- H1; simpl.
-  subst b. rewrite PMap.gss. unfold proj_sumbool. rewrite zle_true.
+  subst b. rewrite BMap.gss. unfold proj_sumbool. rewrite zle_true.
   rewrite zlt_true. simpl. auto with mem. omega. omega.
 Qed.
 
@@ -1738,7 +1882,7 @@ Theorem perm_alloc_inv:
   if eq_block b' b then lo <= ofs < hi else perm m1 b' ofs k p.
 Proof.
   intros until p; unfold perm. inv ALLOC. simpl.
-  rewrite PMap.gsspec. unfold eq_block. destruct (peq b' (nextblock m1)); intros.
+  rewrite BMap.gsspec. change eq_block with BMap.elt_eq. destruct (BMap.elt_eq b' (nextblock m1)); intros.
   destruct (zle lo ofs); try contradiction. destruct (zlt ofs hi); try contradiction.
   split; auto.
   auto.
@@ -1808,7 +1952,7 @@ Proof.
   subst b'. elimtype False. eauto with mem.
   rewrite pred_dec_true; auto.
   injection ALLOC; intros. rewrite <- H2; simpl.
-  rewrite PMap.gso. auto. rewrite H1. apply not_eq_sym; eauto with mem.
+  rewrite BMap.gso. auto. rewrite H1. apply not_eq_sym; eauto with mem.
   rewrite pred_dec_false. auto.
   eauto with mem.
 Qed.
@@ -1828,7 +1972,7 @@ Theorem load_alloc_same:
 Proof.
   intros. exploit load_result; eauto. intro. rewrite H0.
   injection ALLOC; intros. rewrite <- H2; simpl. rewrite <- H1.
-  rewrite PMap.gss. destruct (size_chunk_nat_pos chunk) as [n E]. rewrite E. simpl.
+  rewrite BMap.gss. destruct (size_chunk_nat_pos chunk) as [n E]. rewrite E. simpl.
   rewrite ZMap.gi. apply decode_val_undef.
 Qed.
 
@@ -1853,7 +1997,7 @@ Proof.
   destruct (range_perm_dec m1 b' ofs (ofs + n) Cur Readable).
   rewrite pred_dec_true.
   injection ALLOC; intros A B. rewrite <- B; simpl.
-  rewrite PMap.gso. auto. rewrite A. eauto with mem.
+  rewrite BMap.gso. auto. rewrite A. eauto with mem.
   red; intros. eapply perm_alloc_1; eauto.
   rewrite pred_dec_false; auto.
   red; intros; elim n0. red; intros. eapply perm_alloc_4; eauto. eauto with mem.
@@ -1866,7 +2010,7 @@ Theorem loadbytes_alloc_same:
 Proof.
   unfold loadbytes; intros. destruct (range_perm_dec m2 b ofs (ofs + n) Cur Readable); inv H.
   revert H0.
-  injection ALLOC; intros A B. rewrite <- A; rewrite <- B; simpl. rewrite PMap.gss.
+  injection ALLOC; intros A B. rewrite <- A; rewrite <- B; simpl. rewrite BMap.gss.
   generalize (nat_of_Z n) ofs. induction n0; simpl; intros.
   contradiction.
   rewrite ZMap.gi in H0. destruct H0; eauto.
@@ -1936,7 +2080,7 @@ Theorem perm_free_1:
   perm m2 b ofs k p.
 Proof.
   intros. rewrite free_result. unfold perm, unchecked_free; simpl.
-  rewrite PMap.gsspec. destruct (peq b bf). subst b.
+  rewrite BMap.gsspec. destruct (BMap.elt_eq b bf). subst b.
   destruct (zle lo ofs); simpl.
   destruct (zlt ofs hi); simpl.
   elimtype False; intuition.
@@ -1948,7 +2092,7 @@ Theorem perm_free_2:
   forall ofs k p, lo <= ofs < hi -> ~ perm m2 bf ofs k p.
 Proof.
   intros. rewrite free_result. unfold perm, unchecked_free; simpl.
-  rewrite PMap.gss. unfold proj_sumbool. rewrite zle_true. rewrite zlt_true.
+  rewrite BMap.gss. unfold proj_sumbool. rewrite zle_true. rewrite zlt_true.
   simpl. tauto. omega. omega.
 Qed.
 
@@ -1957,7 +2101,7 @@ Theorem perm_free_3:
   perm m2 b ofs k p -> perm m1 b ofs k p.
 Proof.
   intros until p. rewrite free_result. unfold perm, unchecked_free; simpl.
-  rewrite PMap.gsspec. destruct (peq b bf). subst b.
+  rewrite BMap.gsspec. destruct (BMap.elt_eq b bf). subst b.
   destruct (zle lo ofs); simpl.
   destruct (zlt ofs hi); simpl. tauto.
   auto. auto. auto.
@@ -1969,7 +2113,7 @@ Theorem perm_free_inv:
   (b = bf /\ lo <= ofs < hi) \/ perm m2 b ofs k p.
 Proof.
   intros. rewrite free_result. unfold perm, unchecked_free; simpl.
-  rewrite PMap.gsspec. destruct (peq b bf); auto. subst b.
+  rewrite BMap.gsspec. destruct (BMap.elt_eq b bf); auto. subst b.
   destruct (zle lo ofs); simpl; auto.
   destruct (zlt ofs hi); simpl; auto.
 Qed.
@@ -2007,7 +2151,7 @@ Proof.
   intros. destruct H. split; auto.
   red; intros. generalize (H ofs0 H1).
   rewrite free_result. unfold perm, unchecked_free; simpl.
-  rewrite PMap.gsspec. destruct (peq b bf). subst b.
+  rewrite BMap.gsspec. destruct (BMap.elt_eq b bf). subst b.
   destruct (zle lo ofs0); simpl.
   destruct (zlt ofs0 hi); simpl.
   tauto. auto. auto. auto.
@@ -2128,7 +2272,7 @@ Theorem perm_drop_1:
 Proof.
   intros.
   unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP.
-  unfold perm. simpl. rewrite PMap.gss. unfold proj_sumbool.
+  unfold perm. simpl. rewrite BMap.gss. unfold proj_sumbool.
   rewrite zle_true. rewrite zlt_true. simpl. constructor.
   omega. omega.
 Qed.
@@ -2138,7 +2282,7 @@ Theorem perm_drop_2:
 Proof.
   intros.
   unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP.
-  revert H0. unfold perm; simpl. rewrite PMap.gss. unfold proj_sumbool.
+  revert H0. unfold perm; simpl. rewrite BMap.gss. unfold proj_sumbool.
   rewrite zle_true. rewrite zlt_true. simpl. auto.
   omega. omega.
 Qed.
@@ -2148,7 +2292,7 @@ Theorem perm_drop_3:
 Proof.
   intros.
   unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP.
-  unfold perm; simpl. rewrite PMap.gsspec. destruct (peq b' b). subst b'.
+  unfold perm; simpl. rewrite BMap.gsspec. destruct (BMap.elt_eq b' b). subst b'.
   unfold proj_sumbool. destruct (zle lo ofs). destruct (zlt ofs hi).
   byContradiction. intuition omega.
   auto. auto. auto.
@@ -2159,7 +2303,7 @@ Theorem perm_drop_4:
 Proof.
   intros.
   unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP.
-  revert H. unfold perm; simpl. rewrite PMap.gsspec. destruct (peq b' b).
+  revert H. unfold perm; simpl. rewrite BMap.gsspec. destruct (BMap.elt_eq b' b).
   subst b'. unfold proj_sumbool. destruct (zle lo ofs). destruct (zlt ofs hi).
   simpl. intros. apply perm_implies with p. apply perm_implies with Freeable. apply perm_cur.
   apply r. tauto. auto with mem. auto.
@@ -2407,15 +2551,15 @@ Proof.
   intros.
   rewrite (store_mem_contents _ _ _ _ _ _ H0).
   rewrite (store_mem_contents _ _ _ _ _ _ STORE).
-  rewrite ! PMap.gsspec.
-  destruct (peq b0 b1). subst b0.
+  rewrite ! BMap.gsspec.
+  destruct (BMap.elt_eq b0 b1). subst b0.
   (* block = b1, block = b2 *)
   assert (b3 = b2) by congruence. subst b3.
   assert (delta0 = delta) by congruence. subst delta0.
-  rewrite peq_true.
+  destruct (BMap.elt_eq _ _); try congruence.
   apply setN_inj with (access := fun ofs => perm m1 b1 ofs Cur Readable).
   apply encode_val_inject; auto. intros. eapply mi_memval; eauto. eauto with mem.
-  destruct (peq b3 b2). subst b3.
+  destruct (BMap.elt_eq b3 b2). subst b3.
   (* block <> b1, block = b2 *)
   rewrite setN_other. eapply mi_memval; eauto. eauto with mem.
   rewrite encode_val_length. rewrite <- size_chunk_conv. intros.
@@ -2444,7 +2588,7 @@ Proof.
 (* mem_contents *)
   intros.
   rewrite (store_mem_contents _ _ _ _ _ _ H0).
-  rewrite PMap.gso. eapply mi_memval; eauto with mem.
+  rewrite BMap.gso. eapply mi_memval; eauto with mem.
   congruence.
 Qed.
 
@@ -2466,7 +2610,7 @@ Proof.
 (* mem_contents *)
   intros.
   rewrite (store_mem_contents _ _ _ _ _ _ H1).
-  rewrite PMap.gsspec. destruct (peq b2 b). subst b2.
+  rewrite BMap.gsspec. destruct (BMap.elt_eq b2 b). subst b2.
   rewrite setN_outside. auto.
   rewrite encode_val_length. rewrite <- size_chunk_conv.
   destruct (zlt (ofs0 + delta) ofs); auto.
@@ -2509,13 +2653,13 @@ Proof.
   assert (perm m1 b0 ofs0 Cur Readable). eapply perm_storebytes_2; eauto.
   rewrite (storebytes_mem_contents _ _ _ _ _ H0).
   rewrite (storebytes_mem_contents _ _ _ _ _ STORE).
-  rewrite ! PMap.gsspec. destruct (peq b0 b1). subst b0.
+  rewrite ! BMap.gsspec. destruct (BMap.elt_eq b0 b1). subst b0.
   (* block = b1, block = b2 *)
   assert (b3 = b2) by congruence. subst b3.
   assert (delta0 = delta) by congruence. subst delta0.
-  rewrite peq_true.
+  destruct (BMap.elt_eq _ _); try congruence.
   apply setN_inj with (access := fun ofs => perm m1 b1 ofs Cur Readable); auto.
-  destruct (peq b3 b2). subst b3.
+  destruct (BMap.elt_eq b3 b2). subst b3.
   (* block <> b1, block = b2 *)
   rewrite setN_other. auto.
   intros.
@@ -2547,7 +2691,7 @@ Proof.
 (* mem_contents *)
   intros.
   rewrite (storebytes_mem_contents _ _ _ _ _ H0).
-  rewrite PMap.gso. eapply mi_memval0; eauto. eapply perm_storebytes_2; eauto.
+  rewrite BMap.gso. eapply mi_memval0; eauto. eapply perm_storebytes_2; eauto.
   congruence.
 Qed.
 
@@ -2569,7 +2713,7 @@ Proof.
 (* mem_contents *)
   intros.
   rewrite (storebytes_mem_contents _ _ _ _ _ H1).
-  rewrite PMap.gsspec. destruct (peq b2 b). subst b2.
+  rewrite BMap.gsspec. destruct (BMap.elt_eq b2 b). subst b2.
   rewrite setN_outside. auto.
   destruct (zlt (ofs0 + delta) ofs); auto.
   destruct (zle (ofs + Z.of_nat (length bytes2)) (ofs0 + delta)). omega.
@@ -2598,8 +2742,8 @@ Proof.
   assert (perm m1 b0 ofs Cur Readable). eapply perm_storebytes_2; eauto.
   rewrite (storebytes_mem_contents _ _ _ _ _ H0).
   rewrite (storebytes_mem_contents _ _ _ _ _ H1).
-  simpl. rewrite ! PMap.gsspec.
-  destruct (peq b0 b1); destruct (peq b3 b2); subst; eapply mi_memval0; eauto.
+  simpl. rewrite ! BMap.gsspec.
+  destruct (BMap.elt_eq b0 b1); destruct (BMap.elt_eq b3 b2); subst; eapply mi_memval0; eauto.
 Qed.
 
 (** Preservation of allocations *)
@@ -2621,7 +2765,7 @@ Proof.
   assert (perm m2 b0 (ofs + delta) Cur Readable).
     eapply mi_perm0; eauto.
   assert (valid_block m2 b0) by eauto with mem.
-  rewrite <- MEM; simpl. rewrite PMap.gso. eauto with mem.
+  rewrite <- MEM; simpl. rewrite BMap.gso. eauto with mem.
   rewrite NEXT. eauto with mem.
 Qed.
 
@@ -2644,7 +2788,7 @@ Proof.
   injection H0; intros NEXT MEM. intros.
   rewrite <- MEM; simpl. rewrite NEXT.
   exploit perm_alloc_inv; eauto. intros.
-  rewrite PMap.gsspec. unfold eq_block in H4. destruct (peq b0 b1).
+  rewrite BMap.gsspec. change eq_block with BMap.elt_eq in H4. destruct (BMap.elt_eq b0 b1).
   rewrite ZMap.gi. constructor. eauto.
 Qed.
 
@@ -2680,8 +2824,8 @@ Proof.
   injection H0; intros NEXT MEM.
   intros. rewrite <- MEM; simpl. rewrite NEXT.
   exploit perm_alloc_inv; eauto. intros.
-  rewrite PMap.gsspec. unfold eq_block in H7.
-  destruct (peq b0 b1). rewrite ZMap.gi. constructor. eauto.
+  rewrite BMap.gsspec. change eq_block with BMap.elt_eq in H7.
+  destruct (BMap.elt_eq b0 b1). rewrite ZMap.gi. constructor. eauto.
 Qed.
 
 Lemma free_left_inj:
@@ -3180,7 +3324,7 @@ Theorem valid_block_inject_1:
   inject f m1 m2 ->
   valid_block m1 b1.
 Proof.
-  intros. inv H. destruct (plt b1 (nextblock m1)). auto.
+  intros. inv H. destruct (Block.lt_dec b1 (nextblock m1)). auto.
   assert (f b1 = None). eapply mi_freeblocks; eauto. congruence.
 Qed.
 
@@ -4171,100 +4315,135 @@ Qed.
 (** Injecting a memory into itself. *)
 
 Definition flat_inj (thr: block) : meminj :=
-  fun (b: block) => if plt b thr then Some(b, 0) else None.
+  fun (b: block) => if Block.lt_dec b thr then Some(b, 0) else None.
 
-Definition inject_neutral (thr: block) (m: mem) :=
-  mem_inj (flat_inj thr) m m.
+Definition inject_neutral (m: mem) :=
+  mem_inj (flat_inj Block.init) m m.
 
 Remark flat_inj_no_overlap:
   forall thr m, meminj_no_overlap (flat_inj thr) m.
 Proof.
   unfold flat_inj; intros; red; intros.
-  destruct (plt b1 thr); inversion H0; subst.
-  destruct (plt b2 thr); inversion H1; subst.
+  destruct (Block.lt_dec b1 thr); inversion H0; subst.
+  destruct (Block.lt_dec b2 thr); inversion H1; subst.
   auto.
 Qed.
 
 Theorem neutral_inject:
-  forall m, inject_neutral (nextblock m) m -> inject (flat_inj (nextblock m)) m m.
+  forall m, inject_neutral m -> inject (flat_inj Block.init) m m.
 Proof.
   intros. constructor.
 (* meminj *)
   auto.
 (* freeblocks *)
   unfold flat_inj, valid_block; intros.
-  apply pred_dec_false. auto.
+  apply pred_dec_false.
+  intro LT; apply H0. eapply Block.lt_le_trans; eauto.
 (* mappedblocks *)
   unfold flat_inj, valid_block; intros.
-  destruct (plt b (nextblock m)); inversion H0; subst. auto.
+  destruct (Block.lt_dec b Block.init); inversion H0; subst.
+  eapply Block.lt_le_trans; eauto.
 (* no overlap *)
   apply flat_inj_no_overlap.
 (* range *)
   unfold flat_inj; intros.
-  destruct (plt b (nextblock m)); inv H0. generalize (Ptrofs.unsigned_range_2 ofs); omega.
+  destruct (Block.lt_dec b Block.init); inv H0. generalize (Ptrofs.unsigned_range_2 ofs); omega.
 (* perm inv *)
   unfold flat_inj; intros.
-  destruct (plt b1 (nextblock m)); inv H0.
+  destruct (Block.lt_dec b1 Block.init); inv H0.
   rewrite Z.add_0_r in H1; auto.
 Qed.
 
 Theorem empty_inject_neutral:
-  forall thr, inject_neutral thr empty.
+  inject_neutral empty.
 Proof.
-  intros; red; constructor.
+  apply neutral_inject.
+  constructor.
 (* perm *)
-  unfold flat_inj; intros. destruct (plt b1 thr); inv H.
+  unfold flat_inj; intros. destruct (Block.lt_dec b1 Block.init); inv H.
   replace (ofs + 0) with ofs by omega; auto.
 (* align *)
-  unfold flat_inj; intros. destruct (plt b1 thr); inv H. apply Z.divide_0_r.
+  unfold flat_inj; intros. destruct (Block.lt_dec b1 Block.init); inv H. apply Z.divide_0_r.
 (* mem_contents *)
-  intros; simpl. rewrite ! PMap.gi. rewrite ! ZMap.gi. constructor.
-Qed.
-
-Theorem alloc_inject_neutral:
-  forall thr m lo hi b m',
-  alloc m lo hi = (m', b) ->
-  inject_neutral thr m ->
-  Plt (nextblock m) thr ->
-  inject_neutral thr m'.
-Proof.
-  intros; red.
-  eapply alloc_left_mapped_inj with (m1 := m) (b2 := b) (delta := 0).
-  eapply alloc_right_inj; eauto. eauto. eauto with mem.
-  red. intros. apply Z.divide_0_r.
-  intros.
-  apply perm_implies with Freeable; auto with mem.
-  eapply perm_alloc_2; eauto. omega.
-  unfold flat_inj. apply pred_dec_true.
-  rewrite (alloc_result _ _ _ _ _ H). auto.
+  intros; simpl. rewrite ! BMap.gi. rewrite ! ZMap.gi. constructor.
+Qed.
+
+Lemma alloc_at_mem_inj:
+  forall b,
+    Block.lt b Block.init ->
+    forall m1 m2 lo hi,
+      inject (flat_inj Block.init) m1 m2 ->
+      mem_inj (flat_inj Block.init) (alloc_at m1 b lo hi) (alloc_at m2 b lo hi).
+Proof.
+  intros b BLT m1 m2 lo hi INJ.
+  unfold alloc_at.
+  destruct Block.lt_dec. destruct Block.lt_dec.
+  - constructor.
+    + intros b1 b2 delta0 ofs k p FI PERM.
+      unfold perm in *. simpl in *.
+      unfold flat_inj in FI.
+      destruct Block.lt_dec; try congruence. inv FI.
+      rewrite BMap.gsspec in PERM |- *.
+      destruct (BMap.elt_eq b2 b).
+      * rewrite Z.add_0_r; auto.
+      * destruct INJ. eapply mi_perm; eauto. unfold flat_inj; rewrite pred_dec_true; auto.
+    + intros b1 b2 delta chunk ofs p FI RP.
+      unfold flat_inj in FI.
+      destruct Block.lt_dec; try congruence. inv FI.
+      exists 0; omega.
+    + intros b1 ofs b2 delta FI PERM.
+      red in PERM; simpl in *.
+      unfold flat_inj in FI.
+      destruct Block.lt_dec; try congruence. inv FI.
+      rewrite BMap.gsspec in PERM.
+      rewrite ! BMap.gsspec.
+      destruct BMap.elt_eq.
+      * subst. rewrite ! ZMap.gi. constructor.
+      * eapply mi_memval; eauto. destruct INJ; eauto.
+        unfold flat_inj; rewrite pred_dec_true; auto.
+  - exfalso. apply n.
+    eapply Block.lt_le_trans. apply BLT. apply init_nextblock.
+  - exfalso. apply n.
+    eapply Block.lt_le_trans. apply BLT. apply init_nextblock.
+Qed.
+
+Theorem alloc_at_inject_neutral:
+  forall b m lo hi,
+  inject_neutral m ->
+  Block.lt b Block.init ->
+  inject_neutral (alloc_at m b lo hi).
+Proof.
+  intros; eapply alloc_at_mem_inj; auto.
+  apply neutral_inject; auto.
 Qed.
 
 Theorem store_inject_neutral:
-  forall chunk m b ofs v m' thr,
+  forall chunk m b ofs v m',
   store chunk m b ofs v = Some m' ->
-  inject_neutral thr m ->
-  Plt b thr ->
-  Val.inject (flat_inj thr) v v ->
-  inject_neutral thr m'.
+  inject_neutral m ->
+  Block.lt b Block.init ->
+  Val.inject (flat_inj Block.init) v v ->
+  inject_neutral m'.
 Proof.
-  intros; red.
-  exploit store_mapped_inj. eauto. eauto. apply flat_inj_no_overlap.
-  unfold flat_inj. apply pred_dec_true; auto. eauto.
-  replace (ofs + 0) with ofs by omega.
-  intros [m'' [A B]]. congruence.
+  intros.
+  edestruct store_mapped_inj as (m2' & STORE & INJ); eauto.
+  apply flat_inj_no_overlap.
+  unfold flat_inj. apply pred_dec_true; auto.
+  replace (ofs + 0) with ofs in * by omega.
+  red. congruence.
 Qed.
 
 Theorem drop_inject_neutral:
-  forall m b lo hi p m' thr,
+  forall m b lo hi p m',
   drop_perm m b lo hi p = Some m' ->
-  inject_neutral thr m ->
-  Plt b thr ->
-  inject_neutral thr m'.
+  inject_neutral m ->
+  Block.lt b Block.init ->
+  inject_neutral m'.
 Proof.
-  unfold inject_neutral; intros.
-  exploit drop_mapped_inj; eauto. apply flat_inj_no_overlap.
+  intros.
+  exploit drop_mapped_inj; eauto. inv H0; eauto. apply flat_inj_no_overlap.
   unfold flat_inj. apply pred_dec_true; eauto.
-  repeat rewrite Z.add_0_r. intros [m'' [A B]]. congruence.
+  repeat rewrite Z.add_0_r. intros [m'' [A B]]. red; congruence.
 Qed.
 
 (** * Invariance properties between two memory states *)
@@ -4275,7 +4454,7 @@ Variable P: block -> Z -> Prop.
 
 Record unchanged_on (m_before m_after: mem) : Prop := mk_unchanged_on {
   unchanged_on_nextblock:
-    Ple (nextblock m_before) (nextblock m_after);
+    Block.le (nextblock m_before) (nextblock m_after);
   unchanged_on_perm:
     forall b ofs k p,
     P b ofs -> valid_block m_before b ->
@@ -4283,21 +4462,22 @@ Record unchanged_on (m_before m_after: mem) : Prop := mk_unchanged_on {
   unchanged_on_contents:
     forall b ofs,
     P b ofs -> perm m_before b ofs Cur Readable ->
-    ZMap.get ofs (PMap.get b m_after.(mem_contents)) =
-    ZMap.get ofs (PMap.get b m_before.(mem_contents))
+    ZMap.get ofs (BMap.get b m_after.(mem_contents)) =
+    ZMap.get ofs (BMap.get b m_before.(mem_contents))
 }.
 
 Lemma unchanged_on_refl:
   forall m, unchanged_on m m.
 Proof.
-  intros; constructor. apply Ple_refl. tauto. tauto.
+  intros; constructor. apply Block.le_refl. tauto. tauto.
 Qed.
 
 Lemma valid_block_unchanged_on:
   forall m m' b,
   unchanged_on m m' -> valid_block m b -> valid_block m' b.
 Proof.
-  unfold valid_block; intros. apply unchanged_on_nextblock in H. xomega.
+  unfold valid_block; intros. apply unchanged_on_nextblock in H.
+  eapply Block.lt_le_trans; eauto.
 Qed.
 
 Lemma perm_unchanged_on:
@@ -4320,7 +4500,7 @@ Lemma unchanged_on_trans:
   forall m1 m2 m3, unchanged_on m1 m2 -> unchanged_on m2 m3 -> unchanged_on m1 m3.
 Proof.
   intros; constructor.
-- apply Ple_trans with (nextblock m2); apply unchanged_on_nextblock; auto.
+- apply Block.le_trans with (nextblock m2); apply unchanged_on_nextblock; auto.
 - intros. transitivity (perm m2 b ofs k p); apply unchanged_on_perm; auto.
   eapply valid_block_unchanged_on; eauto.
 - intros. transitivity (ZMap.get ofs (mem_contents m2)#b); apply unchanged_on_contents; auto.
@@ -4394,10 +4574,10 @@ Lemma store_unchanged_on:
   unchanged_on m m'.
 Proof.
   intros; constructor; intros.
-- rewrite (nextblock_store _ _ _ _ _ _ H). apply Ple_refl.
+- rewrite (nextblock_store _ _ _ _ _ _ H). apply Block.le_refl.
 - split; intros; eauto with mem.
-- erewrite store_mem_contents; eauto. rewrite PMap.gsspec.
-  destruct (peq b0 b); auto. subst b0. apply setN_outside.
+- erewrite store_mem_contents; eauto. rewrite BMap.gsspec.
+  destruct (BMap.elt_eq b0 b); auto. subst b0. apply setN_outside.
   rewrite encode_val_length. rewrite <- size_chunk_conv.
   destruct (zlt ofs0 ofs); auto.
   destruct (zlt ofs0 (ofs + size_chunk chunk)); auto.
@@ -4411,28 +4591,48 @@ Lemma storebytes_unchanged_on:
   unchanged_on m m'.
 Proof.
   intros; constructor; intros.
-- rewrite (nextblock_storebytes _ _ _ _ _ H). apply Ple_refl.
+- rewrite (nextblock_storebytes _ _ _ _ _ H). apply Block.le_refl.
 - split; intros. eapply perm_storebytes_1; eauto. eapply perm_storebytes_2; eauto.
-- erewrite storebytes_mem_contents; eauto. rewrite PMap.gsspec.
-  destruct (peq b0 b); auto. subst b0. apply setN_outside.
+- erewrite storebytes_mem_contents; eauto. rewrite BMap.gsspec.
+  destruct (BMap.elt_eq b0 b); auto. subst b0. apply setN_outside.
   destruct (zlt ofs0 ofs); auto.
   destruct (zlt ofs0 (ofs + Z.of_nat (length bytes))); auto.
   elim (H0 ofs0). omega. auto.
 Qed.
 
+Lemma alloc_at_unchanged_on:
+  forall m1 b lo hi m2,
+    alloc_at m1 b lo hi = m2 ->
+    (forall ofs, ~ P b ofs) ->
+    unchanged_on m1 m2.
+Proof.
+  unfold alloc_at; intros m1 b lo hi m2 ALLOCAT Pspec.
+  destruct Block.lt_dec; subst.
+  - constructor; simpl.
+    + apply Block.le_refl.
+    + unfold perm; simpl.
+      intros b0 ofs k p PP VB.
+      rewrite BMap.gso. tauto.
+      intro; subst; apply Pspec in PP; eauto.
+    + intros b0 ofs PP PERM.
+      rewrite BMap.gso; auto.
+      intro; subst; apply Pspec in PP; eauto.
+  - apply unchanged_on_refl.
+Qed.
+
 Lemma alloc_unchanged_on:
   forall m lo hi m' b,
   alloc m lo hi = (m', b) ->
   unchanged_on m m'.
 Proof.
   intros; constructor; intros.
-- rewrite (nextblock_alloc _ _ _ _ _ H). apply Ple_succ.
+- rewrite (nextblock_alloc _ _ _ _ _ H). apply Block.lt_le, Block.lt_succ.
 - split; intros.
   eapply perm_alloc_1; eauto.
   eapply perm_alloc_4; eauto.
   eapply valid_not_valid_diff; eauto with mem.
 - injection H; intros A B. rewrite <- B; simpl.
-  rewrite PMap.gso; auto. rewrite A.  eapply valid_not_valid_diff; eauto with mem.
+  rewrite BMap.gso; auto. rewrite A.  eapply valid_not_valid_diff; eauto with mem.
 Qed.
 
 Lemma free_unchanged_on:
@@ -4442,7 +4642,7 @@ Lemma free_unchanged_on:
   unchanged_on m m'.
 Proof.
   intros; constructor; intros.
-- rewrite (nextblock_free _ _ _ _ _ H). apply Ple_refl.
+- rewrite (nextblock_free _ _ _ _ _ H). apply Block.le_refl.
 - split; intros.
   eapply perm_free_1; eauto.
   destruct (eq_block b0 b); auto. destruct (zlt ofs lo); auto. destruct (zle hi ofs); auto.
@@ -4459,7 +4659,7 @@ Lemma drop_perm_unchanged_on:
   unchanged_on m m'.
 Proof.
   intros; constructor; intros.
-- rewrite (nextblock_drop _ _ _ _ _ _ H). apply Ple_refl.
+- rewrite (nextblock_drop _ _ _ _ _ _ H). apply Block.le_refl.
 - split; intros. eapply perm_drop_3; eauto.
   destruct (eq_block b0 b); auto.
   subst b0.
diff --git a/common/Memtype.v b/common/Memtype.v
index ae4fa5fdbf..8af4803c05 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -93,6 +93,8 @@ Parameter mem: Type.
 (** [empty] is the initial memory state. *)
 Parameter empty: mem.
 
+Parameter alloc_at: forall (m: mem) (b: block) (lo hi: Z), mem.
+
 (** [alloc m lo hi] allocates a fresh block of size [hi - lo] bytes.
   Valid offsets in this block are between [lo] included and [hi] excluded.
   These offsets are writable in the returned memory state.
@@ -175,7 +177,9 @@ Parameter drop_perm: forall (m: mem) (b: block) (lo hi: Z) (p: permission), opti
 
 Parameter nextblock: mem -> block.
 
-Definition valid_block (m: mem) (b: block) := Plt b (nextblock m).
+Axiom init_nextblock: forall m, Block.le Block.init (nextblock m).
+
+Definition valid_block (m: mem) (b: block) := Block.lt b (nextblock m).
 
 Axiom valid_not_valid_diff:
   forall m b b', valid_block m b -> ~(valid_block m b') -> b <> b'.
@@ -275,7 +279,7 @@ Axiom valid_pointer_implies:
 
 (** ** Properties of the initial memory state. *)
 
-Axiom nextblock_empty: nextblock empty = 1%positive.
+Axiom nextblock_empty: nextblock empty = Block.init.
 Axiom perm_empty: forall b ofs k p, ~perm empty b ofs k p.
 Axiom valid_access_empty:
   forall chunk b ofs p, ~valid_access empty chunk b ofs p.
@@ -592,6 +596,21 @@ Axiom storebytes_split:
      storebytes m b ofs bytes1 = Some m1
   /\ storebytes m1 b (ofs + Z.of_nat(length bytes1)) bytes2 = Some m2.
 
+(** ** Properties of [alloc_at] *)
+
+Axiom nextblock_alloc_at:
+  forall m1 b lo hi m2, alloc_at m1 b lo hi = m2 -> nextblock m2 = nextblock m1.
+
+Axiom perm_alloc_at_1:
+  forall m1 b lo hi m2, alloc_at m1 b lo hi = m2 ->
+  forall b' ofs k p, b' <> b -> perm m1 b' ofs k p -> perm m2 b' ofs k p.
+Axiom perm_alloc_at_2:
+  forall m1 b lo hi m2, alloc_at m1 b lo hi = m2 -> valid_block m1 b ->
+  forall ofs k, lo <= ofs < hi -> perm m2 b ofs k Freeable.
+Axiom perm_alloc_at_3:
+  forall m1 b lo hi m2, alloc_at m1 b lo hi = m2 ->
+  forall ofs k p, perm m2 b ofs k p -> lo <= ofs < hi.
+
 (** ** Properties of [alloc]. *)
 
 (** The identifier of the freshly allocated block is the next block
@@ -605,7 +624,7 @@ Axiom alloc_result:
 
 Axiom nextblock_alloc:
   forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) ->
-  nextblock m2 = Pos.succ (nextblock m1).
+  nextblock m2 = Block.succ (nextblock m1).
 
 Axiom valid_block_alloc:
   forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) ->
@@ -1198,37 +1217,36 @@ Axiom drop_outside_inject:
 (** Memory states that inject into themselves. *)
 
 Definition flat_inj (thr: block) : meminj :=
-  fun (b: block) => if plt b thr then Some(b, 0) else None.
+  fun (b: block) => if Block.lt_dec b thr then Some(b, 0) else None.
 
-Parameter inject_neutral: forall (thr: block) (m: mem), Prop.
+Parameter inject_neutral: forall (m: mem), Prop.
 
 Axiom neutral_inject:
-  forall m, inject_neutral (nextblock m) m ->
-  inject (flat_inj (nextblock m)) m m.
+  forall m, inject_neutral m ->
+  inject (flat_inj Block.init) m m.
 
 Axiom empty_inject_neutral:
-  forall thr, inject_neutral thr empty.
+  inject_neutral empty.
 
-Axiom alloc_inject_neutral:
-  forall thr m lo hi b m',
-  alloc m lo hi = (m', b) ->
-  inject_neutral thr m ->
-  Plt (nextblock m) thr ->
-  inject_neutral thr m'.
+Axiom alloc_at_inject_neutral:
+  forall b m lo hi,
+  inject_neutral m ->
+  Block.lt b Block.init ->
+  inject_neutral (alloc_at m b lo hi).
 
 Axiom store_inject_neutral:
-  forall chunk m b ofs v m' thr,
+  forall chunk m b ofs v m',
   store chunk m b ofs v = Some m' ->
-  inject_neutral thr m ->
-  Plt b thr ->
-  Val.inject (flat_inj thr) v v ->
-  inject_neutral thr m'.
+  inject_neutral m ->
+  Block.lt b Block.init ->
+  Val.inject (flat_inj Block.init) v v ->
+  inject_neutral m'.
 
 Axiom drop_inject_neutral:
-  forall m b lo hi p m' thr,
+  forall m b lo hi p m',
   drop_perm m b lo hi p = Some m' ->
-  inject_neutral thr m ->
-  Plt b thr ->
-  inject_neutral thr m'.
+  inject_neutral m ->
+  Block.lt b Block.init ->
+  inject_neutral m'.
 
 End MEM.
diff --git a/common/Separation.v b/common/Separation.v
index a9642d7240..869fe6520c 100644
--- a/common/Separation.v
+++ b/common/Separation.v
@@ -798,18 +798,18 @@ Qed.
 
 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).
+      (DOMAIN: forall b, Block.lt b bound -> j b = Some(b, 0))
+      (IMAGE: forall b1 b2 delta, j b1 = Some(b2, delta) -> Block.lt b2 bound -> b1 = b2)
+      (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> Block.lt b bound)
+      (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> Block.lt b bound)
+      (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> Block.lt 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 => exists bound, Block.le bound (Mem.nextblock m) /\ globalenv_preserved ge j bound;
   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.
+  rename H into bound. exists bound; split; auto. eapply Block.le_trans; eauto. eapply Mem.unchanged_on_nextblock; eauto.
 Qed.
 Next Obligation.
   tauto.
@@ -841,7 +841,7 @@ Proof.
 - eauto.
 - destruct (j b1) as [[b0 delta0]|] eqn:JB1.
 + 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.
++ exploit H0; eauto. intros (X & Y). elim Y. apply Block.lt_le_trans with bound; auto.
 - eauto.
 - eauto.
 - eauto.
diff --git a/common/Values.v b/common/Values.v
index a20dd567f1..8c694a1925 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -20,9 +20,10 @@ Require Import Coqlib.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
+Require Export BlockNames.
 
-Definition block : Type := positive.
-Definition eq_block := peq.
+Definition block : Type := Block.t.
+Definition eq_block := Block.eq.
 
 (** A value is either:
 - a machine integer;
diff --git a/driver/Interp.ml b/driver/Interp.ml
index 6760e76c73..01c3ce6e13 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -23,6 +23,7 @@ open Events
 open Ctypes
 open Csyntax
 open Csem
+open BlockNames
 
 (* Configuration *)
 
@@ -228,7 +229,7 @@ let mem_state = function
 
 let compare_state s1 s2 =
   if s1 == s2 then 0 else
-  let c = P.compare (mem_state s1).Mem.nextblock (mem_state s2).Mem.nextblock in
+  let c = Z.to_int (BlockNames.block_compare (mem_state s1).Mem.nextblock (mem_state s2).Mem.nextblock) in
   if c <> 0 then c else begin
   match s1, s2 with
   | State(f1,s1,k1,e1,m1), State(f2,s2,k2,e2,m2) ->
@@ -316,7 +317,7 @@ let format_value m flags length conv arg =
   | 's', "", _ ->
       "<pointer argument expected>"
   | 'p', "", Vptr(blk, ofs) ->
-      Printf.sprintf "<%ld%+ld>" (P.to_int32 blk) (camlint_of_coqint ofs)
+      Printf.sprintf "<%s%+ld>" (camlstring_of_coqstring (Block.to_string blk)) (camlint_of_coqint ofs)
   | 'p', "", Vint i ->
       format_int32 (flags ^ "x") (camlint_of_coqint i)
   | 'p', "", _ ->
diff --git a/extraction/extraction.v b/extraction/extraction.v
index a47a72373a..67fc832e91 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -62,6 +62,14 @@ Extraction NoInline Memory.Mem.valid_pointer.
 (* Errors *)
 Extraction Inline Errors.bind Errors.bind2.
 
+(* AST *)
+Extract Inlined Constant AST.string_of_ident =>
+  "(fun i -> Camlcoq.coqstring_of_camlstring (Camlcoq.extern_atom i))".
+
+(* BlockNames *)
+Extract Inlined Constant BlockNames.string_of_pos =>
+  "(fun p -> Camlcoq.coqstring_of_camlstring (Printf.sprintf ""%ld"" (Camlcoq.P.to_int32 p)))".
+
 (* Iteration *)
 
 Extract Constant Iteration.GenIter.iterate =>
@@ -167,6 +175,7 @@ Set Extraction AccessOpaque.
 Cd "extraction".
 
 Separate Extraction
+   BlockNames.block_compare
    Compiler.transf_c_program Compiler.transf_cminor_program
    Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
    Ctypes.merge_attributes Ctypes.remove_attributes Ctypes.build_composite_env
diff --git a/lib/Maps.v b/lib/Maps.v
index cfb866baa8..b3ed6ae6bc 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -178,6 +178,9 @@ Module Type MAP.
   Axiom gmap:
     forall (A B: Type) (f: A -> B) (i: elt) (m: t A),
     get i (map f m) = f(get i m).
+  Axiom set2:
+    forall (A: Type) (i: elt) (x y: A) (m: t A),
+    set i y (set i x m) = set i y m.
 End MAP.
 
 (** * An implementation of trees over type [positive] *)
@@ -1046,7 +1049,7 @@ Module Type INDEXED_TYPE.
   Parameter eq: forall (x y: t), {x = y} + {x <> y}.
 End INDEXED_TYPE.
 
-Module IMap(X: INDEXED_TYPE).
+Module IMap(X: INDEXED_TYPE) <: MAP.
 
   Definition elt := X.t.
   Definition elt_eq := X.eq.
@@ -1057,7 +1060,7 @@ Module IMap(X: INDEXED_TYPE).
   Definition map (A B: Type) (f: A -> B) (m: t A) : t B := PMap.map f m.
 
   Lemma gi:
-    forall (A: Type) (x: A) (i: X.t), get i (init x) = x.
+    forall (A: Type) (i: X.t) (x: A), get i (init x) = x.
   Proof.
     intros. unfold get, init. apply PMap.gi.
   Qed.
@@ -1088,6 +1091,16 @@ Module IMap(X: INDEXED_TYPE).
     red; intro. elim n. apply X.index_inj; auto.
   Qed.
 
+  Lemma gsident:
+    forall (A: Type) (i j: X.t) (m: t A),
+    get j (set i (get i m) m) = get j m.
+  Proof.
+    intros.
+    intros. destruct (X.eq i j).
+     rewrite e. rewrite gss. auto.
+     rewrite gso; auto.
+  Qed.
+
   Lemma gmap:
     forall (A B: Type) (f: A -> B) (i: X.t) (m: t A),
     get i (map f m) = f(get i m).
@@ -1147,6 +1160,8 @@ Module NMap := IMap(NIndexed).
 
 (** * An implementation of maps over any type with decidable equality *)
 
+Require Import Axioms. (* functional extensionality is required for set2 *)
+
 Module Type EQUALITY_TYPE.
   Parameter t: Type.
   Parameter eq: forall (x y: t), {x = y} + {x <> y}.
@@ -1199,6 +1214,13 @@ Module EMap(X: EQUALITY_TYPE) <: MAP.
   Proof.
     intros. unfold get, map. reflexivity.
   Qed.
+  Lemma set2:
+    forall (A: Type) (i: elt) (x y: A) (m: t A),
+    set i y (set i x m) = set i y m.
+  Proof.
+    intros. apply functional_extensionality. intros j.
+    unfold set. destruct (X.eq _ _); eauto.
+  Qed.
 End EMap.
 
 (** * A partial implementation of trees over any type that injects into type [positive] *)