Replace `omega` tactic with `lia`

Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal.

Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`,
and `xomegaContradiction` with `lia` and `extlia`.

Turn back on the deprecation warning for uses of `omega`.

Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.

12 files changed, 222 insertions, 219 deletions

diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index b08c3ad7..d763c98c 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -290,7 +290,7 @@ Definition assign_copy_ok (ty: type) (b: block) (ofs: ptrofs) (b': block) (ofs':
 Remark check_assign_copy:
   forall (ty: type) (b: block) (ofs: ptrofs) (b': block) (ofs': ptrofs),
   { assign_copy_ok ty b ofs b' ofs' } + {~ assign_copy_ok ty b ofs b' ofs' }.
-Proof with try (right; intuition omega).
+Proof with try (right; intuition lia).
   intros. unfold assign_copy_ok.
   destruct (Zdivide_dec (alignof_blockcopy ge ty) (Ptrofs.unsigned ofs')); auto...
   destruct (Zdivide_dec (alignof_blockcopy ge ty) (Ptrofs.unsigned ofs)); auto...
@@ -306,8 +306,8 @@ Proof with try (right; intuition omega).
   destruct (zeq (Ptrofs.unsigned ofs') (Ptrofs.unsigned ofs)); auto.
   destruct (zle (Ptrofs.unsigned ofs' + sizeof ge ty) (Ptrofs.unsigned ofs)); auto.
   destruct (zle (Ptrofs.unsigned ofs + sizeof ge ty) (Ptrofs.unsigned ofs')); auto.
-  right; intuition omega.
-  destruct Y... left; intuition omega.
+  right; intuition lia.
+  destruct Y... left; intuition lia.
 Defined.
 
 Definition do_assign_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: ptrofs) (v: val): option (world * trace * mem) :=
@@ -579,7 +579,7 @@ Proof with try congruence.
   replace (Vlong Int64.zero) with Vnullptr. split; constructor.
   unfold Vnullptr; rewrite H0; auto.
 + destruct vargs... mydestr.
-  split. apply SIZE in Heqo0. econstructor; eauto. congruence. omega.
+  split. apply SIZE in Heqo0. econstructor; eauto. congruence. lia.
   constructor.
 - (* EF_memcpy *)
   unfold do_ef_memcpy. destruct vargs... destruct v... destruct vargs...
@@ -636,7 +636,7 @@ Proof.
   inv H0. erewrite SIZE by eauto. rewrite H1, H2. auto.
 - (* EF_free *)
   inv H; unfold do_ef_free.
-+ inv H0. rewrite H1. erewrite SIZE by eauto. rewrite zlt_true. rewrite H3. auto. omega.
++ inv H0. rewrite H1. erewrite SIZE by eauto. rewrite zlt_true. rewrite H3. auto. lia.
 + inv H0. unfold Vnullptr; destruct Archi.ptr64; auto.
 - (* EF_memcpy *)
   inv H; unfold do_ef_memcpy.
diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index 8ab29fe9..239ca370 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -739,7 +739,7 @@ Proof.
   exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]].
   exists (Returnstate vres2 k m2). econstructor; eauto.
 (* trace length *)
-  red; simpl; intros. inv H; simpl; try omega.
+  red; simpl; intros. inv H; simpl; try lia.
   eapply external_call_trace_length; eauto.
   eapply external_call_trace_length; eauto.
 Qed.
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index 45c21f96..1b031866 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -240,7 +240,7 @@ Module VarOrder <: TotalLeBool.
   Theorem leb_total: forall v1 v2, leb v1 v2 = true \/ leb v2 v1 = true.
   Proof.
     unfold leb; intros.
-    assert (snd v1 <= snd v2 \/ snd v2 <= snd v1) by omega.
+    assert (snd v1 <= snd v2 \/ snd v2 <= snd v1) by lia.
     unfold proj_sumbool. destruct H; [left|right]; apply zle_true; auto.
   Qed.
 End VarOrder.
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 5acb996d..bc1c92ca 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -287,7 +287,7 @@ Lemma match_env_external_call:
 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. extlia.
 Qed.
 
 (** [match_env] and allocations *)
@@ -317,18 +317,18 @@ Proof.
   constructor; eauto.
   constructor.
 (* low-high *)
-  rewrite NEXTBLOCK; xomega.
+  rewrite NEXTBLOCK; extlia.
 (* 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; extlia.
+  exploit me_bounded0; eauto. rewrite NEXTBLOCK; extlia.
 (* 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 *; extlia.
 Qed.
 
 (** The sizes of blocks appearing in [e] are respected. *)
@@ -512,23 +512,23 @@ Proof.
   (* base case *)
   econstructor; eauto.
   inv H. constructor; intros; eauto.
-  eapply IMAGE; eauto. eapply H6; eauto. xomega.
+  eapply IMAGE; eauto. eapply H6; eauto. extlia.
   (* inductive case *)
   assert (Ple 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. extlia.
   eapply match_bounds_invariant; eauto.
     intros. eapply H1; eauto.
-    exploit me_bounded; eauto. xomega.
+    exploit me_bounded; eauto. extlia.
   eapply padding_freeable_invariant; eauto.
-    intros. apply H3. xomega.
+    intros. apply H3. extlia.
   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. extlia.
+    intros. eapply H2; eauto. extlia.
+    intros. eapply H3; eauto. extlia.
+    intros. eapply H4; eauto. extlia.
 Qed.
 
 Lemma match_callstack_incr_bound:
@@ -538,8 +538,8 @@ Lemma match_callstack_incr_bound:
   match_callstack f m tm cs bound' tbound'.
 Proof.
   intros. inv H.
-  econstructor; eauto. xomega. xomega.
-  constructor; auto. xomega. xomega.
+  econstructor; eauto. extlia. extlia.
+  constructor; auto. extlia. extlia.
 Qed.
 
 (** Assigning a temporary variable. *)
@@ -596,17 +596,17 @@ Proof.
   auto.
   inv A. assert (Mem.range_perm m b 0 sz Cur Freeable).
   eapply free_list_freeable; eauto. eapply in_blocks_of_env; eauto.
-  replace ofs with ((ofs - delta) + delta) by omega.
-  eapply Mem.perm_inject; eauto. apply H3. omega.
+  replace ofs with ((ofs - delta) + delta) by lia.
+  eapply Mem.perm_inject; eauto. apply H3. lia.
   destruct X as  [tm' FREE].
   exploit nextblock_freelist; eauto. intro NEXT.
   exploit Mem.nextblock_free; eauto. intro NEXT'.
   exists tm'. split. auto. split.
   rewrite NEXT; rewrite NEXT'.
-  apply match_callstack_incr_bound with lo sp; try omega.
+  apply match_callstack_incr_bound with lo sp; try lia.
   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; extlia. extlia. extlia.
   eapply Mem.free_inject; eauto.
   intros. exploit me_inv0; eauto. intros [id [sz A]].
   exists 0; exists sz; split.
@@ -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. extlia.
 (* 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.
+  exploit SEPARATED; eauto. intros [A B]. elim B. red. extlia.
   intros. assert (Ple 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. extlia.
   eapply match_bounds_invariant; eauto.
-  intros. eapply MAXPERMS; eauto. red. exploit me_bounded; eauto. xomega.
+  intros. eapply MAXPERMS; eauto. red. exploit me_bounded; eauto. extlia.
   (* padding-freeable *)
   red; intros.
   destruct (is_reachable_from_env_dec f1 e sp ofs).
@@ -660,10 +660,10 @@ Proof.
   red; intros; red; intros. elim H3.
   exploit me_inv; eauto. intros [id [lv B]].
   exploit BOUND0; eauto. intros C.
-  apply is_reachable_intro with id b0 lv delta; auto; omega.
+  apply is_reachable_intro with id b0 lv delta; auto; lia.
   eauto with mem.
   (* induction *)
-  eapply IHmatch_callstack; eauto. inv MENV; xomega. xomega.
+  eapply IHmatch_callstack; eauto. inv MENV; extlia. extlia.
 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.
+  extlia.
+  unfold block in *; extlia.
   auto.
   constructor; intros.
     rewrite H3. rewrite PTree.gempty. constructor.
-    xomega.
+    extlia.
     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.
@@ -719,23 +719,23 @@ Proof.
   exploit Mem.alloc_result; eauto. intros RES.
   assert (LO: Ple lo (Mem.nextblock m1)) by (eapply me_low_high; eauto).
   constructor.
-  xomega.
+  extlia.
   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. unfold block in *; extlia.
   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.
+  unfold block in *; extlia.
+  intros. apply H4. unfold block in *; extlia.
   intros. destruct (eq_block b0 b).
-  subst b0. rewrite H3 in H. inv H. xomegaContradiction.
+  subst b0. rewrite H3 in H. inv H. extlia.
   rewrite H4 in H; auto.
 Qed.
 
@@ -828,11 +828,11 @@ Proof.
     eexact MINJ.
     eexact H.
     eexact VALID.
-    instantiate (1 := ofs). zify. omega.
-    intros. exploit STKSIZE; eauto. omega.
-    intros. apply STKPERMS. zify. omega.
-    replace (sz - 0) with sz by omega. auto.
-    intros. eapply SEP2. eauto with coqlib. eexact CENV. eauto. eauto. omega.
+    instantiate (1 := ofs). zify. lia.
+    intros. exploit STKSIZE; eauto. lia.
+    intros. apply STKPERMS. zify. lia.
+    replace (sz - 0) with sz by lia. auto.
+    intros. eapply SEP2. eauto with coqlib. eexact CENV. eauto. eauto. lia.
   intros [f2 [A [B [C D]]]].
   exploit (IHalloc_variables f2); eauto.
     red; intros. eapply COMPAT. auto with coqlib.
@@ -841,7 +841,7 @@ Proof.
     subst b. rewrite C in H5; inv H5.
     exploit SEP1. eapply in_eq. eapply in_cons; eauto. eauto. eauto.
     red; intros; subst id0. elim H3. change id with (fst (id, sz0)). apply in_map; auto.
-    omega.
+    lia.
     eapply SEP2. apply in_cons; eauto. eauto.
     rewrite D in H5; eauto. eauto. auto.
     intros. rewrite PTree.gso. eapply UNBOUND; eauto with coqlib.
@@ -890,9 +890,9 @@ Remark block_alignment_pos:
   forall sz, block_alignment sz > 0.
 Proof.
   unfold block_alignment; intros.
-  destruct (zlt sz 2). omega.
-  destruct (zlt sz 4). omega.
-  destruct (zlt sz 8); omega.
+  destruct (zlt sz 2). lia.
+  destruct (zlt sz 4). lia.
+  destruct (zlt sz 8); lia.
 Qed.
 
 Remark assign_variable_incr:
@@ -901,8 +901,8 @@ Remark assign_variable_incr:
 Proof.
   simpl; intros. inv H.
   generalize (align_le stksz (block_alignment sz) (block_alignment_pos sz)).
-  assert (0 <= Z.max 0 sz). apply Zmax_bound_l. omega.
-  omega.
+  assert (0 <= Z.max 0 sz). apply Zmax_bound_l. lia.
+  lia.
 Qed.
 
 Remark assign_variables_incr:
@@ -910,7 +910,7 @@ Remark assign_variables_incr:
   assign_variables (cenv, sz) vars = (cenv', sz') -> sz <= sz'.
 Proof.
   induction vars; intros until sz'.
-  simpl; intros. inv H. omega.
+  simpl; intros. inv H. lia.
 Opaque assign_variable.
   destruct a as [id s]. simpl. intros.
   destruct (assign_variable (cenv, sz) (id, s)) as [cenv1 sz1] eqn:?.
@@ -931,11 +931,11 @@ Proof.
   assert (2 | 8). exists 4; auto.
   assert (4 | 8). exists 2; auto.
   destruct (zlt sz 2).
-  destruct chunk; simpl in *; auto; omegaContradiction.
+  destruct chunk; simpl in *; auto; extlia.
   destruct (zlt sz 4).
-  destruct chunk; simpl in *; auto; omegaContradiction.
+  destruct chunk; simpl in *; auto; extlia.
   destruct (zlt sz 8).
-  destruct chunk; simpl in *; auto; omegaContradiction.
+  destruct chunk; simpl in *; auto; extlia.
   destruct chunk; simpl; auto.
   apply align_divides. apply block_alignment_pos.
 Qed.
@@ -948,7 +948,7 @@ Proof.
   replace (block_alignment sz) with (block_alignment (Z.max 0 sz)).
   apply inj_offset_aligned_block.
   rewrite Zmax_spec. destruct (zlt sz 0); auto.
-  transitivity 1. reflexivity. unfold block_alignment. rewrite zlt_true. auto. omega.
+  transitivity 1. reflexivity. unfold block_alignment. rewrite zlt_true. auto. lia.
 Qed.
 
 Lemma assign_variable_sound:
@@ -976,23 +976,23 @@ Proof.
   exploit COMPAT; eauto. intros [ofs [A [B [C D]]]].
   exists ofs.
   split. rewrite PTree.gso; auto.
-  split. auto. split. auto. zify; omega.
+  split. auto. split. auto. zify; lia.
   inv P. exists (align sz1 (block_alignment sz)).
   split. apply PTree.gss.
   split. apply inj_offset_aligned_block.
-  split. omega.
-  omega.
+  split. lia.
+  lia.
   apply EITHER in H; apply EITHER in H0.
   destruct H as [[P Q] | P]; destruct H0 as [[R S] | R].
   rewrite PTree.gso in *; auto. eapply SEP; eauto.
   inv R. rewrite PTree.gso in H1; auto. rewrite PTree.gss in H2; inv H2.
   exploit COMPAT; eauto. intros [ofs [A [B [C D]]]].
   assert (ofs = ofs1) by congruence. subst ofs.
-  left. zify; omega.
+  left. zify; lia.
   inv P. rewrite PTree.gso in H2; auto. rewrite PTree.gss in H1; inv H1.
   exploit COMPAT; eauto. intros [ofs [A [B [C D]]]].
   assert (ofs = ofs2) by congruence. subst ofs.
-  right. zify; omega.
+  right. zify; lia.
   congruence.
 Qed.
 
@@ -1023,7 +1023,7 @@ Proof.
     split. rewrite map_app. apply list_norepet_append_commut. simpl. constructor; auto.
     rewrite map_app. simpl. red; intros. rewrite in_app in H4. destruct H4.
     eauto. simpl in H4. destruct H4. subst y. red; intros; subst x. tauto. tauto.
-    generalize (assign_variable_incr _ _ _ _ _ _ Heqp). omega.
+    generalize (assign_variable_incr _ _ _ _ _ _ Heqp). lia.
     auto. auto.
   rewrite app_ass. auto.
 Qed.
@@ -1054,7 +1054,7 @@ Proof.
     eexact H.
     simpl. rewrite app_nil_r. apply permutation_norepet with (map fst vars1); auto.
     apply Permutation_map. auto.
-    omega.
+    lia.
     red; intros. contradiction.
     red; intros. contradiction.
   destruct H1 as [A B]. split.
@@ -1680,11 +1680,11 @@ Lemma switch_table_default:
   /\ snd (switch_table sl base) = (n + base)%nat.
 Proof.
   induction sl; simpl; intros.
-- exists O; split. constructor. omega.
+- exists O; split. constructor. lia.
 - destruct o.
   + destruct (IHsl (S base)) as (n & P & Q). exists (S n); split.
     constructor; auto.
-    destruct (switch_table sl (S base)) as [tbl dfl]; simpl in *. omega.
+    destruct (switch_table sl (S base)) as [tbl dfl]; simpl in *. lia.
   + exists O; split. constructor.
     destruct (switch_table sl (S base)) as [tbl dfl]; simpl in *. auto.
 Qed.
@@ -1708,11 +1708,11 @@ Proof.
   exists O; split; auto. constructor.
   specialize (IHsl (S base) dfl). rewrite ST in IHsl. simpl in *.
   destruct (select_switch_case i sl).
-  destruct IHsl as (x & P & Q). exists (S x); split. constructor; auto. omega.
+  destruct IHsl as (x & P & Q). exists (S x); split. constructor; auto. lia.
   auto.
   specialize (IHsl (S base) dfl). rewrite ST in IHsl. simpl in *.
   destruct (select_switch_case i sl).
-  destruct IHsl as (x & P & Q). exists (S x); split. constructor; auto. omega.
+  destruct IHsl as (x & P & Q). exists (S x); split. constructor; auto. lia.
   auto.
 Qed.
 
@@ -1725,10 +1725,10 @@ Proof.
   unfold select_switch; intros.
   generalize (switch_table_case i sl O (snd (switch_table sl O))).
   destruct (select_switch_case i sl) as [sl'|].
-  intros (n & P & Q). replace (n + O)%nat with n in Q by omega. congruence.
+  intros (n & P & Q). replace (n + O)%nat with n in Q by lia. congruence.
   intros E; rewrite E.
   destruct (switch_table_default sl O) as (n & P & Q).
-  replace (n + O)%nat with n in Q by omega. congruence.
+  replace (n + O)%nat with n in Q by lia. congruence.
 Qed.
 
 Inductive transl_lblstmt_cont(cenv: compilenv) (xenv: exit_env): lbl_stmt -> cont -> cont -> Prop :=
@@ -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.
+    extlia. extlia.
     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.
+  extlia. extlia.
   eapply external_call_nextblock; eauto.
   eapply external_call_nextblock; eauto.
 
@@ -2235,7 +2235,7 @@ Proof.
   eapply match_callstate with (f := Mem.flat_inj (Mem.nextblock m0)) (cs := @nil frame) (cenv := PTree.empty Z).
   auto.
   eapply Genv.initmem_inject; eauto.
-  apply mcs_nil with (Mem.nextblock m0). apply match_globalenvs_init; auto. xomega. xomega.
+  apply mcs_nil with (Mem.nextblock m0). apply match_globalenvs_init; auto. extlia. extlia.
   constructor. red; auto.
   constructor.
 Qed.
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 6d2b470f..4fa70ae2 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -839,11 +839,11 @@ Proof.
   unfold semantics; intros; red; simpl; intros.
   set (ge := globalenv p) in *.
   assert (DEREF: forall chunk m b ofs t v, deref_loc ge chunk m b ofs t v -> (length t <= 1)%nat).
-    intros. inv H0; simpl; try omega. inv H3; simpl; try omega.
+    intros. inv H0; simpl; try lia. inv H3; simpl; try lia.
   assert (ASSIGN: forall chunk m b ofs t v m', assign_loc ge chunk m b ofs v t m' -> (length t <= 1)%nat).
-    intros. inv H0; simpl; try omega. inv H3; simpl; try omega.
+    intros. inv H0; simpl; try lia. inv H3; simpl; try lia.
   destruct H.
-  inv H; simpl; try omega. inv H0; eauto; simpl; try omega.
+  inv H; simpl; try lia. inv H0; eauto; simpl; try lia.
   eapply external_call_trace_length; eauto.
-  inv H; simpl; try omega. eapply external_call_trace_length; eauto.
+  inv H; simpl; try lia. eapply external_call_trace_length; eauto.
 Qed.
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 1ceb8e4d..6e653e01 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -689,32 +689,32 @@ Proof.
   destruct (zlt 0 sz); try discriminate.
   destruct (zle sz Ptrofs.max_signed); simpl in SEM; inv SEM.
   assert (E1: Ptrofs.signed (Ptrofs.repr sz) = sz).
-  { apply Ptrofs.signed_repr. generalize Ptrofs.min_signed_neg; omega. }
+  { apply Ptrofs.signed_repr. generalize Ptrofs.min_signed_neg; lia. }
   destruct Archi.ptr64 eqn:SF; inversion EQ0; clear EQ0; subst c.
 + assert (E: Int64.signed (Int64.repr sz) = sz).
   { apply Int64.signed_repr.
     replace Int64.max_signed with Ptrofs.max_signed.
-    generalize Int64.min_signed_neg; omega.
+    generalize Int64.min_signed_neg; lia.
     unfold Ptrofs.max_signed, Ptrofs.half_modulus; rewrite Ptrofs.modulus_eq64 by auto. reflexivity. }
   econstructor; eauto with cshm.
   rewrite SF, dec_eq_true. simpl.
   predSpec Int64.eq Int64.eq_spec (Int64.repr sz) Int64.zero.
-  rewrite H in E; rewrite Int64.signed_zero in E; omegaContradiction.
+  rewrite H in E; rewrite Int64.signed_zero in E; extlia.
   predSpec Int64.eq Int64.eq_spec (Int64.repr sz) Int64.mone.
-  rewrite H0 in E; rewrite Int64.signed_mone in E; omegaContradiction.
+  rewrite H0 in E; rewrite Int64.signed_mone in E; extlia.
   rewrite andb_false_r; simpl. unfold Vptrofs; rewrite SF. apply f_equal.
   apply f_equal. symmetry. auto with ptrofs.
 + assert (E: Int.signed (Int.repr sz) = sz).
   { apply Int.signed_repr.
     replace Int.max_signed with Ptrofs.max_signed.
-    generalize Int.min_signed_neg; omega.
+    generalize Int.min_signed_neg; lia.
     unfold Ptrofs.max_signed, Ptrofs.half_modulus, Ptrofs.modulus, Ptrofs.wordsize, Wordsize_Ptrofs.wordsize. rewrite SF. reflexivity.
   }
   econstructor; eauto with cshm. rewrite SF, dec_eq_true. simpl.
   predSpec Int.eq Int.eq_spec (Int.repr sz) Int.zero.
-  rewrite H in E; rewrite Int.signed_zero in E; omegaContradiction.
+  rewrite H in E; rewrite Int.signed_zero in E; extlia.
   predSpec Int.eq Int.eq_spec (Int.repr sz) Int.mone.
-  rewrite H0 in E; rewrite Int.signed_mone in E; omegaContradiction.
+  rewrite H0 in E; rewrite Int.signed_mone in E; extlia.
   rewrite andb_false_r; simpl. unfold Vptrofs; rewrite SF. apply f_equal. apply f_equal.
   symmetry. auto with ptrofs.
 - destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ).
@@ -772,7 +772,7 @@ Proof.
   assert (Int64.unsigned i = Int.unsigned (Int64.loword i)).
   {
     unfold Int64.loword. rewrite Int.unsigned_repr; auto.
-    comput Int.max_unsigned; omega.
+    comput Int.max_unsigned; lia.
   }
   split; auto. unfold Int.ltu. apply zlt_true. rewrite <- H0. tauto.
 Qed.
@@ -786,7 +786,7 @@ Proof.
   assert (Int64.unsigned i = Int.unsigned (Int64.loword i)).
   {
     unfold Int64.loword. rewrite Int.unsigned_repr; auto.
-    comput Int.max_unsigned; omega.
+    comput Int.max_unsigned; lia.
   }
   unfold Int.ltu. apply zlt_true. rewrite <- H0. tauto.
 Qed.
@@ -797,7 +797,7 @@ Lemma small_shift_amount_3:
   Int64.unsigned (Int64.repr (Int.unsigned i)) = Int.unsigned i.
 Proof.
   intros. apply Int.ltu_inv in H. comput (Int.unsigned Int64.iwordsize').
-  apply Int64.unsigned_repr. comput Int64.max_unsigned; omega.
+  apply Int64.unsigned_repr. comput Int64.max_unsigned; lia.
 Qed.
 
 Lemma make_shl_correct: shift_constructor_correct make_shl sem_shl.
diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v
index c235031f..30e5c2ae 100644
--- a/cfrontend/Cstrategy.v
+++ b/cfrontend/Cstrategy.v
@@ -1553,13 +1553,13 @@ Proof.
   exploit external_call_trace_length; eauto. destruct t1; simpl; intros.
   exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]].
   econstructor; econstructor. left; eapply step_builtin; eauto.
-  omegaContradiction.
+  extlia.
   (* external calls *)
   inv H1.
   exploit external_call_trace_length; eauto. destruct t1; simpl; intros.
   exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]].
   exists (Returnstate vres2 k m2); exists E0; right; econstructor; eauto.
-  omegaContradiction.
+  extlia.
 (* well-behaved traces *)
   red; intros. inv H; inv H0; simpl; auto.
   (* valof volatile *)
@@ -1582,10 +1582,10 @@ Proof.
   exploit deref_loc_trace; eauto. destruct t; auto. destruct t; tauto.
   (* builtins *)
   exploit external_call_trace_length; eauto.
-  destruct t; simpl; auto. destruct t; simpl; auto. intros; omegaContradiction.
+  destruct t; simpl; auto. destruct t; simpl; auto. intros; extlia.
   (* external calls *)
   exploit external_call_trace_length; eauto.
-  destruct t; simpl; auto. destruct t; simpl; auto. intros; omegaContradiction.
+  destruct t; simpl; auto. destruct t; simpl; auto. intros; extlia.
 Qed.
 
 (** The main simulation result. *)
@@ -2734,7 +2734,7 @@ Proof.
   cofix COEL.
   intros. inv H.
 (* cons left *)
-  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Ecall a1 (exprlist_app al (Econs x al0)) ty)).
   eauto. eapply leftcontext_compose; eauto. constructor. auto.
   apply exprlist_app_leftcontext; auto. traceEq.
@@ -2745,7 +2745,7 @@ Proof.
   eapply leftcontext_compose; eauto. repeat constructor. auto.
   apply exprlist_app_leftcontext; auto.
   eapply forever_N_star with (a2 := (esizelist al0)).
-  eexact R. simpl; omega.
+  eexact R. simpl; lia.
   change (Econs a1' al0) with (exprlist_app (Econs a1' Enil) al0).
   rewrite <- exprlist_app_assoc.
   eapply COEL. eauto. auto. auto.
@@ -2754,42 +2754,42 @@ Proof.
 
   intros. inv H.
 (* field *)
-  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Efield x f0 ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* valof *)
-  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Evalof x ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* deref *)
-  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Ederef x ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* addrof *)
-  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Eaddrof x ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* unop *)
-  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Eunop op x ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* binop left *)
-  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Ebinop op x a2 ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* binop right *)
   destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Ebinop op x a2 ty)) f k)
   as [P [Q R]].
   eapply leftcontext_compose; eauto. repeat constructor.
-  eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; lia.
   eapply COE with (C := fun x => C(Ebinop op a1' x ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. auto. traceEq.
 (* cast *)
-  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Ecast x ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* seqand left *)
-  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Eseqand x a2 ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* seqand 2 *)
@@ -2802,7 +2802,7 @@ Proof.
   eapply COE with (C := fun x => (C (Eparen x type_bool ty))). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* seqor left *)
-  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Eseqor x a2 ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* seqor 2 *)
@@ -2815,7 +2815,7 @@ Proof.
   eapply COE with (C := fun x => (C (Eparen x type_bool ty))). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* condition top *)
-  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Econdition x a2 a3 ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* condition *)
@@ -2828,33 +2828,33 @@ Proof.
   eapply COE with (C := fun x => (C (Eparen x ty ty))). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* assign left *)
-  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Eassign x a2 ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* assign right *)
   destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Eassign x a2 ty)) f k)
   as [P [Q R]].
   eapply leftcontext_compose; eauto. repeat constructor.
-  eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; lia.
   eapply COE with (C := fun x => C(Eassign a1' x ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. auto. traceEq.
 (* assignop left *)
-  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Eassignop op x a2 tyres ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* assignop right *)
   destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Eassignop op x a2 tyres ty)) f k)
   as [P [Q R]].
   eapply leftcontext_compose; eauto. repeat constructor.
-  eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; lia.
   eapply COE with (C := fun x => C(Eassignop op a1' x tyres ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. auto. traceEq.
 (* postincr *)
-  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Epostincr id x ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* comma left *)
-  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Ecomma x a2 ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* comma right *)
@@ -2865,14 +2865,14 @@ Proof.
   left; eapply step_comma; eauto. reflexivity.
   eapply COE with (C := C); eauto. traceEq.
 (* call left *)
-  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Ecall x a2 ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* call right *)
   destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Ecall x a2 ty)) f k)
   as [P [Q R]].
   eapply leftcontext_compose; eauto. repeat constructor.
-  eapply forever_N_star with (a2 := (esizelist a2)). eexact R. simpl; omega.
+  eapply forever_N_star with (a2 := (esizelist a2)). eexact R. simpl; lia.
   eapply COEL with (al := Enil). eauto. auto. auto. auto. traceEq.
 (* call *)
   destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Ecall x rargs ty)) f k)
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index 7ce50525..0de5075c 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -350,13 +350,16 @@ Fixpoint sizeof (env: composite_env) (t: type) : Z :=
 Lemma sizeof_pos:
   forall env t, sizeof env t >= 0.
 Proof.
-  induction t; simpl; try omega.
-  destruct i; omega.
-  destruct f; omega.
-  destruct Archi.ptr64; omega.
-  change 0 with (0 * Z.max 0 z) at 2. apply Zmult_ge_compat_r. auto. xomega.
-  destruct (env!i). apply co_sizeof_pos. omega.
-  destruct (env!i). apply co_sizeof_pos. omega.
+  induction t; simpl.
+- lia.
+- destruct i; lia.
+- lia.
+- destruct f; lia.
+- destruct Archi.ptr64; lia.
+- change 0 with (0 * Z.max 0 z) at 2. apply Zmult_ge_compat_r. auto. lia.
+- lia.
+- destruct (env!i). apply co_sizeof_pos. lia.
+- destruct (env!i). apply co_sizeof_pos. lia.
 Qed.
 
 (** The size of a type is an integral multiple of its alignment,
@@ -435,18 +438,18 @@ Lemma sizeof_struct_incr:
   forall env m cur, cur <= sizeof_struct env cur m.
 Proof.
   induction m as [|[id t]]; simpl; intros.
-- omega.
+- lia.
 - apply Z.le_trans with (align cur (alignof env t)).
   apply align_le. apply alignof_pos.
   apply Z.le_trans with (align cur (alignof env t) + sizeof env t).
-  generalize (sizeof_pos env t); omega.
+  generalize (sizeof_pos env t); lia.
   apply IHm.
 Qed.
 
 Lemma sizeof_union_pos:
   forall env m, 0 <= sizeof_union env m.
 Proof.
-  induction m as [|[id t]]; simpl; xomega.
+  induction m as [|[id t]]; simpl; extlia.
 Qed.
 
 (** ** Byte offset for a field of a structure *)
@@ -490,7 +493,7 @@ Proof.
   apply align_le. apply alignof_pos. apply sizeof_struct_incr.
   exploit IHfld; eauto. intros [A B]. split; auto.
   eapply Z.le_trans; eauto. apply Z.le_trans with (align pos (alignof env t)).
-  apply align_le. apply alignof_pos. generalize (sizeof_pos env t). omega.
+  apply align_le. apply alignof_pos. generalize (sizeof_pos env t). lia.
 Qed.
 
 Lemma field_offset_in_range:
@@ -637,7 +640,7 @@ Proof.
     destruct n; auto.
     right; right; right. apply Z.min_l.
     rewrite two_power_nat_two_p. rewrite ! Nat2Z.inj_succ.
-    change 8 with (two_p 3). apply two_p_monotone. omega.
+    change 8 with (two_p 3). apply two_p_monotone. lia.
   }
   induction ty; simpl.
   auto.
@@ -654,7 +657,7 @@ Qed.
 Lemma alignof_blockcopy_pos:
   forall env ty, alignof_blockcopy env ty > 0.
 Proof.
-  intros. generalize (alignof_blockcopy_1248 env ty). simpl. intuition omega.
+  intros. generalize (alignof_blockcopy_1248 env ty). simpl. intuition lia.
 Qed.
 
 Lemma sizeof_alignof_blockcopy_compat:
@@ -670,8 +673,8 @@ Proof.
     apply Z.min_case.
     exists (two_p (Z.of_nat n)).
     change 8 with (two_p 3).
-    rewrite <- two_p_is_exp by omega.
-    rewrite two_power_nat_two_p. rewrite !Nat2Z.inj_succ. f_equal. omega.
+    rewrite <- two_p_is_exp by lia.
+    rewrite two_power_nat_two_p. rewrite !Nat2Z.inj_succ. f_equal. lia.
     apply Z.divide_refl.
   }
   induction ty; simpl.
@@ -1090,8 +1093,8 @@ Remark rank_type_members:
   forall ce id t m, In (id, t) m -> (rank_type ce t <= rank_members ce m)%nat.
 Proof.
   induction m; simpl; intros; intuition auto.
-  subst a. xomega.
-  xomega.
+  subst a. extlia.
+  extlia.
 Qed.
 
 Lemma rank_struct_member:
@@ -1104,7 +1107,7 @@ Proof.
   intros; simpl. rewrite H0.
   erewrite co_consistent_rank by eauto.
   exploit (rank_type_members ce); eauto.
-  omega.
+  lia.
 Qed.
 
 Lemma rank_union_member:
@@ -1117,7 +1120,7 @@ Proof.
   intros; simpl. rewrite H0.
   erewrite co_consistent_rank by eauto.
   exploit (rank_type_members ce); eauto.
-  omega.
+  lia.
 Qed.
 
 (** * Programs and compilation units *)
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index d9637b6a..83f3cfe0 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -1428,8 +1428,8 @@ Lemma pres_cast_int_int:
   forall sz sg n, wt_int (cast_int_int sz sg n) sz sg.
 Proof.
   intros. unfold cast_int_int. destruct sz; simpl.
-- destruct sg. apply Int.sign_ext_idem; omega. apply Int.zero_ext_idem; omega.
-- destruct sg. apply Int.sign_ext_idem; omega. apply Int.zero_ext_idem; omega.
+- destruct sg. apply Int.sign_ext_idem; lia. apply Int.zero_ext_idem; lia.
+- destruct sg. apply Int.sign_ext_idem; lia. apply Int.zero_ext_idem; lia.
 - auto.
 - destruct (Int.eq n Int.zero); auto.
 Qed.
@@ -1616,12 +1616,12 @@ Proof.
   unfold access_mode, Val.load_result. remember Archi.ptr64 as ptr64. 
   intros until v; intros AC. destruct ty; simpl in AC; try discriminate AC.
 - destruct i; [destruct s|destruct s|idtac|idtac]; inv AC; simpl.
-  destruct v; auto with ty. constructor; red. apply Int.sign_ext_idem; omega.
-  destruct v; auto with ty. constructor; red. apply Int.zero_ext_idem; omega.
-  destruct v; auto with ty. constructor; red. apply Int.sign_ext_idem; omega.
-  destruct v; auto with ty. constructor; red. apply Int.zero_ext_idem; omega.
+  destruct v; auto with ty. constructor; red. apply Int.sign_ext_idem; lia.
+  destruct v; auto with ty. constructor; red. apply Int.zero_ext_idem; lia.
+  destruct v; auto with ty. constructor; red. apply Int.sign_ext_idem; lia.
+  destruct v; auto with ty. constructor; red. apply Int.zero_ext_idem; lia.
   destruct Archi.ptr64 eqn:SF; destruct v; auto with ty.
-  destruct v; auto with ty. constructor; red. apply Int.zero_ext_idem; omega.
+  destruct v; auto with ty. constructor; red. apply Int.zero_ext_idem; lia.
 - inv AC. destruct Archi.ptr64 eqn:SF; destruct v; auto with ty.
 - destruct f; inv AC; destruct v; auto with ty.
 - inv AC. unfold Mptr. destruct Archi.ptr64 eqn:SF; destruct v; auto with ty.
@@ -1637,16 +1637,16 @@ Proof.
   destruct ty; simpl in ACC; try discriminate. 
 - destruct i; [destruct s|destruct s|idtac|idtac]; inv ACC; unfold decode_val.
   destruct (proj_bytes vl); auto with ty.
-  constructor; red. apply Int.sign_ext_idem; omega.
+  constructor; red. apply Int.sign_ext_idem; lia.
   destruct (proj_bytes vl); auto with ty.
-  constructor; red. apply Int.zero_ext_idem; omega.
+  constructor; red. apply Int.zero_ext_idem; lia.
   destruct (proj_bytes vl); auto with ty.
-  constructor; red. apply Int.sign_ext_idem; omega.
+  constructor; red. apply Int.sign_ext_idem; lia.
   destruct (proj_bytes vl); auto with ty.
-  constructor; red. apply Int.zero_ext_idem; omega.
+  constructor; red. apply Int.zero_ext_idem; lia.
   destruct (proj_bytes vl). auto with ty. destruct Archi.ptr64 eqn:SF; auto with ty. 
   destruct (proj_bytes vl); auto with ty.
-  constructor; red. apply Int.zero_ext_idem; omega.
+  constructor; red. apply Int.zero_ext_idem; lia.
 - inv ACC. unfold decode_val. destruct (proj_bytes vl). auto with ty.
   destruct Archi.ptr64 eqn:SF; auto with ty. 
 - destruct f; inv ACC; unfold decode_val; destruct (proj_bytes vl); auto with ty.
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index 272b929f..10ccbeff 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -561,7 +561,7 @@ Local Opaque sizeof.
 + destruct (zeq sz 0). 
   inv TR. exists (@nil init_data); split; auto. constructor.
   destruct (zle 0 sz).
-  inv TR. econstructor; split. constructor. omega. auto.
+  inv TR. econstructor; split. constructor. lia. auto.
   discriminate.
 + monadInv TR. 
   destruct (transl_init_rec_spec _ _ _ _ EQ) as (d1 & A1 & B1).
@@ -672,8 +672,8 @@ Remark padding_size:
   forall frm to, frm <= to -> idlsize (tr_padding frm to) = to - frm.
 Proof.
   unfold tr_padding; intros. destruct (zlt frm to).
-  simpl. xomega.
-  simpl. omega.
+  simpl. extlia.
+  simpl. lia.
 Qed.
 
 Remark idlsize_app:
@@ -681,7 +681,7 @@ Remark idlsize_app:
 Proof.
   induction d1; simpl; intros.
   auto.
-  rewrite IHd1. omega.
+  rewrite IHd1. lia.
 Qed.
 
 Remark union_field_size:
@@ -690,8 +690,8 @@ Proof.
   induction fl as [|[i t]]; simpl; intros.
 - inv H.
 - destruct (ident_eq f i).
-  + inv H. xomega.
-  + specialize (IHfl H). xomega.
+  + inv H. extlia.
+  + specialize (IHfl H). extlia.
 Qed.
 
 Hypothesis ce_consistent: composite_env_consistent ge.
@@ -712,16 +712,16 @@ with tr_init_struct_size:
 Proof.
 Local Opaque sizeof.
 - destruct 1; simpl.
-+ erewrite transl_init_single_size by eauto. omega.
++ erewrite transl_init_single_size by eauto. lia.
 + Local Transparent sizeof. simpl. eapply tr_init_array_size; eauto. 
-+ replace (idlsize d) with (idlsize d + 0) by omega.
++ replace (idlsize d) with (idlsize d + 0) by lia.
   eapply tr_init_struct_size; eauto. simpl.
   unfold lookup_composite in H. destruct (ge.(genv_cenv)!id) as [co'|] eqn:?; inv H.
   erewrite co_consistent_sizeof by (eapply ce_consistent; eauto).
   unfold sizeof_composite. rewrite H0. apply align_le.
   destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ. apply two_power_nat_pos.
 + rewrite idlsize_app, padding_size. 
-  exploit tr_init_size; eauto. intros EQ; rewrite EQ. omega.
+  exploit tr_init_size; eauto. intros EQ; rewrite EQ. lia.
   simpl. unfold lookup_composite in H. destruct (ge.(genv_cenv)!id) as [co'|] eqn:?; inv H.
   apply Z.le_trans with (sizeof_union ge (co_members co)).
   eapply union_field_size; eauto.
@@ -730,21 +730,21 @@ Local Opaque sizeof.
   destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ. apply two_power_nat_pos.
 
 - destruct 1; simpl.
-+ omega.
++ lia.
 + rewrite Z.mul_comm.
   assert (0 <= sizeof ge ty * sz).
-  { apply Zmult_gt_0_le_0_compat. omega. generalize (sizeof_pos ge ty); omega. }
-  xomega.
+  { apply Zmult_gt_0_le_0_compat. lia. generalize (sizeof_pos ge ty); lia. }
+  extlia.
 + rewrite idlsize_app. 
   erewrite tr_init_size by eauto. 
   erewrite tr_init_array_size by eauto.
   ring.
 
 - destruct 1; simpl; intros.
-+ rewrite padding_size by auto. omega.
++ rewrite padding_size by auto. lia.
 + rewrite ! idlsize_app, padding_size. 
   erewrite tr_init_size by eauto. 
-  rewrite <- (tr_init_struct_size _ _ _ _ _ H0 H1). omega.
+  rewrite <- (tr_init_struct_size _ _ _ _ _ H0 H1). lia.
   unfold pos1. apply align_le. apply alignof_pos. 
 Qed.
 
@@ -806,7 +806,7 @@ Remark exec_init_array_length:
   forall m b ofs ty sz il m',
   exec_init_array m b ofs ty sz il m' -> sz >= 0.
 Proof.
-  induction 1; omega.
+  induction 1; lia.
 Qed.
 
 Lemma store_init_data_list_app:
@@ -847,10 +847,10 @@ Local Opaque sizeof.
   inv H3. simpl. erewrite transl_init_single_steps by eauto. auto.
 - (* array *)
   inv H1. replace (Z.max 0 sz) with sz in H7. eauto.
-  assert (sz >= 0) by (eapply exec_init_array_length; eauto). xomega.
+  assert (sz >= 0) by (eapply exec_init_array_length; eauto). extlia.
 - (* struct *)
   inv H3. unfold lookup_composite in H7. rewrite H in H7. inv H7. 
-  replace ofs with (ofs + 0) by omega. eauto.
+  replace ofs with (ofs + 0) by lia. eauto.
 - (* union *)
   inv H4. unfold lookup_composite in H9. rewrite H in H9. inv H9. rewrite H1 in H12; inv H12. 
   eapply store_init_data_list_app. eauto.
@@ -870,7 +870,7 @@ Local Opaque sizeof.
   inv H4. simpl in H3; inv H3. 
   eapply store_init_data_list_app. apply store_init_data_list_padding.
   rewrite padding_size.
-  replace (ofs + pos0 + (pos2 - pos0)) with (ofs + pos2) by omega.
+  replace (ofs + pos0 + (pos2 - pos0)) with (ofs + pos2) by lia.
   eapply store_init_data_list_app.
   eauto.
   rewrite (tr_init_size _ _ _ H9).
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index 9a3f32ec..2d059ddd 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -1449,13 +1449,13 @@ Proof.
   (* for val *)
   intros [SL1 [TY1 EV1]]. subst sl.
   econstructor; split.
-  right; split. apply star_refl. destruct r; simpl; (contradiction || omega).
+  right; split. apply star_refl. destruct r; simpl; (contradiction || lia).
   econstructor; eauto.
   instantiate (1 := tmps). apply tr_top_val_val; auto.
   (* for effects *)
   intros SL1. subst sl.
   econstructor; split.
-  right; split. apply star_refl. destruct r; simpl; (contradiction || omega).
+  right; split. apply star_refl. destruct r; simpl; (contradiction || lia).
   econstructor; eauto.
   instantiate (1 := tmps). apply tr_top_base. constructor.
   (* for set *)
@@ -1779,7 +1779,7 @@ Proof.
   subst; simpl Kseqlist.
   econstructor; split.
   right; split. rewrite app_ass. rewrite Kseqlist_app. eexact EXEC.
-  simpl. omega.
+  simpl. lia.
   constructor.
   (* for value *)
   exploit tr_simple_lvalue; eauto. intros [SL1 [TY1 EV1]].
@@ -1788,7 +1788,7 @@ Proof.
   subst; simpl Kseqlist.
   econstructor; split.
   right; split. rewrite app_ass. rewrite Kseqlist_app. eexact EXEC.
-  simpl. omega.
+  simpl. lia.
   constructor.
 (* postincr *)
   exploit tr_top_leftcontext; eauto. clear H14.
@@ -1846,7 +1846,7 @@ Proof.
   subst. simpl Kseqlist.
   econstructor; split.
   right; split. rewrite app_ass; rewrite Kseqlist_app. eexact EXEC.
-  simpl; omega.
+  simpl; lia.
   constructor.
   (* for value *)
   exploit tr_simple_lvalue; eauto. intros [SL1 [TY1 EV1]].
@@ -1863,7 +1863,7 @@ Proof.
   subst sl0; simpl Kseqlist.
   econstructor; split.
   right; split. apply star_refl. simpl. apply plus_lt_compat_r.
-  apply (leftcontext_size _ _ _ H). simpl. omega.
+  apply (leftcontext_size _ _ _ H). simpl. lia.
   econstructor; eauto. apply S.
   eapply tr_expr_monotone; eauto.
   auto. auto.
@@ -1885,7 +1885,7 @@ Proof.
   (* for effects *)
   econstructor; split.
   right; split. apply star_refl. simpl. apply plus_lt_compat_r.
-  apply (leftcontext_size _ _ _ H). simpl. omega.
+  apply (leftcontext_size _ _ _ H). simpl. lia.
   econstructor; eauto.
   exploit tr_simple_rvalue; eauto. simpl. intros A. subst sl1.
   apply S. constructor; auto. auto. auto.
@@ -2015,12 +2015,12 @@ Proof.
   inv H6. inv H0.
   econstructor; split.
   right; split. apply push_seq.
-  simpl. omega.
+  simpl. lia.
   econstructor; eauto. constructor. auto.
 (* do 2 *)
   inv H7. inv H6. inv H.
   econstructor; split.
-  right; split. apply star_refl. simpl. omega.
+  right; split. apply star_refl. simpl. lia.
   econstructor; eauto. constructor.
 
 (* seq *)
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 2dd34389..8246a748 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -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.
+  extlia.
   intros. destruct (f b) as [[b'' delta']|] eqn:?. eauto.
   exploit H2; eauto. unfold Mem.valid_block. intros [A B].
-  xomegaContradiction.
+  extlia.
 Qed.
 
 (** Properties of values resulting from a cast *)
@@ -606,7 +606,7 @@ Proof.
   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.
   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. extlia.
 Qed.
 
 Lemma alloc_variables_injective:
@@ -622,12 +622,12 @@ 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. exploit H2; eauto. unfold block; extlia.
+  inv H7. exploit Mem.alloc_result; eauto. exploit H2; eauto. unfold block; extlia.
   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. unfold block; extlia.
+  exploit H2; eauto. exploit Mem.nextblock_alloc; eauto. unfold block; extlia.
 Qed.
 
 Lemma match_alloc_variables:
@@ -719,7 +719,7 @@ 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.
+    unfold block; extlia.
   split. intros. destruct (ident_eq id0 id).
     (* same var *)
     subst id0.
@@ -760,7 +760,7 @@ Proof.
     destruct ty; try destruct i; try destruct s; try destruct f; inv H; auto;
     unfold Mptr; simpl; destruct Archi.ptr64; auto.
   }
-  omega.
+  lia.
 Qed.
 
 Definition env_initial_value (e: env) (m: mem) :=
@@ -778,7 +778,7 @@ Proof.
   apply IHalloc_variables. red; intros. rewrite PTree.gsspec in H2.
   destruct (peq id0 id). inv H2.
   eapply Mem.load_alloc_same'; eauto.
-  omega. rewrite Z.add_0_l. eapply sizeof_by_value; eauto.
+  lia. rewrite Z.add_0_l. eapply sizeof_by_value; eauto.
   apply Z.divide_0_r.
   eapply Mem.load_alloc_other; eauto.
 Qed.
@@ -985,7 +985,7 @@ 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. extlia.
   intros [id0 [ty0 [U [V W]]]]. split; auto.
   destruct (ident_eq id id0). congruence.
   assert (b' <> b').
@@ -1032,34 +1032,34 @@ Proof.
 + (* special case size = 0 *)
   assert (bytes = nil).
   { exploit (Mem.loadbytes_empty m bsrc (Ptrofs.unsigned osrc) (sizeof tge ty)).
-    omega. congruence. }
+    lia. congruence. }
   subst.
   destruct (Mem.range_perm_storebytes tm bdst' (Ptrofs.unsigned (Ptrofs.add odst (Ptrofs.repr delta))) nil)
   as [tm' SB].
-  simpl. red; intros; omegaContradiction.
+  simpl. red; intros; extlia.
   exists tm'.
   split. eapply assign_loc_copy; eauto.
-  intros; omegaContradiction.
-  intros; omegaContradiction.
-  rewrite e; right; omega.
-  apply Mem.loadbytes_empty. omega.
+  intros; extlia.
+  intros; extlia.
+  rewrite e; right; lia.
+  apply Mem.loadbytes_empty. lia.
   split. eapply Mem.storebytes_empty_inject; eauto.
   intros. rewrite <- H0. eapply Mem.load_storebytes_other; eauto.
   left. congruence.
 + (* general case size > 0 *)
   exploit Mem.loadbytes_length; eauto. intros LEN.
   assert (SZPOS: sizeof tge ty > 0).
-  { generalize (sizeof_pos tge ty); omega. }
+  { generalize (sizeof_pos tge ty); lia. }
   assert (RPSRC: Mem.range_perm m bsrc (Ptrofs.unsigned osrc) (Ptrofs.unsigned osrc + sizeof tge ty) Cur Nonempty).
     eapply Mem.range_perm_implies. eapply Mem.loadbytes_range_perm; eauto. auto with mem.
   assert (RPDST: Mem.range_perm m bdst (Ptrofs.unsigned odst) (Ptrofs.unsigned odst + sizeof tge ty) Cur Nonempty).
     replace (sizeof tge ty) with (Z.of_nat (List.length bytes)).
     eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem.
-    rewrite LEN. apply Z2Nat.id. omega.
+    rewrite LEN. apply Z2Nat.id. lia.
   assert (PSRC: Mem.perm m bsrc (Ptrofs.unsigned osrc) Cur Nonempty).
-    apply RPSRC. omega.
+    apply RPSRC. lia.
   assert (PDST: Mem.perm m bdst (Ptrofs.unsigned odst) Cur Nonempty).
-    apply RPDST. omega.
+    apply RPDST. lia.
   exploit Mem.address_inject.  eauto. eexact PSRC. eauto. intros EQ1.
   exploit Mem.address_inject.  eauto. eexact PDST. eauto. intros EQ2.
   exploit Mem.loadbytes_inject; eauto. intros [bytes2 [A B]].
@@ -1244,7 +1244,7 @@ Proof.
   destruct (Mem.range_perm_free m b lo hi) as [m1 A]; auto.
   rewrite A. apply IHl; auto.
   intros. red; intros. eapply Mem.perm_free_1; eauto.
-  exploit H1; eauto. intros [B|B]. auto. right; omega.
+  exploit H1; eauto. intros [B|B]. auto. right; lia.
   eapply H; eauto.
 Qed.
 
@@ -1276,11 +1276,11 @@ Proof.
       change id' with (fst (id', (b', ty'))). apply List.in_map; auto. }
     assert (Mem.perm m b0 0 Max Nonempty).
     { apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable.
-      eapply PERMS; eauto. omega. auto with mem. }
+      eapply PERMS; eauto. lia. auto with mem. }
     assert (Mem.perm m b0' 0 Max Nonempty).
     { apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable.
-      eapply PERMS; eauto. omega. auto with mem. }
-    exploit Mem.mi_no_overlap; eauto. intros [A|A]. auto. omegaContradiction.
+      eapply PERMS; eauto. lia. auto with mem. }
+    exploit Mem.mi_no_overlap; eauto. intros [A|A]. auto. extlia.
 Qed.
 
 Lemma free_list_right_inject:
@@ -1326,7 +1326,7 @@ Local Opaque ge tge.
     unfold block_of_binding in EQ; inv EQ.
     exploit me_mapped; eauto. eapply PTree.elements_complete; eauto.
     intros [b [A B]].
-    change 0 with (0 + 0). replace (sizeof ge ty) with (sizeof ge ty + 0) by omega.
+    change 0 with (0 + 0). replace (sizeof ge ty) with (sizeof ge ty + 0) by lia.
     eapply Mem.range_perm_inject; eauto.
     eapply free_blocks_of_env_perm_2; eauto.
   - (* no overlap *)
@@ -1343,7 +1343,7 @@ Local Opaque ge tge.
   intros [[id [b' ty]] [EQ IN]]. unfold block_of_binding in EQ. inv EQ.
   exploit me_flat; eauto. apply PTree.elements_complete; eauto.
   intros [P Q]. subst delta. eapply free_blocks_of_env_perm_1 with (m := m); eauto.
-  rewrite <- comp_env_preserved. omega.
+  rewrite <- comp_env_preserved. lia.
 Qed.
 
 (** Matching global environments *)
@@ -1577,17 +1577,17 @@ 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. extlia.
   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. extlia.
+  intros. apply INJ1; auto; extlia.
+  intros. eapply INJ2; eauto; extlia.
   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; extlia.
+  intros; apply INJ1. inv H0; extlia.
+  intros; eapply INJ2; eauto. inv H0; extlia.
 Qed.
 
 (** Invariance by assignment to location "above" *)
@@ -1602,9 +1602,9 @@ 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; extlia.
   (* block copy *)
-  eapply Mem.load_storebytes_other; eauto. left. unfold block; xomega.
+  eapply Mem.load_storebytes_other; eauto. left. unfold block; extlia.
 Qed.
 
 (** Invariance by external calls *)
@@ -1622,9 +1622,9 @@ Proof.
   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]. extlia.
   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]. extlia.
 Qed.
 
 (** Invariance by change of bounds *)
@@ -1636,7 +1636,7 @@ Lemma match_cont_incr_bounds:
   Ple bound bound' -> Ple tbound tbound' ->
   match_cont f cenv k tk m bound' tbound'.
 Proof.
-  induction 1; intros; econstructor; eauto; xomega.
+  induction 1; intros; econstructor; eauto; extlia.
 Qed.
 
 (** [match_cont] and call continuations. *)
@@ -1690,7 +1690,7 @@ Proof.
   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 (Plt b' b) by eauto. unfold block; extlia.
 Qed.
 
 Lemma match_cont_free_env:
@@ -1708,9 +1708,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. extlia.
+  rewrite (free_list_nextblock _ _ _ H3). inv H; extlia.
+  rewrite (free_list_nextblock _ _ _ H4). inv H; extlia.
 Qed.
 
 (** Matching of global environments *)
@@ -2018,7 +2018,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. extlia.
   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,7 +2068,7 @@ Proof.
   eapply match_envs_set_opttemp; eauto.
   eapply match_envs_extcall; eauto.
   eapply match_cont_extcall; eauto.
-  inv MENV; xomega. inv MENV; xomega.
+  inv MENV; extlia. inv MENV; extlia.
   eapply Ple_trans; eauto. eapply external_call_nextblock; eauto.
   eapply Ple_trans; eauto. eapply external_call_nextblock; eauto.
 
@@ -2212,11 +2212,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'. extlia.
   eapply alloc_variables_load; eauto.
   apply compat_cenv_for.
-  rewrite (bind_parameters_nextblock _ _ _ _ _ _ H2). xomega.
-  rewrite T; xomega.
+  rewrite (bind_parameters_nextblock _ _ _ _ _ _ H2). extlia.
+  rewrite T; extlia.
 
 (* external function *)
   monadInv TRFD. inv FUNTY.
@@ -2227,7 +2227,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. extlia. extlia.
   eapply external_call_nextblock; eauto.
   eapply external_call_nextblock; eauto.
 
@@ -2262,7 +2262,7 @@ Proof.
   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.
+  extlia. extlia.
   eapply Genv.initmem_inject; eauto.
   constructor.
 Qed.