Merge of the "princeton" branch:

- Define type "block" as "positive" instead of "Z".
- Strengthen mem_unchanged_on so that the permissions are identical,
  instead of possibly increasing.
- Move mem_unchanged_on from Events to Memory.Mem.
- Define it in terms of mem_contents rather than in terms of Mem.load.
- ExportClight: try to name temporaries introduced by SimplExpr
- SimplExpr: avoid reusing temporaries between different functions,
  instead, thread a single generator through all functions.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2276 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

7 files changed, 153 insertions, 161 deletions

diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v
index f74fba8..3801a4f 100644
--- a/backend/Asmgenproof0.v
+++ b/backend/Asmgenproof0.v
@@ -844,10 +844,10 @@ Inductive match_stack: list Mach.stackframe -> Prop :=
       match_stack (Stackframe fb sp ra c :: s).
 
 Lemma parent_sp_def: forall s, match_stack s -> parent_sp s <> Vundef.
-Proof. induction 1; simpl. congruence. auto. Qed.
+Proof. induction 1; simpl. unfold Vzero; congruence. auto. Qed.
 
 Lemma parent_ra_def: forall s, match_stack s -> parent_ra s <> Vundef.
-Proof. induction 1; simpl. unfold Vzero. congruence. inv H0. congruence. Qed.
+Proof. induction 1; simpl. unfold Vzero; congruence. inv H0. congruence. Qed.
 
 Lemma lessdef_parent_sp:
   forall s v,
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index a6385f4..2d11d94 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -255,7 +255,7 @@ Proof.
   intros. eapply Mem.load_alloc_unchanged; eauto. 
   split. eauto with mem.
   intros; red; intros. exploit Mem.perm_alloc_inv; eauto. 
-  rewrite zeq_false. apply C. eapply Mem.valid_not_valid_diff; eauto with mem.
+  rewrite dec_eq_false. apply C. eapply Mem.valid_not_valid_diff; eauto with mem.
 Qed.
 
 Lemma mem_match_approx_free:
@@ -267,7 +267,7 @@ Proof.
   intros; red; intros. exploit H; eauto. intros [A [B C]].
   split. apply Genv.load_store_init_data_invariant with m; auto.
   intros. eapply Mem.load_free; eauto.
-  destruct (zeq b0 b); auto. subst b0.
+  destruct (eq_block b0 b); auto. subst b0.
   right. destruct (zlt lo hi); auto. 
   elim (C lo). apply Mem.perm_cur_max. 
   exploit Mem.free_range_perm; eauto. instantiate (1 := lo); omega. 
@@ -323,10 +323,10 @@ Proof.
   unfold Genv.add_global, Genv.find_symbol, Genv.find_var_info in *;
   simpl in *.
   destruct EITHER as [[A B] | [A B]].
-  subst id0. rewrite PTree.gss in H1. inv H1. rewrite ZMap.gss. auto.
+  subst id0. rewrite PTree.gss in H1. inv H1. rewrite PTree.gss. auto.
   rewrite PTree.gso in H1; auto. destruct gd. eapply H; eauto. 
-  rewrite ZMap.gso. eapply H; eauto.
-  exploit Genv.genv_symb_range; eauto. unfold ZIndexed.t. omega.
+  rewrite PTree.gso. eapply H; eauto.
+  red; intros; subst b. eelim Plt_strict; eapply Genv.genv_symb_range; eauto.
 Qed.
 
 Theorem mem_match_approx_init:
diff --git a/backend/Inlining.v b/backend/Inlining.v
index 7b19f80..683d190 100644
--- a/backend/Inlining.v
+++ b/backend/Inlining.v
@@ -22,8 +22,6 @@ Require Import Op.
 Require Import Registers.
 Require Import RTL.
 
-Ltac xomega := unfold Plt, Ple in *; zify; omega.
-
 (** ** Environment of inlinable functions *)
 
 (** We maintain a mapping from function names to their definitions.
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index ba61ed0..15d0b28 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -291,7 +291,7 @@ Proof.
   exploit (H ofs). generalize (Zmax2 sz 0). omega. intros [A B].
   split; auto. intros; red; intros.
   exploit Mem.perm_alloc_inv; eauto.
-  destruct (zeq b sp); intros.
+  destruct (eq_block b sp); intros.
   subst b. rewrite H1 in H4; inv H4. 
   rewrite Zmax_spec in H3. destruct (zlt 0 sz); omega.
   rewrite H2 in H4; auto. eelim B; eauto. 
@@ -331,7 +331,7 @@ Lemma range_private_extcall:
   range_private F m1 m1' sp base hi ->
   (forall b ofs p,
      Mem.valid_block m1 b -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) ->
-  mem_unchanged_on (loc_out_of_reach F m1) m1' m2' ->
+  Mem.unchanged_on (loc_out_of_reach F m1) m1' m2' ->
   Mem.inject F m1 m1' ->
   inject_incr F F' ->
   inject_separated F F' m1 m1' ->
@@ -340,26 +340,24 @@ Lemma range_private_extcall:
 Proof.
   intros until hi; intros RP PERM UNCH INJ INCR SEP VB.
   red; intros. exploit RP; eauto. intros [A B].
-  destruct UNCH as [U1 U2].
-  split. auto. 
+  split. eapply Mem.perm_unchanged_on; eauto. 
   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 (zlt b (Mem.nextblock m1)); auto. 
+  red. destruct (plt b (Mem.nextblock m1)); auto. 
   exploit Mem.mi_freeblocks; eauto. congruence.
   exploit SEP; eauto. tauto. 
 Qed.
 
 (** ** Relating global environments *)
 
-Inductive match_globalenvs (F: meminj) (bound: Z): Prop :=
+Inductive match_globalenvs (F: meminj) (bound: block): Prop :=
   | mk_match_globalenvs
-      (POS: bound > 0)
-      (DOMAIN: forall b, b < bound -> F b = Some(b, 0))
-      (IMAGE: forall b1 b2 delta, F b1 = Some(b2, delta) -> b2 < bound -> b1 = b2)
-      (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> b < bound)
-      (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> b < bound)
-      (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound).
+      (DOMAIN: forall b, Plt b bound -> F b = Some(b, 0))
+      (IMAGE: forall b1 b2 delta, F b1 = Some(b2, delta) -> Plt b2 bound -> b1 = b2)
+      (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> Plt b bound)
+      (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> Plt b bound)
+      (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> Plt b bound).
 
 Lemma find_function_agree:
   forall ros rs fd F ctx rs' bound,
@@ -390,7 +388,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: bound1 <= bound),
+        (BELOW: Ple 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 ctx
         (MS: match_stacks_inside F m m' stk stk' f' ctx sp' rs')
@@ -401,7 +399,7 @@ Inductive match_stacks (F: meminj) (m m': mem):
         (SSZ1: 0 <= f'.(fn_stacksize) < Int.max_unsigned)
         (SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize))
         (RES: Ple res ctx.(mreg))
-        (BELOW: sp' < bound),
+        (BELOW: Plt sp' bound),
       match_stacks F m m'
                    (Stackframe res f (Vptr sp Int.zero) pc rs :: stk)
                    (Stackframe (sreg ctx res) f' (Vptr sp' Int.zero) (spc ctx pc) rs' :: stk')
@@ -412,7 +410,7 @@ Inductive match_stacks (F: meminj) (m m': mem):
         (SSZ1: 0 <= f'.(fn_stacksize) < Int.max_unsigned)
         (SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize))
         (RET: ctx.(retinfo) = Some (rpc, res))
-        (BELOW: sp' < bound),
+        (BELOW: Plt sp' bound),
       match_stacks F m m'
                    stk
                    (Stackframe res f' (Vptr sp' Int.zero) rpc rs' :: stk')
@@ -474,13 +472,13 @@ Qed.
 Lemma match_stacks_bound:
   forall stk stk' bound bound1,
   match_stacks F m m' stk stk' bound ->
-  bound <= bound1 ->
+  Ple bound bound1 ->
   match_stacks F m m' stk stk' bound1.
 Proof.
   intros. inv H.
-  apply match_stacks_nil with bound0. auto. omega.
-  eapply match_stacks_cons; eauto. omega.
-  eapply match_stacks_untailcall; eauto. omega. 
+  apply match_stacks_nil with bound0. auto. eapply Ple_trans; eauto. 
+  eapply match_stacks_cons; eauto. eapply Plt_le_trans; eauto. 
+  eapply match_stacks_untailcall; eauto. eapply Plt_le_trans; eauto. 
 Qed. 
 
 Variable F1: meminj.
@@ -490,13 +488,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) -> b2 < bound -> F b1 = Some(b2, delta))
+               F1 b1 = Some(b2, delta) -> Plt b2 bound -> F b1 = Some(b2, delta))
          (PERM1: forall b1 b2 delta ofs,
-               F1 b1 = Some(b2, delta) -> b2 < bound ->
+               F1 b1 = Some(b2, delta) -> Plt b2 bound ->
                Mem.perm m1 b1 ofs Max Nonempty -> Mem.perm m b1 ofs Max Nonempty)
-         (PERM2: forall b ofs, b < bound ->
+         (PERM2: forall b ofs, Plt b bound ->
                Mem.perm m' b ofs Cur Freeable -> Mem.perm m1' b ofs Cur Freeable)
-         (PERM3: forall b ofs k p, b < bound ->
+         (PERM3: forall b ofs k p, Plt b bound ->
                Mem.perm m1' b ofs k p -> Mem.perm m' b ofs k p),
   match_stacks F1 m1 m1' stk stk' bound
 
@@ -506,13 +504,13 @@ with match_stacks_inside_invariant:
   forall rs2
          (RS: forall r, Ple r ctx.(dreg) -> rs2#r = rs1#r)
          (INJ: forall b1 b2 delta, 
-               F1 b1 = Some(b2, delta) -> b2 <= sp' -> F b1 = Some(b2, delta))
+               F1 b1 = Some(b2, delta) -> Ple b2 sp' -> F b1 = Some(b2, delta))
          (PERM1: forall b1 b2 delta ofs,
-               F1 b1 = Some(b2, delta) -> b2 <= sp' ->
+               F1 b1 = Some(b2, delta) -> Ple b2 sp' ->
                Mem.perm m1 b1 ofs Max Nonempty -> Mem.perm m b1 ofs Max Nonempty)
-         (PERM2: forall b ofs, b <= sp' ->
+         (PERM2: forall b ofs, Ple b sp' ->
                Mem.perm m' b ofs Cur Freeable -> Mem.perm m1' b ofs Cur Freeable)
-         (PERM3: forall b ofs k p, b <= sp' ->
+         (PERM3: forall b ofs k p, Ple 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.
 
@@ -521,34 +519,34 @@ Proof.
   (* nil *)
   apply match_stacks_nil with (bound1 := bound1).
   inv MG. constructor; auto. 
-  intros. apply IMAGE with delta. eapply INJ; eauto. omega. auto. 
-  omega.
+  intros. apply IMAGE with delta. eapply INJ; eauto. eapply Plt_le_trans; eauto.
+  auto. auto.
   (* cons *)
   apply match_stacks_cons with (ctx := ctx); auto.
   eapply match_stacks_inside_invariant; eauto.
-  intros; eapply INJ; eauto; omega.
-  intros; eapply PERM1; eauto; omega.
-  intros; eapply PERM2; eauto; omega.
-  intros; eapply PERM3; eauto; omega.
+  intros; eapply INJ; eauto; xomega. 
+  intros; eapply PERM1; eauto; xomega.
+  intros; eapply PERM2; eauto; xomega.
+  intros; eapply PERM3; eauto; xomega.
   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; omega.
-  intros; eapply PERM1; eauto; omega.
-  intros; eapply PERM2; eauto; omega.
-  intros; eapply PERM3; eauto; omega.
+  intros; eapply INJ; eauto; xomega.
+  intros; eapply PERM1; eauto; xomega.
+  intros; eapply PERM2; eauto; xomega.
+  intros; eapply PERM3; eauto; xomega.
   eapply range_private_invariant; eauto. 
 
   induction 1; intros.
   (* base *)
   eapply match_stacks_inside_base; eauto.
   eapply match_stacks_invariant; eauto. 
-  intros; eapply INJ; eauto; omega.
-  intros; eapply PERM1; eauto; omega.
-  intros; eapply PERM2; eauto; omega.
-  intros; eapply PERM3; eauto; omega.
+  intros; eapply INJ; eauto; xomega.
+  intros; eapply PERM1; eauto; xomega.
+  intros; eapply PERM2; eauto; xomega.
+  intros; eapply PERM3; eauto; xomega.
   (* inlined *)
   apply match_stacks_inside_inlined with (ctx' := ctx'); auto. 
   apply IHmatch_stacks_inside; auto.
@@ -557,8 +555,8 @@ Proof.
   apply agree_regs_invariant with rs'; auto. 
   intros. apply RS. red in BELOW. xomega. 
   eapply range_private_invariant; eauto.
-    intros. split. eapply INJ; eauto. omega. eapply PERM1; eauto. omega.
-    intros. eapply PERM2; eauto. omega.
+    intros. split. eapply INJ; eauto. xomega. eapply PERM1; eauto. xomega.
+    intros. eapply PERM2; eauto. xomega.
 Qed.
 
 Lemma match_stacks_empty:
@@ -621,17 +619,17 @@ 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. omegaContradiction.
+  subst b1. rewrite H1 in H4; inv H4. eelim Plt_strict; eauto. 
   rewrite H2 in H4; auto. 
-  intros. exploit Mem.perm_alloc_inv; eauto. destruct (zeq b1 b); intros; auto.
-  subst b1. rewrite H1 in H4. inv H4. omegaContradiction.
+  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. 
   (* inlined *)
   eapply match_stacks_inside_inlined; eauto. 
   eapply IHmatch_stacks_inside; eauto. destruct SBELOW. omega. 
   eapply agree_regs_incr; eauto.
   eapply range_private_invariant; eauto. 
-  intros. exploit Mem.perm_alloc_inv; eauto. destruct (zeq b0 b); intros.
-  subst b0. rewrite H2 in H5; inv H5. omegaContradiction. 
+  intros. exploit Mem.perm_alloc_inv; eauto. destruct (eq_block b0 b); intros.
+  subst b0. rewrite H2 in H5; inv H5. elimtype False; xomega. 
   rewrite H3 in H5; auto. 
 Qed.
 
@@ -654,7 +652,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. left. unfold block; omega.
+  intros. eapply Mem.perm_free_1; eauto. 
   intros. eapply Mem.perm_free_3; eauto.
 Qed.
 
@@ -691,7 +689,7 @@ Variables F1 F2: meminj.
 Variables m1 m2 m1' m2': mem.
 Hypothesis MAXPERM: forall b ofs p, Mem.valid_block m1 b -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p.
 Hypothesis MAXPERM': forall b ofs p, Mem.valid_block m1' b -> Mem.perm m2' b ofs Max p -> Mem.perm m1' b ofs Max p.
-Hypothesis UNCHANGED: mem_unchanged_on (loc_out_of_reach F1 m1) m1' m2'.
+Hypothesis UNCHANGED: Mem.unchanged_on (loc_out_of_reach F1 m1) m1' m2'.
 Hypothesis INJ: Mem.inject F1 m1 m1'.
 Hypothesis INCR: inject_incr F1 F2.
 Hypothesis SEP: inject_separated F1 F2 m1 m1'.
@@ -699,12 +697,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 ->
-  bound <= Mem.nextblock m1' ->
+  Ple 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' ->
-  sp' < Mem.nextblock m1' ->
+  Plt sp' (Mem.nextblock m1') ->
   match_stacks_inside F2 m2 m2' stk stk' f' ctx sp' rs'.
 Proof.
   induction 1; intros.
@@ -712,19 +710,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. omega. 
+    exploit SEP; eauto. intros [A B]. elim B. red. xomega. 
   eapply match_stacks_cons; eauto. 
-    eapply match_stacks_inside_extcall; eauto. omega. 
+    eapply match_stacks_inside_extcall; eauto. xomega. 
     eapply agree_regs_incr; eauto. 
-    eapply range_private_extcall; eauto. red; omega. 
-    intros. apply SSZ2; auto. apply MAXPERM'; auto. red; omega.
+    eapply range_private_extcall; eauto. red; xomega. 
+    intros. apply SSZ2; auto. apply MAXPERM'; auto. red; xomega.
   eapply match_stacks_untailcall; eauto. 
-    eapply match_stacks_inside_extcall; eauto. omega. 
-    eapply range_private_extcall; eauto. red; omega. 
-    intros. apply SSZ2; auto. apply MAXPERM'; auto. red; omega.
+    eapply match_stacks_inside_extcall; eauto. xomega. 
+    eapply range_private_extcall; eauto. red; xomega. 
+    intros. apply SSZ2; auto. apply MAXPERM'; auto. red; xomega.
   induction 1; intros.
   eapply match_stacks_inside_base; eauto.
-    eapply match_stacks_extcall; eauto. omega. 
+    eapply match_stacks_extcall; eauto. xomega. 
   eapply match_stacks_inside_inlined; eauto. 
     eapply agree_regs_incr; eauto. 
     eapply range_private_extcall; eauto.
@@ -952,9 +950,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. left; unfold block; omega.
+    intros. eapply Mem.perm_free_1; eauto. 
     intros. eapply Mem.perm_free_3; eauto.
-  erewrite Mem.nextblock_free; eauto. red in VB; omega.
+  erewrite Mem.nextblock_free; eauto. red in VB; xomega.
   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 *)
@@ -1048,9 +1046,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. left; unfold block; omega.
+    intros. eapply Mem.perm_free_1; eauto. 
     intros. eapply Mem.perm_free_3; eauto.
-  erewrite Mem.nextblock_free; eauto. red in VB; omega.
+  erewrite Mem.nextblock_free; eauto. red in VB; xomega.
   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 *)
@@ -1085,25 +1083,25 @@ Proof.
   rewrite <- SP in MS0. 
   eapply match_stacks_invariant; eauto.
     intros. destruct (eq_block b1 stk). 
-    subst b1. rewrite D in H7; inv H7. unfold block in *; omegaContradiction.
+    subst b1. rewrite D in H7; inv H7. subst b2. eelim Plt_strict; eauto.  
     rewrite E in H7; auto. 
     intros. exploit Mem.perm_alloc_inv. eexact H. eauto. 
-    destruct (zeq b1 stk); intros; auto. 
-    subst b1. rewrite D in H7; inv H7. unfold block in *; omegaContradiction.
+    destruct (eq_block b1 stk); intros; auto. 
+    subst b1. rewrite D in H7; inv H7. subst b2. eelim Plt_strict; eauto.  
     intros. eapply Mem.perm_alloc_1; eauto. 
     intros. exploit Mem.perm_alloc_inv. eexact A. eauto. 
-    rewrite zeq_false; auto. unfold block; omega.
+    rewrite dec_eq_false; auto.
   auto. auto. auto. 
   rewrite H4. apply agree_regs_init_regs. eauto. auto. inv H0; auto. congruence. auto.
   eapply Mem.valid_new_block; eauto.
   red; intros. split.
   eapply Mem.perm_alloc_2; eauto. inv H0; xomega.
   intros; red; intros. exploit Mem.perm_alloc_inv. eexact H. eauto.
-  destruct (zeq b stk); intros. 
+  destruct (eq_block b stk); intros. 
   subst. rewrite D in H8; inv H8. inv H0; xomega.
   rewrite E in H8; auto. eelim Mem.fresh_block_alloc. eexact A. eapply Mem.mi_mappedblocks; eauto.
   auto.
-  intros. exploit Mem.perm_alloc_inv; eauto. rewrite zeq_true. omega. 
+  intros. exploit Mem.perm_alloc_inv; eauto. rewrite dec_eq_true. omega. 
 
 (* internal function, inlined *)
   inversion FB; subst.
@@ -1156,7 +1154,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.
-    omega.
+    xomega.
     eapply external_call_nextblock; eauto. 
     auto. auto.
 
@@ -1217,13 +1215,12 @@ Proof.
   instantiate (1 := Mem.flat_inj (Mem.nextblock m0)). 
   apply match_stacks_nil with (Mem.nextblock m0).
   constructor; intros. 
-    apply Mem.nextblock_pos.
-    unfold Mem.flat_inj. apply zlt_true; auto. 
-    unfold Mem.flat_inj in H. destruct (zlt b1 (Mem.nextblock m0)); congruence.
+    unfold Mem.flat_inj. apply pred_dec_true; auto. 
+    unfold Mem.flat_inj in H. destruct (plt b1 (Mem.nextblock m0)); congruence.
     eapply Genv.find_symbol_not_fresh; eauto.
     eapply Genv.find_funct_ptr_not_fresh; eauto.
     eapply Genv.find_var_info_not_fresh; eauto. 
-    omega.
+    apply Ple_refl. 
   eapply Genv.initmem_inject; eauto.
 Qed.
 
diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v
index e8dba67..f41f376 100644
--- a/backend/Inliningspec.v
+++ b/backend/Inliningspec.v
@@ -46,17 +46,17 @@ Proof.
   (* same *)
   subst id0. inv H1. destruct gd. destruct f0. 
   destruct (should_inline id f0).
-  rewrite PTree.gss in H0. rewrite ZMap.gss. inv H0; auto.
+  rewrite PTree.gss in H0. rewrite PTree.gss. inv H0; auto.
   rewrite PTree.grs in H0; discriminate.
   rewrite PTree.grs in H0; discriminate.
   rewrite PTree.grs in H0; discriminate.
   (* different *)
-  destruct gd. rewrite ZMap.gso. eapply H; eauto. 
+  destruct gd. rewrite PTree.gso. eapply H; eauto. 
   destruct f0. destruct (should_inline id f0).
   rewrite PTree.gso in H0; auto.
   rewrite PTree.gro in H0; auto.
   rewrite PTree.gro in H0; auto.
-  exploit Genv.genv_symb_range; eauto. intros [A B]. unfold ZIndexed.t; omega.
+  red; intros; subst b. eelim Plt_strict. eapply Genv.genv_symb_range; eauto.
   rewrite PTree.gro in H0; auto. eapply H; eauto. 
 Qed.
 
diff --git a/backend/Mach.v b/backend/Mach.v
index 316e788..f0fb56a 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -273,7 +273,7 @@ Inductive state: Type :=
 
 Definition parent_sp (s: list stackframe) : val :=
   match s with
-  | nil => Vptr Mem.nullptr Int.zero
+  | nil => Vzero
   | Stackframe f sp ra c :: s' => sp
   end.
 
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index dfa81d8..9b144cb 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -967,7 +967,7 @@ Lemma agree_frame_extcall_invariant:
   (Mem.valid_block m sp -> Mem.valid_block m1 sp) ->
   (forall ofs p, Mem.perm m1 sp ofs Max p -> Mem.perm m sp ofs Max p) ->
   (Mem.valid_block m' sp' -> Mem.valid_block m1' sp') ->
-  mem_unchanged_on (loc_out_of_reach j m) m' m1' ->
+  Mem.unchanged_on (loc_out_of_reach j m) m' m1' ->
   agree_frame j ls ls0 m1 sp m1' sp' parent retaddr.
 Proof.
   intros.
@@ -977,8 +977,8 @@ Proof.
   intros; red; intros. exploit agree_inj_unique; eauto. intros [EQ1 EQ2]; subst.
   red; intros. exploit agree_bounds; eauto. omega. 
   eapply agree_frame_invariant; eauto.
-  intros. apply H3. intros. apply REACH. omega. auto. 
-  intros. apply H3; auto. 
+  intros. eapply Mem.load_unchanged_on; eauto. intros. apply REACH. omega. auto. 
+  intros. eapply Mem.perm_unchanged_on; eauto with mem. auto. 
 Qed.
 
 (** Preservation by parallel stores in the Linear and Mach codes *)
@@ -1000,7 +1000,7 @@ Opaque Int.add.
   eauto with mem.
   eauto with mem.
   intros. rewrite <- H1. eapply Mem.load_store_other; eauto. 
-    destruct (zeq sp' b2); auto.
+    destruct (eq_block sp' b2); auto.
     subst b2. right.
     exploit agree_inj_unique; eauto. intros [P Q]. subst b1 delta.
     exploit Mem.store_valid_access_3. eexact STORE1. intros [A B].
@@ -1462,13 +1462,13 @@ Proof.
 Qed.
 
 Lemma stores_in_frame_contents:
-  forall chunk b ofs sp, b < sp ->
+  forall chunk b ofs sp, Plt b sp ->
   forall m m', stores_in_frame sp m m' -> 
   Mem.load chunk m' b ofs = Mem.load chunk m b ofs.
 Proof.
   induction 2. auto. 
   rewrite IHstores_in_frame. eapply Mem.load_store_other; eauto.
-  left; unfold block; omega.
+  left. apply Plt_ne; auto.
 Qed.
 
 (** As a corollary of the previous lemmas, we obtain the following
@@ -1512,7 +1512,7 @@ Proof.
     instantiate (1 := fe_stack_data fe).
     generalize stack_data_offset_valid (bound_stack_data_pos b) size_no_overflow; omega.
     intros; right. 
-    exploit Mem.perm_alloc_inv. eexact ALLOC'. eauto. rewrite zeq_true. 
+    exploit Mem.perm_alloc_inv. eexact ALLOC'. eauto. rewrite dec_eq_true. 
     generalize size_no_overflow. omega. 
     intros. apply Mem.perm_implies with Freeable; auto with mem. 
     eapply Mem.perm_alloc_2; eauto.
@@ -1552,7 +1552,7 @@ Proof.
     rewrite size_type_chunk. apply offset_of_index_disj_stack_data_2; auto. red; auto.
   (* separation *)
   assert (SEP: forall b0 delta, j' b0 = Some(sp', delta) -> b0 = sp /\ delta = fe_stack_data fe).
-    intros. destruct (zeq b0 sp). 
+    intros. destruct (eq_block b0 sp). 
     subst b0. rewrite MAP1 in H; inv H; auto.
     rewrite MAP2 in H; auto. 
     assert (Mem.valid_block m1' sp'). eapply Mem.valid_block_inject_2; eauto.
@@ -1619,7 +1619,7 @@ Proof.
     (* valid sp' *)
     eapply stores_in_frame_valid with (m := m2'); eauto with mem.
     (* bounds *)
-    exploit Mem.perm_alloc_inv. eexact ALLOC. eauto. rewrite zeq_true. auto.
+    exploit Mem.perm_alloc_inv. eexact ALLOC. eauto. rewrite dec_eq_true. auto.
     (* perms *)
     auto.
     (* wt *)
@@ -1630,7 +1630,7 @@ Proof.
   split. eapply inject_alloc_separated; eauto with mem.
   (* inject *)
   split. eapply stores_in_frame_inject; eauto.
-  intros. exploit Mem.perm_alloc_inv. eexact ALLOC. eauto. rewrite zeq_true. auto.
+  intros. exploit Mem.perm_alloc_inv. eexact ALLOC. eauto. rewrite dec_eq_true. auto.
   (* stores in frame *)
   auto.
 Qed.
@@ -1850,19 +1850,18 @@ End FRAME_PROPERTIES.
 
 (** * Call stack invariant *)
 
-Inductive match_globalenvs (j: meminj) (bound: Z) : Prop :=
+Inductive match_globalenvs (j: meminj) (bound: block) : Prop :=
   | match_globalenvs_intro
-      (POS: bound > 0)
-      (DOMAIN: forall b, b < bound -> j b = Some(b, 0))
-      (IMAGE: forall b1 b2 delta, j b1 = Some(b2, delta) -> b2 < bound -> b1 = b2)
-      (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> b < bound)
-      (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> b < bound)
-      (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound).
+      (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).
 
 Inductive match_stacks (j: meminj) (m m': mem): 
-       list Linear.stackframe -> list stackframe -> signature -> Z -> Z -> Prop :=
+       list Linear.stackframe -> list stackframe -> signature -> block -> block -> Prop :=
   | match_stacks_empty: forall sg hi bound bound',
-      hi <= bound -> hi <= bound' -> match_globalenvs j hi ->
+      Ple hi bound -> Ple hi bound' -> match_globalenvs j hi ->
       tailcall_possible sg ->
       match_stacks j m m' nil nil sg bound bound'
   | match_stacks_cons: forall f sp ls c cs fb sp' ra c' cs' sg bound bound' trf
@@ -1877,8 +1876,8 @@ Inductive match_stacks (j: meminj) (m m': mem):
            In (S Outgoing ofs ty) (loc_arguments sg) ->
            slot_within_bounds (function_bounds f) Outgoing ofs ty)
         (STK: match_stacks j m m' cs cs' (Linear.fn_sig f) sp sp')
-        (BELOW: sp < bound)
-        (BELOW': sp' < bound'),
+        (BELOW: Plt sp bound)
+        (BELOW': Plt sp' bound'),
       match_stacks j m m'
                    (Linear.Stackframe f (Vptr sp Int.zero) ls c :: cs)
                    (Stackframe fb (Vptr sp' Int.zero) ra c' :: cs')
@@ -1890,12 +1889,12 @@ Lemma match_stacks_change_bounds:
   forall j m1 m' cs cs' sg bound bound',
   match_stacks j m1 m' cs cs' sg bound bound' ->
   forall xbound xbound',
-  bound <= xbound -> bound' <= xbound' ->
+  Ple bound xbound -> Ple bound' xbound' ->
   match_stacks j m1 m' cs cs' sg xbound xbound'.
 Proof.
   induction 1; intros. 
-  apply match_stacks_empty with hi; auto. omega. omega.
-  econstructor; eauto. omega. omega.
+  apply match_stacks_empty with hi; auto. apply Ple_trans with bound; eauto. apply Ple_trans with bound'; eauto. 
+  econstructor; eauto. eapply Plt_le_trans; eauto. eapply Plt_le_trans; eauto. 
 Qed.
 
 (** Invariance with respect to change of [m]. *)
@@ -1903,8 +1902,8 @@ Qed.
 Lemma match_stacks_change_linear_mem:
   forall j m1 m2 m' cs cs' sg bound bound',
   match_stacks j m1 m' cs cs' sg bound bound' ->
-  (forall b, b < bound -> Mem.valid_block m1 b -> Mem.valid_block m2 b) ->
-  (forall b ofs p, b < bound -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) ->
+  (forall b, Plt b bound -> Mem.valid_block m1 b -> Mem.valid_block m2 b) ->
+  (forall b ofs p, Plt b bound -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) ->
   match_stacks j m2 m' cs cs' sg bound bound'.
 Proof.
   induction 1; intros.
@@ -1912,8 +1911,8 @@ Proof.
   econstructor; eauto.
   eapply agree_frame_invariant; eauto. 
   apply IHmatch_stacks.
-  intros. apply H0; auto. omega.
-  intros. apply H1. omega. auto.
+  intros. apply H0; auto. apply Plt_trans with sp; auto.
+  intros. apply H1. apply Plt_trans with sp; auto. auto.
 Qed.
 
 (** Invariance with respect to change of [m']. *)
@@ -1921,9 +1920,9 @@ Qed.
 Lemma match_stacks_change_mach_mem:
   forall j m m1' m2' cs cs' sg bound bound',
   match_stacks j m m1' cs cs' sg bound bound' ->
-  (forall b, b < bound' -> Mem.valid_block m1' b -> Mem.valid_block m2' b) ->
-  (forall b ofs k p, b < bound' -> Mem.perm m1' b ofs k p -> Mem.perm m2' b ofs k p) ->
-  (forall chunk b ofs v, b < bound' -> Mem.load chunk m1' b ofs = Some v -> Mem.load chunk m2' b ofs = Some v) ->
+  (forall b, Plt b bound' -> Mem.valid_block m1' b -> Mem.valid_block m2' b) ->
+  (forall b ofs k p, Plt b bound' -> Mem.perm m1' b ofs k p -> Mem.perm m2' b ofs k p) ->
+  (forall chunk b ofs v, Plt b bound' -> Mem.load chunk m1' b ofs = Some v -> Mem.load chunk m2' b ofs = Some v) ->
   match_stacks j m m2' cs cs' sg bound bound'.
 Proof.
   induction 1; intros.
@@ -1931,9 +1930,9 @@ Proof.
   econstructor; eauto.
   eapply agree_frame_invariant; eauto. 
   apply IHmatch_stacks. 
-  intros; apply H0; auto; omega.
-  intros; apply H1; auto; omega.
-  intros; apply H2; auto. omega.
+  intros; apply H0; auto. apply Plt_trans with sp'; auto. 
+  intros; apply H1; auto. apply Plt_trans with sp'; auto. 
+  intros; apply H2; auto. apply Plt_trans with sp'; auto. 
 Qed.
 
 (** A variant of the latter, for use with external calls *)
@@ -1941,10 +1940,10 @@ Qed.
 Lemma match_stacks_change_mem_extcall:
   forall j m1 m2 m1' m2' cs cs' sg bound bound',
   match_stacks j m1 m1' cs cs' sg bound bound' ->
-  (forall b, b < bound -> Mem.valid_block m1 b -> Mem.valid_block m2 b) ->
-  (forall b ofs p, b < bound -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) ->
-  (forall b, b < bound' -> Mem.valid_block m1' b -> Mem.valid_block m2' b) ->
-  mem_unchanged_on (loc_out_of_reach j m1) m1' m2' ->
+  (forall b, Plt b bound -> Mem.valid_block m1 b -> Mem.valid_block m2 b) ->
+  (forall b ofs p, Plt b bound -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) ->
+  (forall b, Plt b bound' -> Mem.valid_block m1' b -> Mem.valid_block m2' b) ->
+  Mem.unchanged_on (loc_out_of_reach j m1) m1' m2' ->
   match_stacks j m2 m2' cs cs' sg bound bound'.
 Proof.
   induction 1; intros.
@@ -1952,9 +1951,9 @@ Proof.
   econstructor; eauto.
   eapply agree_frame_extcall_invariant; eauto.
   apply IHmatch_stacks. 
-  intros; apply H0; auto; omega.
-  intros; apply H1. omega. auto.
-  intros; apply H2; auto; omega.
+  intros; apply H0; auto. apply Plt_trans with sp; auto. 
+  intros; apply H1. apply Plt_trans with sp; auto. auto.
+  intros; apply H2; auto. apply Plt_trans with sp'; auto. 
   auto.
 Qed.
 
@@ -1966,7 +1965,7 @@ Lemma match_stacks_change_meminj:
   inject_separated j j' m1 m1' ->
   forall cs cs' sg bound bound',
   match_stacks j m m' cs cs' sg bound bound' ->
-  bound' <= Mem.nextblock m1' ->
+  Ple bound' (Mem.nextblock m1') ->
   match_stacks j' m m' cs cs' sg bound bound'.
 Proof.
   induction 3; intros.
@@ -1974,10 +1973,11 @@ Proof.
   inv H3. constructor; auto.
   intros. red in H0. case_eq (j b1).
   intros [b' delta'] EQ. rewrite (H _ _ _ EQ) in H3. inv H3. eauto.
-  intros EQ. exploit H0; eauto. intros [A B]. elim B. red. omega. 
+  intros EQ. exploit H0; eauto. intros [A B]. elim B. red.
+  apply Plt_le_trans with hi. auto. apply Ple_trans with bound'; auto.
   econstructor; eauto. 
-  eapply agree_frame_inject_incr; eauto. red; omega. 
-  apply IHmatch_stacks. omega.
+  eapply agree_frame_inject_incr; eauto. red. eapply Plt_le_trans; eauto. 
+  apply IHmatch_stacks. apply Ple_trans with bound'; auto. apply Plt_Ple; auto.
 Qed.
 
 (** Preservation by parallel stores in Linear and Mach. *)
@@ -2007,17 +2007,17 @@ Lemma match_stack_change_extcall:
   external_call ec ge args' m1' t' res' m2' ->
   inject_incr j j' ->
   inject_separated j j' m1 m1' ->
-  mem_unchanged_on (loc_out_of_reach j m1) m1' m2' ->
+  Mem.unchanged_on (loc_out_of_reach j m1) m1' m2' ->
   forall cs cs' sg bound bound',
   match_stacks j m1 m1' cs cs' sg bound bound' ->
-  bound <= Mem.nextblock m1 -> bound' <= Mem.nextblock m1' ->
+  Ple bound (Mem.nextblock m1) -> Ple bound' (Mem.nextblock m1') ->
   match_stacks j' m2 m2' cs cs' sg bound bound'.
 Proof.
   intros. 
   eapply match_stacks_change_meminj; eauto. 
   eapply match_stacks_change_mem_extcall; eauto.
   intros; eapply external_call_valid_block; eauto.
-  intros; eapply external_call_max_perm; eauto. red; omega.
+  intros; eapply external_call_max_perm; eauto. red. eapply Plt_le_trans; eauto. 
   intros; eapply external_call_valid_block; eauto.
 Qed.
 
@@ -2318,7 +2318,7 @@ Variables m m': mem.
 Variable cs: list Linear.stackframe.
 Variable cs': list stackframe.
 Variable sg: signature.
-Variables bound bound': Z.
+Variables bound bound': block.
 Hypothesis MS: match_stacks j m m' cs cs' sg bound bound'.
 Variable ls: locset.
 Variable rs: regset.
@@ -2574,7 +2574,7 @@ Proof.
     exploit agree_bounds. eauto. apply Mem.perm_cur_max. eauto. 
     omega.
   apply match_stacks_change_mach_mem with m'; auto.
-  eauto with mem. eauto with mem. intros. rewrite <- H3; eapply Mem.load_store_other; eauto. left; unfold block; omega.
+  eauto with mem. eauto with mem. intros. rewrite <- H3; eapply Mem.load_store_other; eauto. left; apply Plt_ne; auto. 
   eauto. eauto. auto. 
   apply agree_regs_set_slot. apply agree_regs_undef_regs; auto. 
   destruct sl.
@@ -2687,11 +2687,11 @@ Proof.
   apply match_stacks_change_linear_mem with m. 
   apply match_stacks_change_mach_mem with m'0.
   auto. 
-  eauto with mem. intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega. 
-  intros. rewrite <- H3. eapply Mem.load_free; eauto. left; unfold block; omega.
+  eauto with mem. intros. eapply Mem.perm_free_1; eauto. left; apply Plt_ne; auto. 
+  intros. rewrite <- H3. eapply Mem.load_free; eauto. left; apply Plt_ne; auto. 
   eauto with mem. intros. eapply Mem.perm_free_3; eauto. 
-  apply Zlt_le_weak. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. 
-  apply Zlt_le_weak. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. 
+  apply Plt_Ple. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. 
+  apply Plt_Ple. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. 
   apply zero_size_arguments_tailcall_possible; auto. 
   apply wt_return_regs; auto. eapply match_stacks_wt_locset; eauto. eapply agree_wt_ls; eauto.
 
@@ -2707,8 +2707,8 @@ Proof.
   econstructor; eauto with coqlib.
   inversion H; inversion A; subst.
   eapply match_stack_change_extcall; eauto.
-  apply Zlt_le_weak. change (Mem.valid_block m sp0). eapply agree_valid_linear; eauto.
-  apply Zlt_le_weak. change (Mem.valid_block m'0 sp'). eapply agree_valid_mach; eauto.
+  apply Plt_Ple. change (Mem.valid_block m sp0). eapply agree_valid_linear; eauto.
+  apply Plt_Ple. change (Mem.valid_block m'0 sp'). eapply agree_valid_mach; eauto.
   apply agree_regs_set_regs; auto. apply agree_regs_undef_regs; auto. eapply agree_regs_inject_incr; eauto.
   apply agree_frame_set_regs; auto. apply agree_frame_undef_regs; auto.
   eapply agree_frame_inject_incr; eauto. 
@@ -2733,8 +2733,8 @@ Proof.
   exact symbols_preserved. exact varinfo_preserved.
   econstructor; eauto with coqlib.
   inv H; inv A. eapply match_stack_change_extcall; eauto.
-  apply Zlt_le_weak. change (Mem.valid_block m sp0). eapply agree_valid_linear; eauto.
-  apply Zlt_le_weak. change (Mem.valid_block m'0 sp'). eapply agree_valid_mach; eauto.
+  apply Plt_Ple. change (Mem.valid_block m sp0). eapply agree_valid_linear; eauto.
+  apply Plt_Ple. change (Mem.valid_block m'0 sp'). eapply agree_valid_mach; eauto.
   eapply agree_regs_inject_incr; eauto.
   eapply agree_frame_inject_incr; eauto. 
   apply agree_frame_extcall_invariant with m m'0; auto.
@@ -2796,11 +2796,11 @@ Proof.
   apply match_stacks_change_linear_mem with m. 
   apply match_stacks_change_mach_mem with m'0.
   eauto. 
-  eauto with mem. intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega. 
-  intros. rewrite <- H1. eapply Mem.load_free; eauto. left; unfold block; omega.
+  eauto with mem. intros. eapply Mem.perm_free_1; eauto. left; apply Plt_ne; auto. 
+  intros. rewrite <- H1. eapply Mem.load_free; eauto. left; apply Plt_ne; auto. 
   eauto with mem. intros. eapply Mem.perm_free_3; eauto. 
-  apply Zlt_le_weak. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. 
-  apply Zlt_le_weak. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. 
+  apply Plt_Ple. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. 
+  apply Plt_Ple. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. 
   apply wt_return_regs; auto. eapply match_stacks_wt_locset; eauto. eapply agree_wt_ls; eauto.
 
   (* internal function *)
@@ -2821,9 +2821,9 @@ Proof.
   apply match_stacks_change_mach_mem with m'0.
   apply match_stacks_change_linear_mem with m.
   rewrite SP_EQ; rewrite SP'_EQ.
-  eapply match_stacks_change_meminj; eauto. omega.
+  eapply match_stacks_change_meminj; eauto. apply Ple_refl. 
   eauto with mem. intros. exploit Mem.perm_alloc_inv. eexact H. eauto. 
-  rewrite zeq_false. auto. omega. 
+  rewrite dec_eq_false; auto. apply Plt_ne; auto. 
   intros. eapply stores_in_frame_valid; eauto with mem. 
   intros. eapply stores_in_frame_perm; eauto with mem.
   intros. rewrite <- H1. transitivity (Mem.load chunk m2' b ofs). eapply stores_in_frame_contents; eauto.
@@ -2843,11 +2843,9 @@ Proof.
   exact symbols_preserved. exact varinfo_preserved.
   econstructor; eauto.
   apply match_stacks_change_bounds with (Mem.nextblock m) (Mem.nextblock m'0).
-  inv H0; inv A. eapply match_stack_change_extcall; eauto. omega. omega.
-  exploit external_call_valid_block'. eexact H0. 
-    instantiate (1 := (Mem.nextblock m - 1)). red; omega. unfold Mem.valid_block; omega.
-  exploit external_call_valid_block'. eexact A. 
-    instantiate (1 := (Mem.nextblock m'0 - 1)). red; omega. unfold Mem.valid_block; omega.
+  inv H0; inv A. eapply match_stack_change_extcall; eauto. apply Ple_refl. apply Ple_refl. 
+  eapply external_call_nextblock'; eauto.
+  eapply external_call_nextblock'; eauto.
   inv H0. apply wt_setlist_result. eapply external_call_well_typed; eauto. auto.
   apply agree_regs_set_regs; auto. apply agree_regs_inject_incr with j; auto. 
   apply agree_callee_save_set_result; auto. 
@@ -2873,11 +2871,10 @@ Proof.
   rewrite symbols_preserved. eauto.
   econstructor; eauto.
   eapply Genv.initmem_inject; eauto.
-  apply match_stacks_empty with (Mem.nextblock m0). omega. omega.
+  apply match_stacks_empty with (Mem.nextblock m0). apply Ple_refl. apply Ple_refl. 
   constructor.
-    apply Mem.nextblock_pos.
-    intros. unfold Mem.flat_inj. apply zlt_true; auto.
-    unfold Mem.flat_inj; intros. destruct (zlt b1 (Mem.nextblock m0)); congruence.
+    intros. unfold Mem.flat_inj. apply pred_dec_true; auto.
+    unfold Mem.flat_inj; intros. destruct (plt b1 (Mem.nextblock m0)); congruence.
     intros. change (Mem.valid_block m0 b0). eapply Genv.find_symbol_not_fresh; eauto.
     intros. change (Mem.valid_block m0 b0). eapply Genv.find_funct_ptr_not_fresh; eauto.
     intros. change (Mem.valid_block m0 b0). eapply Genv.find_var_info_not_fresh; eauto.