Merge branch 'kvx-work' into BTL

38 files changed, 774 insertions, 738 deletions

diff --git a/backend/Allocationproof.v b/backend/Allocationproof.v
index 3c7df58a..15cbdcdc 100644
--- a/backend/Allocationproof.v
+++ b/backend/Allocationproof.v
@@ -548,7 +548,7 @@ Proof.
   unfold select_reg_l; intros. destruct H.
   red in H. congruence.
   rewrite Pos.leb_le in *. red in H. destruct H as [A | [A B]].
-  red in A. zify; omega.
+  red in A. zify; lia.
   rewrite <- A; auto.
 Qed.
 
@@ -560,7 +560,7 @@ Proof.
   unfold select_reg_h; intros. destruct H.
   red in H. congruence.
   rewrite Pos.leb_le in *. red in H. destruct H as [A | [A B]].
-  red in A. zify; omega.
+  red in A. zify; lia.
   rewrite A; auto.
 Qed.
 
@@ -568,7 +568,7 @@ Remark select_reg_charact:
   forall r q, select_reg_l r q = true /\ select_reg_h r q = true <-> ereg q = r.
 Proof.
   unfold select_reg_l, select_reg_h; intros; split.
-  rewrite ! Pos.leb_le. unfold reg; zify; omega.
+  rewrite ! Pos.leb_le. unfold reg; zify; lia.
   intros. rewrite H. rewrite ! Pos.leb_refl; auto.
 Qed.
 
diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml
index cc171cae..1017ce26 100644
--- a/backend/Asmexpandaux.ml
+++ b/backend/Asmexpandaux.ml
@@ -58,7 +58,7 @@ let get_current_function_args () =
   (!current_function).fn_sig.sig_args
 
 let is_current_function_variadic () =
-  (!current_function).fn_sig.sig_cc.cc_vararg
+  (!current_function).fn_sig.sig_cc.cc_vararg <> None
 
 let get_current_function_sig () =
   (!current_function).fn_sig
diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v
index 3638c465..85cee14f 100644
--- a/backend/Asmgenproof0.v
+++ b/backend/Asmgenproof0.v
@@ -31,7 +31,7 @@ Require Import Conventions.
 
 (** * Processor registers and register states *)
 
-Hint Extern 2 (_ <> _) => congruence: asmgen.
+Global Hint Extern 2 (_ <> _) => congruence: asmgen.
 
 Lemma ireg_of_eq:
   forall r r', ireg_of r = OK r' -> preg_of r = IR r'.
@@ -56,7 +56,7 @@ Lemma preg_of_data:
 Proof.
   intros. destruct r; reflexivity.
 Qed.
-Hint Resolve preg_of_data: asmgen.
+Global Hint Resolve preg_of_data: asmgen.
 
 Lemma data_diff:
   forall r r',
@@ -64,7 +64,7 @@ Lemma data_diff:
 Proof.
   congruence.
 Qed.
-Hint Resolve data_diff: asmgen.
+Global Hint Resolve data_diff: asmgen.
 
 Lemma preg_of_not_SP:
   forall r, preg_of r <> SP.
@@ -78,7 +78,7 @@ Proof.
   intros. apply data_diff; auto with asmgen.
 Qed.
 
-Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen.
+Global Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen.
 
 Lemma nextinstr_pc:
   forall rs, (nextinstr rs)#PC = Val.offset_ptr rs#PC Ptrofs.one.
@@ -473,7 +473,7 @@ Inductive code_tail: Z -> code -> code -> Prop :=
 Lemma code_tail_pos:
   forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0.
 Proof.
-  induction 1. omega. omega.
+  induction 1. lia. lia.
 Qed.
 
 Lemma find_instr_tail:
@@ -484,8 +484,8 @@ Proof.
   induction c1; simpl; intros.
   inv H.
   destruct (zeq pos 0). subst pos.
-  inv H. auto. generalize (code_tail_pos _ _ _ H4). intro. omegaContradiction.
-  inv H. congruence. replace (pos0 + 1 - 1) with pos0 by omega.
+  inv H. auto. generalize (code_tail_pos _ _ _ H4). intro. extlia.
+  inv H. congruence. replace (pos0 + 1 - 1) with pos0 by lia.
   eauto.
 Qed.
 
@@ -494,8 +494,8 @@ Remark code_tail_bounds_1:
   code_tail ofs fn c -> 0 <= ofs <= list_length_z fn.
 Proof.
   induction 1; intros; simpl.
-  generalize (list_length_z_pos c). omega.
-  rewrite list_length_z_cons. omega.
+  generalize (list_length_z_pos c). lia.
+  rewrite list_length_z_cons. lia.
 Qed.
 
 Remark code_tail_bounds_2:
@@ -505,8 +505,8 @@ Proof.
   assert (forall ofs fn c, code_tail ofs fn c ->
           forall i c', c = i :: c' -> 0 <= ofs < list_length_z fn).
   induction 1; intros; simpl.
-  rewrite H. rewrite list_length_z_cons. generalize (list_length_z_pos c'). omega.
-  rewrite list_length_z_cons. generalize (IHcode_tail _ _ H0). omega.
+  rewrite H. rewrite list_length_z_cons. generalize (list_length_z_pos c'). lia.
+  rewrite list_length_z_cons. generalize (IHcode_tail _ _ H0). lia.
   eauto.
 Qed.
 
@@ -531,7 +531,7 @@ Lemma code_tail_next_int:
 Proof.
   intros. rewrite Ptrofs.add_unsigned, Ptrofs.unsigned_one.
   rewrite Ptrofs.unsigned_repr. apply code_tail_next with i; auto.
-  generalize (code_tail_bounds_2 _ _ _ _ H0). omega.
+  generalize (code_tail_bounds_2 _ _ _ _ H0). lia.
 Qed.
 
 (** [transl_code_at_pc pc fb f c ep tf tc] holds if the code pointer [pc] points
@@ -654,7 +654,7 @@ Opaque transl_instr.
   exists (Ptrofs.repr ofs). red; intros.
   rewrite Ptrofs.unsigned_repr. congruence.
   exploit code_tail_bounds_1; eauto.
-  apply transf_function_len in TF. omega.
+  apply transf_function_len in TF. lia.
 + exists Ptrofs.zero; red; intros. congruence.
 Qed.
 
@@ -663,7 +663,7 @@ End RETADDR_EXISTS.
 Remark code_tail_no_bigger:
   forall pos c1 c2, code_tail pos c1 c2 -> (length c2 <= length c1)%nat.
 Proof.
-  induction 1; simpl; omega.
+  induction 1; simpl; lia.
 Qed.
 
 Remark code_tail_unique:
@@ -671,8 +671,8 @@ Remark code_tail_unique:
   code_tail pos fn c -> code_tail pos' fn c -> pos = pos'.
 Proof.
   induction fn; intros until pos'; intros ITA CT; inv ITA; inv CT; auto.
-  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
-  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
+  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; lia.
+  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; lia.
   f_equal. eauto.
 Qed.
 
@@ -713,13 +713,13 @@ Proof.
   case (is_label lbl a).
   intro EQ; injection EQ; intro; subst c'.
   exists (pos + 1). split. auto. split.
-  replace (pos + 1 - pos) with (0 + 1) by omega. constructor. constructor.
-  rewrite list_length_z_cons. generalize (list_length_z_pos c). omega.
+  replace (pos + 1 - pos) with (0 + 1) by lia. constructor. constructor.
+  rewrite list_length_z_cons. generalize (list_length_z_pos c). lia.
   intros. generalize (IHc (pos + 1) c' H). intros [pos' [A [B C]]].
   exists pos'. split. auto. split.
-  replace (pos' - pos) with ((pos' - (pos + 1)) + 1) by omega.
+  replace (pos' - pos) with ((pos' - (pos + 1)) + 1) by lia.
   constructor. auto.
-  rewrite list_length_z_cons. omega.
+  rewrite list_length_z_cons. lia.
 Qed.
 
 (** Helper lemmas to reason about
@@ -746,7 +746,7 @@ Qed.
 Definition nolabel (i: instruction) :=
   match i with Plabel _ => False | _ => True end.
 
-Hint Extern 1 (nolabel _) => exact I : labels.
+Global Hint Extern 1 (nolabel _) => exact I : labels.
 
 Lemma tail_nolabel_cons:
   forall i c k,
@@ -757,7 +757,7 @@ Proof.
   intros. simpl. rewrite <- H1. destruct i; reflexivity || contradiction.
 Qed.
 
-Hint Resolve tail_nolabel_refl: labels.
+Global Hint Resolve tail_nolabel_refl: labels.
 
 Ltac TailNoLabel :=
   eauto with labels;
diff --git a/backend/Bounds.v b/backend/Bounds.v
index b8c12166..d6b67a02 100644
--- a/backend/Bounds.v
+++ b/backend/Bounds.v
@@ -163,7 +163,7 @@ Proof.
   intros until valu. unfold max_over_list.
   assert (forall l z, fold_left (fun x y => Z.max x (valu y)) l z >= z).
   induction l; simpl; intros.
-  omega. apply Zge_trans with (Z.max z (valu a)).
+  lia. apply Zge_trans with (Z.max z (valu a)).
   auto. apply Z.le_ge. apply Z.le_max_l. auto.
 Qed.
 
@@ -307,7 +307,7 @@ Proof.
             let f := fold_left (fun x y => Z.max x (valu y)) c z in
             z <= f /\ (In x c -> valu x <= f)).
     induction c; simpl; intros.
-    split. omega. tauto.
+    split. lia. tauto.
     elim (IHc (Z.max z (valu a))); intros.
     split. apply Z.le_trans with (Z.max z (valu a)). apply Z.le_max_l. auto.
     intro H1; elim H1; intro.
@@ -446,12 +446,12 @@ Lemma size_callee_save_area_rec_incr:
 Proof.
 Local Opaque mreg_type.
   induction l as [ | r l]; intros; simpl.
-- omega.
+- lia.
 - eapply Z.le_trans. 2: apply IHl.
   generalize (AST.typesize_pos (mreg_type r)); intros.
   apply Z.le_trans with (align ofs (AST.typesize (mreg_type r))).
   apply align_le; auto.
-  omega.
+  lia.
 Qed.
 
 Lemma size_callee_save_area_incr:
diff --git a/backend/CSEdomain.v b/backend/CSEdomain.v
index 34ec0118..f78e1d25 100644
--- a/backend/CSEdomain.v
+++ b/backend/CSEdomain.v
@@ -92,7 +92,7 @@ Record wf_numbering (n: numbering) : Prop := {
       In r (PMap.get v n.(num_val)) -> PTree.get r n.(num_reg) = Some v
 }.
 
-Hint Resolve wf_num_eqs wf_num_reg wf_num_val: cse.
+Global Hint Resolve wf_num_eqs wf_num_reg wf_num_val: cse.
 
 (** Satisfiability of numberings.  A numbering holds in a concrete
   execution state if there exists a valuation assigning values to
@@ -139,7 +139,7 @@ Record numbering_holds (valu: valuation) (ge: genv) (sp: val)
      n.(num_reg)!r = Some v -> rs#r = valu v
 }.
 
-Hint Resolve num_holds_wf num_holds_eq num_holds_reg: cse.
+Global Hint Resolve num_holds_wf num_holds_eq num_holds_reg: cse.
 
 Lemma empty_numbering_holds:
   forall valu ge sp rs m,
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index a7465cee..cf51f5a2 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -132,9 +132,9 @@ Proof.
   exists valu2; splitall.
 + constructor; simpl; intros.
 * constructor; simpl; intros.
-  apply wf_equation_incr with (num_next n). eauto with cse. xomega.
+  apply wf_equation_incr with (num_next n). eauto with cse. extlia.
   rewrite PTree.gsspec in H0. destruct (peq r0 r).
-  inv H0; xomega.
+  inv H0; extlia.
   apply Plt_trans_succ; eauto with cse.
   rewrite PMap.gsspec in H0. destruct (peq v (num_next n)).
   replace r0 with r by (simpl in H0; intuition). rewrite PTree.gss. subst; auto.
@@ -146,8 +146,8 @@ Proof.
   rewrite peq_false. eauto with cse. apply Plt_ne; eauto with cse.
 + unfold valu2. rewrite peq_true; auto.
 + auto.
-+ xomega.
-+ xomega.
++ extlia.
++ extlia.
 Qed.
 
 Lemma valnum_regs_holds:
@@ -162,7 +162,7 @@ Lemma valnum_regs_holds:
   /\ Ple n.(num_next) n'.(num_next).
 Proof.
   induction rl; simpl; intros.
-- inv H0. exists valu1; splitall; auto. red; auto. simpl; tauto. xomega.
+- inv H0. exists valu1; splitall; auto. red; auto. simpl; tauto. extlia.
 - destruct (valnum_reg n a) as [n1 v1] eqn:V1.
   destruct (valnum_regs n1 rl) as [n2 vs] eqn:V2.
   inv H0.
@@ -173,9 +173,9 @@ Proof.
   exists valu3; splitall.
   + auto.
   + simpl; f_equal; auto. rewrite R; auto.
-  + red; intros. transitivity (valu2 v); auto. apply R. xomega.
-  + simpl; intros. destruct H0; auto. subst v1; xomega.
-  + xomega.
+  + red; intros. transitivity (valu2 v); auto. apply R. extlia.
+  + simpl; intros. destruct H0; auto. subst v1; extlia.
+  + extlia.
 Qed.
 
 Lemma find_valnum_rhs_charact:
@@ -331,11 +331,11 @@ Proof.
   { red; intros. unfold valu2. apply peq_false. apply Plt_ne; auto. }
   exists valu2; constructor; simpl; intros.
 + constructor; simpl; intros.
-  * destruct H3. inv H3. simpl; split. xomega.
+  * destruct H3. inv H3. simpl; split. extlia.
     red; intros. apply Plt_trans_succ; eauto.
-    apply wf_equation_incr with (num_next n). eauto with cse. xomega.
+    apply wf_equation_incr with (num_next n). eauto with cse. extlia.
   * rewrite PTree.gsspec in H3. destruct (peq r rd).
-    inv H3. xomega.
+    inv H3. extlia.
     apply Plt_trans_succ; eauto with cse.
   * apply update_reg_charact; eauto with cse.
 + destruct H3. inv H3.
@@ -546,10 +546,10 @@ Lemma store_normalized_range_sound:
 Proof.
   intros. unfold Val.load_result; remember Archi.ptr64 as ptr64.
   destruct chunk; simpl in *; destruct v; auto.
-- inv H. rewrite is_sgn_sign_ext in H4 by omega. rewrite H4; auto.
-- inv H. rewrite is_uns_zero_ext in H4 by omega. rewrite H4; auto.
-- inv H. rewrite is_sgn_sign_ext in H4 by omega. rewrite H4; auto.
-- inv H. rewrite is_uns_zero_ext in H4 by omega. rewrite H4; auto.
+- inv H. rewrite is_sgn_sign_ext in H4 by lia. rewrite H4; auto.
+- inv H. rewrite is_uns_zero_ext in H4 by lia. rewrite H4; auto.
+- inv H. rewrite is_sgn_sign_ext in H4 by lia. rewrite H4; auto.
+- inv H. rewrite is_uns_zero_ext in H4 by lia. rewrite H4; auto.
 - destruct ptr64; auto.
 - destruct ptr64; auto.
 - destruct ptr64; auto.
@@ -608,7 +608,7 @@ Proof.
   simpl.
   rewrite negb_false_iff in H8.
   eapply Mem.load_storebytes_other. eauto.
-  rewrite H6. rewrite Z2Nat.id by omega.
+  rewrite H6. rewrite Z2Nat.id by lia.
   eapply pdisjoint_sound. eauto.
   unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto.
   erewrite <- regs_valnums_sound by eauto. eauto with va.
@@ -620,7 +620,7 @@ Proof.
   destruct a; simpl in H10; try discriminate; simpl; trivial.
   rewrite negb_false_iff in H8.
   eapply Mem.load_storebytes_other. eauto.
-  rewrite H6. rewrite Z2Nat.id by omega.
+  rewrite H6. rewrite Z2Nat.id by lia.
   eapply pdisjoint_sound. eauto.
   unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto.
   erewrite <- regs_valnums_sound by eauto. eauto with va.
@@ -642,39 +642,39 @@ Proof.
   set (n1 := i - ofs1).
   set (n2 := size_chunk chunk).
   set (n3 := sz - (n1 + n2)).
-  replace sz with (n1 + (n2 + n3)) in H by (unfold n3, n2, n1; omega).
+  replace sz with (n1 + (n2 + n3)) in H by (unfold n3, n2, n1; lia).
   exploit Mem.loadbytes_split; eauto.
-  unfold n1; omega.
-  unfold n3, n2, n1; omega.
+  unfold n1; lia.
+  unfold n3, n2, n1; lia.
   intros (bytes1 & bytes23 & LB1 & LB23 & EQ).
   clear H.
   exploit Mem.loadbytes_split; eauto.
-  unfold n2; omega.
-  unfold n3, n2, n1; omega.
+  unfold n2; lia.
+  unfold n3, n2, n1; lia.
   intros (bytes2 & bytes3 & LB2 & LB3 & EQ').
   subst bytes23; subst bytes.
   exploit Mem.load_loadbytes; eauto. intros (bytes2' & A & B).
   assert (bytes2' = bytes2).
-  { replace (ofs1 + n1) with i in LB2 by (unfold n1; omega). unfold n2 in LB2. congruence.  }
+  { replace (ofs1 + n1) with i in LB2 by (unfold n1; lia). unfold n2 in LB2. congruence.  }
   subst bytes2'.
   exploit Mem.storebytes_split; eauto. intros (m1 & SB1 & SB23).
   clear H0.
   exploit Mem.storebytes_split; eauto. intros (m2 & SB2 & SB3).
   clear SB23.
   assert (L1: Z.of_nat (length bytes1) = n1).
-  { erewrite Mem.loadbytes_length by eauto. apply Z2Nat.id. unfold n1; omega. }
+  { erewrite Mem.loadbytes_length by eauto. apply Z2Nat.id. unfold n1; lia. }
   assert (L2: Z.of_nat (length bytes2) = n2).
-  { erewrite Mem.loadbytes_length by eauto. apply Z2Nat.id. unfold n2; omega. }
+  { erewrite Mem.loadbytes_length by eauto. apply Z2Nat.id. unfold n2; lia. }
   rewrite L1 in *. rewrite L2 in *.
   assert (LB': Mem.loadbytes m2 b2 (ofs2 + n1) n2 = Some bytes2).
   { rewrite <- L2. eapply Mem.loadbytes_storebytes_same; eauto. }
   assert (LB'': Mem.loadbytes m' b2 (ofs2 + n1) n2 = Some bytes2).
   { rewrite <- LB'. eapply Mem.loadbytes_storebytes_other; eauto.
-    unfold n2; omega.
-    right; left; omega. }
+    unfold n2; lia.
+    right; left; lia. }
   exploit Mem.load_valid_access; eauto. intros [P Q].
   rewrite B. apply Mem.loadbytes_load.
-  replace (i + (ofs2 - ofs1)) with (ofs2 + n1) by (unfold n1; omega).
+  replace (i + (ofs2 - ofs1)) with (ofs2 + n1) by (unfold n1; lia).
   exact LB''.
   apply Z.divide_add_r; auto.
 Qed.
@@ -719,9 +719,9 @@ Proof with (try discriminate).
     Mem.loadv chunk m (Vptr sp ofs) = Some v ->
     Mem.loadv chunk m' (Vptr sp (Ptrofs.repr j)) = Some v).
   {
-    simpl; intros. rewrite Ptrofs.unsigned_repr by omega.
+    simpl; intros. rewrite Ptrofs.unsigned_repr by lia.
     unfold j, delta. eapply load_memcpy; eauto.
-    apply Zmod_divide; auto. generalize (align_chunk_pos chunk); omega.
+    apply Zmod_divide; auto. generalize (align_chunk_pos chunk); lia.
   }
   inv H2.
 + inv H3. exploit eval_addressing_Ainstack_inv; eauto. intros [E1 E2].
diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v
index 84ca403e..39c3919f 100644
--- a/backend/CleanupLabelsproof.v
+++ b/backend/CleanupLabelsproof.v
@@ -298,7 +298,7 @@ Proof.
   constructor.
   econstructor; eauto with coqlib.
   (* eliminated *)
-  right. split. simpl. omega. split. auto. econstructor; eauto with coqlib.
+  right. split. simpl. lia. split. auto. econstructor; eauto with coqlib.
 (* Lgoto *)
   left; econstructor; split.
   econstructor. eapply find_label_translated; eauto. red; auto.
diff --git a/backend/Cminor.v b/backend/Cminor.v
index dcebbb86..829adca0 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -6,10 +6,11 @@
 (*                                                                     *)
 (*  Copyright Institut National de Recherche en Informatique et en     *)
 (*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the GNU General Public License as published by  *)
-(*  the Free Software Foundation, either version 2 of the License, or  *)
-(*  (at your option) any later version.  This file is also distributed *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*  under the terms of the GNU Lesser General Public License as        *)
+(*  published by the Free Software Foundation, either version 2.1 of   *)
+(*  the License, or  (at your option) any later version.               *)
+(*  This file is also distributed under the terms of the               *)
+(*  INRIA Non-Commercial License Agreement.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
@@ -590,7 +591,7 @@ Proof.
   exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]].
   exists (Returnstate vres2 k m2). econstructor; eauto.
 (* trace length *)
-  red; intros; inv H; simpl; try omega; eapply external_call_trace_length; eauto.
+  red; intros; inv H; simpl; try lia; eapply external_call_trace_length; eauto.
 Qed.
 
 (** This semantics is determinate. *)
@@ -647,7 +648,7 @@ Proof.
     intros (A & B). split; intros; auto.
     apply B in H; destruct H; congruence.
 - (* single event *)
-  red; simpl. destruct 1; simpl; try omega;
+  red; simpl. destruct 1; simpl; try lia;
   eapply external_call_trace_length; eauto.
 - (* initial states *)
   inv H; inv H0. unfold ge0, ge1 in *. congruence.
diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index 26f47e23..cedd2bed 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -464,7 +464,7 @@ Inductive final_state: state -> int -> Prop :=
 Definition semantics (p: program) :=
   Semantics step (initial_state p) final_state (Genv.globalenv p).
 
-Hint Constructors eval_expr eval_exprlist eval_condexpr: evalexpr.
+Global Hint Constructors eval_expr eval_exprlist eval_condexpr: evalexpr.
 
 (** * Lifting of let-bound variables *)
 
@@ -522,9 +522,9 @@ Lemma insert_lenv_lookup1:
   nth_error le' n = Some v.
 Proof.
   induction 1; intros.
-  omegaContradiction.
+  extlia.
   destruct n; simpl; simpl in H0. auto.
-  apply IHinsert_lenv. auto. omega.
+  apply IHinsert_lenv. auto. lia.
 Qed.
 
 Lemma insert_lenv_lookup2:
@@ -536,8 +536,8 @@ Lemma insert_lenv_lookup2:
 Proof.
   induction 1; intros.
   simpl. assumption.
-  simpl. destruct n. omegaContradiction.
-  apply IHinsert_lenv. exact H0. omega.
+  simpl. destruct n. extlia.
+  apply IHinsert_lenv. exact H0. lia.
 Qed.
 
 Lemma eval_lift_expr:
@@ -580,4 +580,4 @@ Proof.
   eexact H. apply insert_lenv_0.
 Qed.
 
-Hint Resolve eval_lift: evalexpr.
+Global Hint Resolve eval_lift: evalexpr.
diff --git a/backend/Cminortyping.v b/backend/Cminortyping.v
index 8945cecf..d9e99122 100644
--- a/backend/Cminortyping.v
+++ b/backend/Cminortyping.v
@@ -291,7 +291,7 @@ Lemma expect_incr: forall te e t1 t2 e',
 Proof.
   unfold expect; intros. destruct (typ_eq t1 t2); inv H; auto.
 Qed.
-Hint Resolve expect_incr: ty.
+Global Hint Resolve expect_incr: ty.
 
 Lemma expect_sound: forall e t1 t2 e',
   expect e t1 t2 = OK e' -> t1 = t2.
@@ -306,7 +306,7 @@ Proof.
 - destruct (type_unop u) as [targ1 tres]; monadInv T; eauto with ty.
 - destruct (type_binop b) as [[targ1 targ2] tres]; monadInv T; eauto with ty.
 Qed.
-Hint Resolve type_expr_incr: ty.
+Global Hint Resolve type_expr_incr: ty.
 
 Lemma type_expr_sound: forall te a t e e',
     type_expr e a t = OK e' -> S.satisf te e' -> wt_expr te a t.
@@ -326,7 +326,7 @@ Lemma type_exprlist_incr: forall te al tl e e',
 Proof.
   induction al; destruct tl; simpl; intros until e'; intros T SAT; monadInv T; eauto with ty.
 Qed.
-Hint Resolve type_exprlist_incr: ty.
+Global Hint Resolve type_exprlist_incr: ty.
 
 Lemma type_exprlist_sound: forall te al tl e e',
     type_exprlist e al tl = OK e' -> S.satisf te e' -> list_forall2 (wt_expr te) al tl.
@@ -343,7 +343,7 @@ Proof.
 - destruct (type_unop u) as [targ1 tres]; monadInv T; eauto with ty.
 - destruct (type_binop b) as [[targ1 targ2] tres]; monadInv T; eauto with ty.
 Qed.
-Hint Resolve type_assign_incr: ty.
+Global Hint Resolve type_assign_incr: ty.
 
 Lemma type_assign_sound: forall te id a e e',
     type_assign e id a = OK e' -> S.satisf te e' -> wt_expr te a (te id).
@@ -363,7 +363,7 @@ Lemma opt_set_incr: forall te optid optty e e',
 Proof.
   unfold opt_set; intros. destruct optid, optty; try (monadInv H); eauto with ty.
 Qed.
-Hint Resolve opt_set_incr: ty.
+Global Hint Resolve opt_set_incr: ty.
 
 Lemma opt_set_sound: forall te optid sg e e',
     opt_set e optid (proj_sig_res sg) = OK e' -> S.satisf te e' ->
@@ -380,7 +380,7 @@ Proof.
   induction s; simpl; intros e1 e2 T SAT; try (monadInv T); eauto with ty.
 - destruct tret, o; try (monadInv T); eauto with ty.
 Qed.
-Hint Resolve type_stmt_incr: ty.
+Global Hint Resolve type_stmt_incr: ty.
 
 Lemma type_stmt_sound: forall te tret s e e',
     type_stmt tret e s = OK e' -> S.satisf te e' -> wt_stmt te tret s.
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index 60663503..b59ee8b4 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -364,7 +364,7 @@ Proof.
 
 - (* Inop, skipped over *)
   assert (s0 = pc') by congruence. subst s0.
-  right; exists n; split. omega. split. auto.
+  right; exists n; split. lia. split. auto.
   apply match_states_intro; auto.
 
 - (* Iop *)
@@ -583,7 +583,7 @@ Opaque builtin_strength_reduction.
 
 - (* Icond, skipped over *)
   rewrite H1 in H; inv H.
-  right; exists n; split. omega. split. auto.
+  right; exists n; split. lia. split. auto.
   econstructor; eauto.
 
 - (* Ijumptable *)
diff --git a/backend/Conventions.v b/backend/Conventions.v
index 14ffb587..8910ee49 100644
--- a/backend/Conventions.v
+++ b/backend/Conventions.v
@@ -60,9 +60,9 @@ Remark fold_max_outgoing_above:
   forall l n, fold_left max_outgoing_2 l n >= n.
 Proof.
   assert (A: forall n l, max_outgoing_1 n l >= n).
-  { intros; unfold max_outgoing_1. destruct l as [_ | []]; xomega. }
+  { intros; unfold max_outgoing_1. destruct l as [_ | []]; extlia. }
   induction l; simpl; intros. 
-  - omega.
+  - lia.
   - eapply Zge_trans. eauto.
     destruct a; simpl. apply A. eapply Zge_trans; eauto.
 Qed.
@@ -80,14 +80,14 @@ Lemma loc_arguments_bounded:
 Proof.
   intros until ty.
   assert (A: forall n l, n <= max_outgoing_1 n l).
-  { intros; unfold max_outgoing_1. destruct l as [_ | []]; xomega. }
+  { intros; unfold max_outgoing_1. destruct l as [_ | []]; extlia. }
   assert (B: forall p n,
              In (S Outgoing ofs ty) (regs_of_rpair p) ->
              ofs + typesize ty <= max_outgoing_2 n p).
   { intros. destruct p; simpl in H; intuition; subst; simpl.
-  - xomega.
-  - eapply Z.le_trans. 2: apply A. xomega.
-  - xomega. }
+  - extlia.
+  - eapply Z.le_trans. 2: apply A. extlia.
+  - extlia. }
   assert (C: forall l n,
              In (S Outgoing ofs ty) (regs_of_rpairs l) ->
              ofs + typesize ty <= fold_left max_outgoing_2 l n).
@@ -168,7 +168,7 @@ Proof.
   unfold loc_argument_acceptable.
   destruct l; intros. auto. destruct sl; try contradiction. destruct H1.
   generalize (loc_arguments_bounded _ _ _ H0).
-  generalize (typesize_pos ty). omega.
+  generalize (typesize_pos ty). lia.
 Qed.
 
 
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v
index 6919fe78..b51d6cce 100644
--- a/backend/Deadcodeproof.v
+++ b/backend/Deadcodeproof.v
@@ -67,7 +67,7 @@ Lemma mextends_agree:
   forall m1 m2 P, Mem.extends m1 m2 -> magree m1 m2 P.
 Proof.
   intros. destruct H. destruct mext_inj. constructor; intros.
-- replace ofs with (ofs + 0) by omega. eapply mi_perm; eauto. auto.
+- replace ofs with (ofs + 0) by lia. eapply mi_perm; eauto. auto.
 - eauto.
 - exploit mi_memval; eauto. unfold inject_id; eauto.
   rewrite Z.add_0_r. auto.
@@ -99,15 +99,15 @@ Proof.
     induction n; intros; simpl.
     constructor.
     rewrite Nat2Z.inj_succ in H. constructor.
-    apply H. omega.
-    apply IHn. intros; apply H; omega.
+    apply H. lia.
+    apply IHn. intros; apply H; lia.
   }
 Local Transparent Mem.loadbytes.
   unfold Mem.loadbytes; intros. destruct H.
   destruct (Mem.range_perm_dec m1 b ofs (ofs + n) Cur Readable); inv H0.
   rewrite pred_dec_true. econstructor; split; eauto.
   apply GETN. intros. rewrite Z_to_nat_max in H.
-  assert (ofs <= i < ofs + n) by xomega.
+  assert (ofs <= i < ofs + n) by extlia.
   apply ma_memval0; auto.
   red; intros; eauto.
 Qed.
@@ -146,11 +146,11 @@ Proof.
                    (ZMap.get q (Mem.setN bytes2 p c2))).
   {
     induction 1; intros; simpl.
-  - apply H; auto. simpl. omega.
+  - apply H; auto. simpl. lia.
   - simpl length in H1; rewrite Nat2Z.inj_succ in H1.
     apply IHlist_forall2; auto.
     intros. rewrite ! ZMap.gsspec. destruct (ZIndexed.eq i p). auto.
-    apply H1; auto. unfold ZIndexed.t in *; omega.
+    apply H1; auto. unfold ZIndexed.t in *; lia.
   }
   intros.
   destruct (Mem.range_perm_storebytes m2 b ofs bytes2) as [m2' ST2].
@@ -211,8 +211,8 @@ Proof.
 - rewrite (Mem.storebytes_mem_contents _ _ _ _ _ H0).
   rewrite PMap.gsspec. destruct (peq b0 b).
 + subst b0. rewrite Mem.setN_outside. eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto.
-  destruct (zlt ofs0 ofs); auto. destruct (zle (ofs + Z.of_nat (length bytes1)) ofs0); try omega.
-  elim (H1 ofs0). omega. auto.
+  destruct (zlt ofs0 ofs); auto. destruct (zle (ofs + Z.of_nat (length bytes1)) ofs0); try lia.
+  elim (H1 ofs0). lia. auto.
 + eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto.
 - rewrite (Mem.nextblock_storebytes _ _ _ _ _ H0).
   eapply ma_nextblock; eauto.
@@ -358,7 +358,7 @@ Proof.
   intros. destruct ros; simpl in *. eapply add_need_all_eagree; eauto. auto.
 Qed.
 
-Hint Resolve add_need_all_eagree add_need_all_lessdef
+Global Hint Resolve add_need_all_eagree add_need_all_lessdef
              add_need_eagree add_need_vagree
              add_needs_all_eagree add_needs_all_lessdef
              add_needs_eagree add_needs_vagree
@@ -1043,7 +1043,7 @@ Ltac UseTransfer :=
   intros. eapply nlive_remove; eauto.
   unfold adst, vanalyze; rewrite AN; eapply aaddr_arg_sound_1; eauto.
   erewrite Mem.loadbytes_length in H1 by eauto.
-  rewrite Z2Nat.id in H1 by omega. auto.
+  rewrite Z2Nat.id in H1 by lia. auto.
   eauto.
   intros (tm' & A & B).
   econstructor; split.
@@ -1070,7 +1070,7 @@ Ltac UseTransfer :=
   intros (bc & A & B & C).
   intros. eapply nlive_contains; eauto.
   erewrite Mem.loadbytes_length in H0 by eauto.
-  rewrite Z2Nat.id in H0 by omega. auto.
+  rewrite Z2Nat.id in H0 by lia. auto.
 + (* annot *)
   destruct (transfer_builtin_args (kill_builtin_res res ne, nm) _x2) as (ne1, nm1) eqn:TR.
   InvSoundState.
diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index 8ca6c6ab..22bee067 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -49,13 +49,11 @@ let stats_nb_overpredict = ref 0
 let wrong_opcode = ref 0
 let wrong_return = ref 0
 let wrong_loop2 = ref 0
-let wrong_loop = ref 0
 let wrong_call = ref 0
 
 let right_opcode = ref 0
 let right_return = ref 0
 let right_loop2 = ref 0
-let right_loop = ref 0
 let right_call = ref 0
 
 let reset_stats () = begin
@@ -67,12 +65,10 @@ let reset_stats () = begin
   wrong_opcode := 0;
   wrong_return := 0;
   wrong_loop2 := 0;
-  wrong_loop := 0;
   wrong_call := 0;
   right_opcode := 0;
   right_return := 0;
   right_loop2 := 0;
-  right_loop := 0;
   right_call := 0;
 end
 
@@ -86,11 +82,11 @@ let write_stats_oc () =
   match !stats_oc with
   | None -> ()
   | Some oc -> begin
-      Printf.fprintf oc "%d %d %d %d %d %d %d %d %d %d %d %d %d %d %d\n" !stats_nb_total
+      Printf.fprintf oc "%d %d %d %d %d %d %d %d %d %d %d %d %d\n" !stats_nb_total
         !stats_nb_correct_predicts !stats_nb_mispredicts !stats_nb_missed_opportunities
         !stats_nb_overpredict
-        !wrong_opcode !wrong_return !wrong_loop2 !wrong_loop !wrong_call
-        !right_opcode !right_return !right_loop2 !right_loop !right_call
+        !wrong_opcode !wrong_return !wrong_loop2 !wrong_call
+        !right_opcode !right_return !right_loop2 !right_call
         ;
       close_out oc
     end
@@ -417,7 +413,7 @@ let get_directions f code entrypoint = begin
           if stats_oc_recording () || not @@ has_some pred then
             (* debug "Analyzing %d.." (P.to_int n); *)
             let heuristics = [ do_opcode_heuristic;
-              do_return_heuristic; do_loop2_heuristic loop_info n; do_loop_heuristic; do_call_heuristic;
+              do_return_heuristic; do_loop2_heuristic loop_info n; (* do_loop_heuristic; *) do_call_heuristic;
                (* do_store_heuristic *) ] in
             let preferred = ref None in
             let current_heuristic = ref 0 in
@@ -438,8 +434,7 @@ let get_directions f code entrypoint = begin
                           | 0 -> incr wrong_opcode
                           | 1 -> incr wrong_return
                           | 2 -> incr wrong_loop2
-                          | 3 -> incr wrong_loop
-                          | 4 -> incr wrong_call
+                          | 3 -> incr wrong_call
                           | _ -> failwith "Shouldn't happen"
                           end
                       | Some false, Some false
@@ -448,8 +443,7 @@ let get_directions f code entrypoint = begin
                           | 0 -> incr right_opcode
                           | 1 -> incr right_return
                           | 2 -> incr right_loop2
-                          | 3 -> incr right_loop
-                          | 4 -> incr right_call
+                          | 3 -> incr right_call
                           | _ -> failwith "Shouldn't happen"
                           end
                       | _ -> ()
@@ -1050,9 +1044,13 @@ let extract_upto_icond f code head =
 let rotate_inner_loop f code revmap iloop =
   let header = extract_upto_icond f code iloop.head in
   let limit = !Clflags.option_flooprotate in
-  if count_ignore_nops code header > limit then begin
+  let nb_duplicated = count_ignore_nops code header in
+  if nb_duplicated > limit then begin
     debug "Loop Rotate: too many nodes to duplicate (%d > %d)" (List.length header) limit;
     (code, revmap)
+  end else if nb_duplicated == count_ignore_nops code iloop.body then begin
+    debug "The conditional branch is already at the end! No need to rotate.";
+    (code, revmap)
   end else
     let (code2, revmap2, dupheader, fwmap) = clone code revmap header in
     let code' = ref code2 in
diff --git a/backend/Injectproof.v b/backend/Injectproof.v
index 9e5ad6df..dd5e72f8 100644
--- a/backend/Injectproof.v
+++ b/backend/Injectproof.v
@@ -89,7 +89,7 @@ Qed.
 Obligation 2.
 Proof.
   simpl in BOUND.
-  omega.
+  lia.
 Qed.
 
 Program Definition bounded_nth_S_statement : Prop :=
@@ -104,14 +104,14 @@ Lemma bounded_nth_proof_irr :
          (BOUND1 BOUND2 : (k < List.length l)%nat),
     (bounded_nth k l BOUND1) = (bounded_nth k l BOUND2).
 Proof.
-  induction k; destruct l; simpl; intros; trivial; omega.
+  induction k; destruct l; simpl; intros; trivial; lia.
 Qed.
 
 Lemma bounded_nth_S : bounded_nth_S_statement.
 Proof.
   unfold bounded_nth_S_statement.
   induction k; destruct l; simpl; intros; trivial.
-  1, 2: omega.
+  1, 2: lia.
   apply bounded_nth_proof_irr.
 Qed.
 
@@ -121,7 +121,7 @@ Lemma inject_list_injected:
     Some (inject_instr (bounded_nth k l BOUND) (Pos.succ (pos_add_nat pc k))).
 Proof.
   induction l; simpl; intros.
-  - omega.
+  - lia.
   - simpl.
     destruct k as [ | k]; simpl pos_add_nat.
     + simpl bounded_nth.
diff --git a/backend/Inlining.v b/backend/Inlining.v
index 8c7e1898..0e18d38e 100644
--- a/backend/Inlining.v
+++ b/backend/Inlining.v
@@ -71,12 +71,12 @@ Inductive sincr (s1 s2: state) : Prop :=
 
 Remark sincr_refl: forall s, sincr s s.
 Proof.
-  intros; constructor; xomega.
+  intros; constructor; extlia.
 Qed.
 
 Lemma sincr_trans: forall s1 s2 s3, sincr s1 s2 -> sincr s2 s3 -> sincr s1 s3.
 Proof.
-  intros. inv H; inv H0. constructor; xomega.
+  intros. inv H; inv H0. constructor; extlia.
 Qed.
 
 (** Dependently-typed state monad, ensuring that the final state is
@@ -111,7 +111,7 @@ Program Definition set_instr (pc: node) (i: instruction): mon unit :=
       (mkstate s.(st_nextreg) s.(st_nextnode) (PTree.set pc i s.(st_code)) s.(st_stksize))
       _.
 Next Obligation.
-  intros; constructor; simpl; xomega.
+  intros; constructor; simpl; extlia.
 Qed.
 
 Program Definition add_instr (i: instruction): mon node :=
@@ -121,7 +121,7 @@ Program Definition add_instr (i: instruction): mon node :=
       (mkstate s.(st_nextreg) (Pos.succ pc) (PTree.set pc i s.(st_code)) s.(st_stksize))
       _.
 Next Obligation.
-  intros; constructor; simpl; xomega.
+  intros; constructor; simpl; extlia.
 Qed.
 
 Program Definition reserve_nodes (numnodes: positive): mon positive :=
@@ -130,7 +130,7 @@ Program Definition reserve_nodes (numnodes: positive): mon positive :=
       (mkstate s.(st_nextreg) (Pos.add s.(st_nextnode) numnodes) s.(st_code) s.(st_stksize))
       _.
 Next Obligation.
-  intros; constructor; simpl; xomega.
+  intros; constructor; simpl; extlia.
 Qed.
 
 Program Definition reserve_regs (numregs: positive): mon positive :=
@@ -139,7 +139,7 @@ Program Definition reserve_regs (numregs: positive): mon positive :=
       (mkstate (Pos.add s.(st_nextreg) numregs) s.(st_nextnode) s.(st_code) s.(st_stksize))
       _.
 Next Obligation.
-  intros; constructor; simpl; xomega.
+  intros; constructor; simpl; extlia.
 Qed.
 
 Program Definition request_stack (sz: Z): mon unit :=
@@ -148,7 +148,7 @@ Program Definition request_stack (sz: Z): mon unit :=
       (mkstate s.(st_nextreg) s.(st_nextnode) s.(st_code) (Z.max s.(st_stksize) sz))
       _.
 Next Obligation.
-  intros; constructor; simpl; xomega.
+  intros; constructor; simpl; extlia.
 Qed.
 
 Program Definition ptree_mfold {A: Type} (f: positive -> A -> mon unit) (t: PTree.t A): mon unit :=
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index c4efaf18..eb30732b 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -67,21 +67,21 @@ Qed.
 Remark sreg_below_diff:
   forall ctx r r', Plt r' ctx.(dreg) -> sreg ctx r <> r'.
 Proof.
-  intros. zify. unfold sreg; rewrite shiftpos_eq. xomega.
+  intros. zify. unfold sreg; rewrite shiftpos_eq. extlia.
 Qed.
 
 Remark context_below_diff:
   forall ctx1 ctx2 r1 r2,
   context_below ctx1 ctx2 -> Ple r1 ctx1.(mreg) -> sreg ctx1 r1 <> sreg ctx2 r2.
 Proof.
-  intros. red in H. zify. unfold sreg; rewrite ! shiftpos_eq. xomega.
+  intros. red in H. zify. unfold sreg; rewrite ! shiftpos_eq. extlia.
 Qed.
 
 Remark context_below_lt:
   forall ctx1 ctx2 r, context_below ctx1 ctx2 -> Ple r ctx1.(mreg) -> Plt (sreg ctx1 r) ctx2.(dreg).
 Proof.
   intros. red in H. unfold Plt; zify. unfold sreg; rewrite shiftpos_eq.
-  xomega.
+  extlia.
 Qed.
 
 (*
@@ -89,7 +89,7 @@ Remark context_below_le:
   forall ctx1 ctx2 r, context_below ctx1 ctx2 -> Ple r ctx1.(mreg) -> Ple (sreg ctx1 r) ctx2.(dreg).
 Proof.
   intros. red in H. unfold Ple; zify. unfold sreg; rewrite shiftpos_eq.
-  xomega.
+  extlia.
 Qed.
 *)
 
@@ -105,7 +105,7 @@ Definition val_reg_charact (F: meminj) (ctx: context) (rs': regset) (v: val) (r:
 Remark Plt_Ple_dec:
   forall p q, {Plt p q} + {Ple q p}.
 Proof.
-  intros. destruct (plt p q). left; auto. right; xomega.
+  intros. destruct (plt p q). left; auto. right; extlia.
 Qed.
 
 Lemma agree_val_reg_gen:
@@ -149,7 +149,7 @@ Proof.
   repeat rewrite Regmap.gsspec.
   destruct (peq r0 r). subst r0. rewrite peq_true. auto.
   rewrite peq_false. auto. apply shiftpos_diff; auto.
-  rewrite Regmap.gso. auto. xomega.
+  rewrite Regmap.gso. auto. extlia.
 Qed.
 
 Lemma agree_set_reg_undef:
@@ -184,7 +184,7 @@ Proof.
   unfold agree_regs; intros. destruct H. split; intros.
   rewrite H0. auto.
   apply shiftpos_above.
-  eapply Pos.lt_le_trans. apply shiftpos_below. xomega.
+  eapply Pos.lt_le_trans. apply shiftpos_below. extlia.
   apply H1; auto.
 Qed.
 
@@ -272,7 +272,7 @@ Lemma range_private_invariant:
   range_private F1 m1 m1' sp lo hi.
 Proof.
   intros; red; intros. exploit H; eauto. intros [A B]. split; auto.
-  intros; red; intros. exploit H0; eauto. omega. intros [P Q].
+  intros; red; intros. exploit H0; eauto. lia. intros [P Q].
   eelim B; eauto.
 Qed.
 
@@ -293,12 +293,12 @@ Lemma range_private_alloc_left:
   range_private F1 m1 m' sp' (base + Z.max sz 0) hi.
 Proof.
   intros; red; intros.
-  exploit (H ofs). generalize (Z.le_max_r sz 0). omega. intros [A B].
+  exploit (H ofs). generalize (Z.le_max_r sz 0). lia. intros [A B].
   split; auto. intros; red; intros.
   exploit Mem.perm_alloc_inv; eauto.
   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 Zmax_spec in H3. destruct (zlt 0 sz); lia.
   rewrite H2 in H4; auto. eelim B; eauto.
 Qed.
 
@@ -313,21 +313,21 @@ Proof.
   intros; red; intros.
   destruct (zlt ofs (base + Z.max sz 0)) as [z|z].
   red; split.
-  replace ofs with ((ofs - base) + base) by omega.
+  replace ofs with ((ofs - base) + base) by lia.
   eapply Mem.perm_inject; eauto.
   eapply Mem.free_range_perm; eauto.
-  rewrite Zmax_spec in z. destruct (zlt 0 sz); omega.
+  rewrite Zmax_spec in z. destruct (zlt 0 sz); lia.
   intros; red; intros. destruct (eq_block b b0).
   subst b0. rewrite H1 in H4; inv H4.
-  eelim Mem.perm_free_2; eauto. rewrite Zmax_spec in z. destruct (zlt 0 sz); omega.
+  eelim Mem.perm_free_2; eauto. rewrite Zmax_spec in z. destruct (zlt 0 sz); lia.
   exploit Mem.mi_no_overlap; eauto.
   apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
   eapply Mem.free_range_perm. eauto.
-  instantiate (1 := ofs - base). rewrite Zmax_spec in z. destruct (zlt 0 sz); omega.
+  instantiate (1 := ofs - base). rewrite Zmax_spec in z. destruct (zlt 0 sz); lia.
   eapply Mem.perm_free_3; eauto.
-  intros [A | A]. congruence. omega.
+  intros [A | A]. congruence. lia.
 
-  exploit (H ofs). omega. intros [A B]. split. auto.
+  exploit (H ofs). lia. intros [A B]. split. auto.
   intros; red; intros. eelim B; eauto. eapply Mem.perm_free_3; eauto.
 Qed.
 
@@ -607,39 +607,39 @@ Proof.
   (* cons *)
   apply match_stacks_cons with (fenv := fenv) (ctx := ctx); auto.
   eapply match_stacks_inside_invariant; eauto.
-  intros; eapply INJ; eauto; xomega.
-  intros; eapply PERM1; eauto; xomega.
-  intros; eapply PERM2; eauto; xomega.
-  intros; eapply PERM3; eauto; xomega.
+  intros; eapply INJ; eauto; extlia.
+  intros; eapply PERM1; eauto; extlia.
+  intros; eapply PERM2; eauto; extlia.
+  intros; eapply PERM3; eauto; extlia.
   eapply agree_regs_incr; eauto.
   eapply range_private_invariant; eauto.
   (* untailcall *)
   apply match_stacks_untailcall with (ctx := ctx); auto.
   eapply match_stacks_inside_invariant; eauto.
-  intros; eapply INJ; eauto; xomega.
-  intros; eapply PERM1; eauto; xomega.
-  intros; eapply PERM2; eauto; xomega.
-  intros; eapply PERM3; eauto; xomega.
+  intros; eapply INJ; eauto; extlia.
+  intros; eapply PERM1; eauto; extlia.
+  intros; eapply PERM2; eauto; extlia.
+  intros; eapply PERM3; eauto; extlia.
   eapply range_private_invariant; eauto.
 
   induction 1; intros.
   (* base *)
   eapply match_stacks_inside_base; eauto.
   eapply match_stacks_invariant; eauto.
-  intros; eapply INJ; eauto; xomega.
-  intros; eapply PERM1; eauto; xomega.
-  intros; eapply PERM2; eauto; xomega.
-  intros; eapply PERM3; eauto; xomega.
+  intros; eapply INJ; eauto; extlia.
+  intros; eapply PERM1; eauto; extlia.
+  intros; eapply PERM2; eauto; extlia.
+  intros; eapply PERM3; eauto; extlia.
   (* inlined *)
   apply match_stacks_inside_inlined with (fenv := fenv) (ctx' := ctx'); auto.
   apply IHmatch_stacks_inside; auto.
-  intros. apply RS. red in BELOW. xomega.
+  intros. apply RS. red in BELOW. extlia.
   apply agree_regs_incr with F; auto.
   apply agree_regs_invariant with rs'; auto.
-  intros. apply RS. red in BELOW. xomega.
+  intros. apply RS. red in BELOW. extlia.
   eapply range_private_invariant; eauto.
-    intros. split. eapply INJ; eauto. xomega. eapply PERM1; eauto. xomega.
-    intros. eapply PERM2; eauto. xomega.
+    intros. split. eapply INJ; eauto. extlia. eapply PERM1; eauto. extlia.
+    intros. eapply PERM2; eauto. extlia.
 Qed.
 
 Lemma match_stacks_empty:
@@ -668,7 +668,7 @@ Lemma match_stacks_inside_set_reg:
   match_stacks_inside F m m' stk stk' f' ctx sp' (rs'#(sreg ctx r) <- v).
 Proof.
   intros. eapply match_stacks_inside_invariant; eauto.
-  intros. apply Regmap.gso. zify. unfold sreg; rewrite shiftpos_eq. xomega.
+  intros. apply Regmap.gso. zify. unfold sreg; rewrite shiftpos_eq. extlia.
 Qed.
 
 Lemma match_stacks_inside_set_res:
@@ -717,11 +717,11 @@ Proof.
   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 IHmatch_stacks_inside; eauto. destruct SBELOW. lia.
   eapply agree_regs_incr; eauto.
   eapply range_private_invariant; eauto.
   intros. exploit Mem.perm_alloc_inv; eauto. destruct (eq_block b0 b); intros.
-  subst b0. rewrite H2 in H5; inv H5. elimtype False; xomega.
+  subst b0. rewrite H2 in H5; inv H5. elimtype False; extlia.
   rewrite H3 in H5; auto.
 Qed.
 
@@ -753,25 +753,25 @@ Lemma min_alignment_sound:
 Proof.
   intros; red; intros. unfold min_alignment in H.
   assert (2 <= sz -> (2 | n)). intros.
-    destruct (zle sz 1). omegaContradiction.
+    destruct (zle sz 1). extlia.
     destruct (zle sz 2). auto.
     destruct (zle sz 4). apply Z.divide_trans with 4; auto. exists 2; auto.
     apply Z.divide_trans with 8; auto. exists 4; auto.
   assert (4 <= sz -> (4 | n)). intros.
-    destruct (zle sz 1). omegaContradiction.
-    destruct (zle sz 2). omegaContradiction.
+    destruct (zle sz 1). extlia.
+    destruct (zle sz 2). extlia.
     destruct (zle sz 4). auto.
     apply Z.divide_trans with 8; auto. exists 2; auto.
   assert (8 <= sz -> (8 | n)). intros.
-    destruct (zle sz 1). omegaContradiction.
-    destruct (zle sz 2). omegaContradiction.
-    destruct (zle sz 4). omegaContradiction.
+    destruct (zle sz 1). extlia.
+    destruct (zle sz 2). extlia.
+    destruct (zle sz 4). extlia.
     auto.
   destruct chunk; simpl in *; auto.
   apply Z.divide_1_l.
   apply Z.divide_1_l.
-  apply H2; omega.
-  apply H2; omega.
+  apply H2; lia.
+  apply H2; lia.
 Qed.
 
 (** Preservation by external calls *)
@@ -803,19 +803,19 @@ Proof.
     inv MG. constructor; intros; eauto.
     destruct (F1 b1) as [[b2' delta']|] eqn:?.
     exploit INCR; eauto. intros EQ; rewrite H0 in EQ; inv EQ. eapply IMAGE; eauto.
-    exploit SEP; eauto. intros [A B]. elim B. red. xomega.
+    exploit SEP; eauto. intros [A B]. elim B. red. extlia.
   eapply match_stacks_cons; eauto.
-    eapply match_stacks_inside_extcall; eauto. xomega.
+    eapply match_stacks_inside_extcall; eauto. extlia.
     eapply agree_regs_incr; eauto.
-    eapply range_private_extcall; eauto. red; xomega.
-    intros. apply SSZ2; auto. apply MAXPERM'; auto. red; xomega.
+    eapply range_private_extcall; eauto. red; extlia.
+    intros. apply SSZ2; auto. apply MAXPERM'; auto. red; extlia.
   eapply match_stacks_untailcall; eauto.
-    eapply match_stacks_inside_extcall; eauto. xomega.
-    eapply range_private_extcall; eauto. red; xomega.
-    intros. apply SSZ2; auto. apply MAXPERM'; auto. red; xomega.
+    eapply match_stacks_inside_extcall; eauto. extlia.
+    eapply range_private_extcall; eauto. red; extlia.
+    intros. apply SSZ2; auto. apply MAXPERM'; auto. red; extlia.
   induction 1; intros.
   eapply match_stacks_inside_base; eauto.
-    eapply match_stacks_extcall; eauto. xomega.
+    eapply match_stacks_extcall; eauto. extlia.
   eapply match_stacks_inside_inlined; eauto.
     eapply agree_regs_incr; eauto.
     eapply range_private_extcall; eauto.
@@ -829,7 +829,7 @@ Lemma align_unchanged:
   forall n amount, amount > 0 -> (amount | n) -> align n amount = n.
 Proof.
   intros. destruct H0 as [p EQ]. subst n. unfold align. decEq.
-  apply Zdiv_unique with (b := amount - 1). omega. omega.
+  apply Zdiv_unique with (b := amount - 1). lia. lia.
 Qed.
 
 Lemma match_stacks_inside_inlined_tailcall:
@@ -849,10 +849,10 @@ Proof.
   (* inlined *)
   assert (dstk ctx <= dstk ctx'). rewrite H1. apply align_le. apply min_alignment_pos.
   eapply match_stacks_inside_inlined; eauto.
-  red; intros. destruct (zlt ofs (dstk ctx)). apply PAD; omega. apply H3. inv H4. xomega.
+  red; intros. destruct (zlt ofs (dstk ctx)). apply PAD; lia. apply H3. inv H4. extlia.
   congruence.
-  unfold context_below in *. xomega.
-  unfold context_stack_call in *. omega.
+  unfold context_below in *. extlia.
+  unfold context_stack_call in *. lia.
 Qed.
 
 (** ** Relating states *)
@@ -1068,12 +1068,12 @@ Proof.
 + (* inlined *)
   assert (EQ: fd = Internal f0) by (eapply find_inlined_function; eauto).
   subst fd.
-  right; split. simpl; omega. split. auto.
+  right; split. simpl; lia. split. auto.
   econstructor; eauto.
   eapply match_stacks_inside_inlined; eauto.
-  red; intros. apply PRIV. inv H13. destruct H16. xomega.
+  red; intros. apply PRIV. inv H13. destruct H16. extlia.
   apply agree_val_regs_gen; auto.
-  red; intros; apply PRIV. destruct H16. omega.
+  red; intros; apply PRIV. destruct H16. lia.
 
 - (* tailcall *)
   exploit match_stacks_inside_globalenvs; eauto. intros [bound G].
@@ -1086,9 +1086,9 @@ Proof.
   assert (X: { m1' | Mem.free m'0 sp' 0 (fn_stacksize f') = Some m1'}).
     apply Mem.range_perm_free. red; intros.
     destruct (zlt ofs f.(fn_stacksize)).
-    replace ofs with (ofs + dstk ctx) by omega. eapply Mem.perm_inject; eauto.
-    eapply Mem.free_range_perm; eauto. omega.
-    inv FB. eapply range_private_perms; eauto. xomega.
+    replace ofs with (ofs + dstk ctx) by lia. eapply Mem.perm_inject; eauto.
+    eapply Mem.free_range_perm; eauto. lia.
+    inv FB. eapply range_private_perms; eauto. extlia.
   destruct X as [m1' FREE].
   left; econstructor; split.
   eapply plus_one. eapply exec_Itailcall; eauto.
@@ -1099,12 +1099,12 @@ Proof.
     intros. eapply Mem.perm_free_3; eauto.
     intros. eapply Mem.perm_free_1; eauto with ordered_type.
     intros. eapply Mem.perm_free_3; eauto.
-  erewrite Mem.nextblock_free; eauto. red in VB; xomega.
+  erewrite Mem.nextblock_free; eauto. red in VB; extlia.
   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 *)
-  intros. rewrite DSTK in PRIV'. exploit (PRIV' (ofs + delta)). omega. intros [P Q].
-  eelim Q; eauto. replace (ofs + delta - delta) with ofs by omega.
+  intros. rewrite DSTK in PRIV'. exploit (PRIV' (ofs + delta)). lia. intros [P Q].
+  eelim Q; eauto. replace (ofs + delta - delta) with ofs by lia.
   apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem.
 + (* turned into a call *)
   left; econstructor; split.
@@ -1119,7 +1119,7 @@ Proof.
 + (* inlined *)
   assert (EQ: fd = Internal f0) by (eapply find_inlined_function; eauto).
   subst fd.
-  right; split. simpl; omega. split. auto.
+  right; split. simpl; lia. split. auto.
   econstructor; eauto.
   eapply match_stacks_inside_inlined_tailcall; eauto.
   eapply match_stacks_inside_invariant; eauto.
@@ -1128,7 +1128,7 @@ Proof.
   eapply Mem.free_left_inject; eauto.
   red; intros; apply PRIV'.
     assert (dstk ctx <= dstk ctx'). red in H14; rewrite H14. apply align_le. apply min_alignment_pos.
-    omega.
+    lia.
 
 - (* builtin *)
   exploit tr_funbody_inv; eauto. intros TR; inv TR.
@@ -1178,10 +1178,10 @@ Proof.
   assert (X: { m1' | Mem.free m'0 sp' 0 (fn_stacksize f') = Some m1'}).
     apply Mem.range_perm_free. red; intros.
     destruct (zlt ofs f.(fn_stacksize)).
-    replace ofs with (ofs + dstk ctx) by omega. eapply Mem.perm_inject; eauto.
-    eapply Mem.free_range_perm; eauto. omega.
+    replace ofs with (ofs + dstk ctx) by lia. eapply Mem.perm_inject; eauto.
+    eapply Mem.free_range_perm; eauto. lia.
     inv FB. eapply range_private_perms; eauto.
-    generalize (Zmax_spec (fn_stacksize f) 0). destruct (zlt 0 (fn_stacksize f)); omega.
+    generalize (Zmax_spec (fn_stacksize f) 0). destruct (zlt 0 (fn_stacksize f)); lia.
   destruct X as [m1' FREE].
   left; econstructor; split.
   eapply plus_one. eapply exec_Ireturn; eauto.
@@ -1191,19 +1191,19 @@ Proof.
     intros. eapply Mem.perm_free_3; eauto.
     intros. eapply Mem.perm_free_1; eauto with ordered_type.
     intros. eapply Mem.perm_free_3; eauto.
-  erewrite Mem.nextblock_free; eauto. red in VB; xomega.
+  erewrite Mem.nextblock_free; eauto. red in VB; extlia.
   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 *)
   intros. inversion FB; subst.
   assert (PRIV': range_private F m' m'0 sp' (dstk ctx) f'.(fn_stacksize)).
     rewrite H8 in PRIV. eapply range_private_free_left; eauto.
-  rewrite DSTK in PRIV'. exploit (PRIV' (ofs + delta)). omega. intros [A B].
-  eelim B; eauto. replace (ofs + delta - delta) with ofs by omega.
+  rewrite DSTK in PRIV'. exploit (PRIV' (ofs + delta)). lia. intros [A B].
+  eelim B; eauto. replace (ofs + delta - delta) with ofs by lia.
   apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem.
 
 + (* inlined *)
-  right. split. simpl. omega. split. auto.
+  right. split. simpl. lia. split. auto.
   econstructor; eauto.
   eapply match_stacks_inside_invariant; eauto.
     intros. eapply Mem.perm_free_3; eauto.
@@ -1219,7 +1219,7 @@ Proof.
   { eapply tr_function_linkorder; eauto. }
   inversion TR; subst.
   exploit Mem.alloc_parallel_inject. eauto. eauto. apply Z.le_refl.
-    instantiate (1 := fn_stacksize f'). inv H1. xomega.
+    instantiate (1 := fn_stacksize f'). inv H1. extlia.
   intros [F' [m1' [sp' [A [B [C [D E]]]]]]].
   left; econstructor; split.
   eapply plus_one. eapply exec_function_internal; eauto.
@@ -1241,13 +1241,13 @@ Proof.
   rewrite H5. apply agree_regs_init_regs. eauto. auto. inv H1; auto. congruence. auto.
   eapply Mem.valid_new_block; eauto.
   red; intros. split.
-  eapply Mem.perm_alloc_2; eauto. inv H1; xomega.
+  eapply Mem.perm_alloc_2; eauto. inv H1; extlia.
   intros; red; intros. exploit Mem.perm_alloc_inv. eexact H. eauto.
   destruct (eq_block b stk); intros.
-  subst. rewrite D in H9; inv H9. inv H1; xomega.
+  subst. rewrite D in H9; inv H9. inv H1; extlia.
   rewrite E in H9; auto. eelim Mem.fresh_block_alloc. eexact A. eapply Mem.mi_mappedblocks; eauto.
   auto.
-  intros. exploit Mem.perm_alloc_inv; eauto. rewrite dec_eq_true. omega.
+  intros. exploit Mem.perm_alloc_inv; eauto. rewrite dec_eq_true. lia.
 
 - (* internal function, inlined *)
   inversion FB; subst.
@@ -1257,19 +1257,19 @@ Proof.
     (* sp' is valid *)
     instantiate (1 := sp'). auto.
     (* offset is representable *)
-    instantiate (1 := dstk ctx). generalize (Z.le_max_r (fn_stacksize f) 0). omega.
+    instantiate (1 := dstk ctx). generalize (Z.le_max_r (fn_stacksize f) 0). lia.
     (* size of target block is representable *)
-    intros. right. exploit SSZ2; eauto with mem. inv FB; omega.
+    intros. right. exploit SSZ2; eauto with mem. inv FB; lia.
     (* we have full permissions on sp' at and above dstk ctx *)
     intros. apply Mem.perm_cur. apply Mem.perm_implies with Freeable; auto with mem.
-    eapply range_private_perms; eauto. xomega.
+    eapply range_private_perms; eauto. extlia.
     (* offset is aligned *)
-    replace (fn_stacksize f - 0) with (fn_stacksize f) by omega.
+    replace (fn_stacksize f - 0) with (fn_stacksize f) by lia.
     inv FB. apply min_alignment_sound; auto.
     (* nobody maps to (sp, dstk ctx...) *)
-    intros. exploit (PRIV (ofs + delta')); eauto. xomega.
+    intros. exploit (PRIV (ofs + delta')); eauto. extlia.
     intros [A B]. eelim B; eauto.
-    replace (ofs + delta' - delta') with ofs by omega.
+    replace (ofs + delta' - delta') with ofs by lia.
     apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem.
   intros [F' [A [B [C D]]]].
   exploit tr_moves_init_regs; eauto. intros [rs'' [P [Q R]]].
@@ -1278,7 +1278,7 @@ Proof.
   econstructor.
   eapply match_stacks_inside_alloc_left; eauto.
   eapply match_stacks_inside_invariant; eauto.
-  omega.
+  lia.
   eauto. auto.
   apply agree_regs_incr with F; auto.
   auto. auto. auto.
@@ -1299,7 +1299,7 @@ Proof.
     eapply match_stacks_extcall with (F1 := F) (F2 := F1) (m1 := m) (m1' := m'0); eauto.
     intros; eapply external_call_max_perm; eauto.
     intros; eapply external_call_max_perm; eauto.
-    xomega.
+    extlia.
     eapply external_call_nextblock; eauto.
     auto. auto.
 
@@ -1321,14 +1321,14 @@ Proof.
   eauto. auto.
   apply agree_set_reg; auto.
   auto. auto. auto.
-  red; intros. destruct (zlt ofs (dstk ctx)). apply PAD; omega. apply PRIV; omega.
+  red; intros. destruct (zlt ofs (dstk ctx)). apply PAD; lia. apply PRIV; lia.
   auto. auto.
 
 - (* return from inlined function *)
   inv MS0; try congruence. rewrite RET0 in RET; inv RET.
   unfold inline_return in AT.
   assert (PRIV': range_private F m m' sp' (dstk ctx' + mstk ctx') f'.(fn_stacksize)).
-    red; intros. destruct (zlt ofs (dstk ctx)). apply PAD. omega. apply PRIV. omega.
+    red; intros. destruct (zlt ofs (dstk ctx)). apply PAD. lia. apply PRIV. lia.
   destruct or.
 + (* with a result *)
   left; econstructor; split.
diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v
index eba026ec..e846e0fd 100644
--- a/backend/Inliningspec.v
+++ b/backend/Inliningspec.v
@@ -73,7 +73,7 @@ Qed.
 Lemma shiftpos_eq: forall x y, Zpos (shiftpos x y) = (Zpos x + Zpos y) - 1.
 Proof.
   intros. unfold shiftpos. zify.  try rewrite Pos2Z.inj_sub. auto.
-  zify. omega.
+  zify. lia.
 Qed.
 
 Lemma shiftpos_inj:
@@ -82,7 +82,7 @@ Proof.
   intros.
   assert (Zpos (shiftpos x n) = Zpos (shiftpos y n)) by congruence.
   rewrite ! shiftpos_eq in H0.
-  assert (Z.pos x = Z.pos y) by omega.
+  assert (Z.pos x = Z.pos y) by lia.
   congruence.
 Qed.
 
@@ -95,25 +95,25 @@ Qed.
 Lemma shiftpos_above:
   forall x n, Ple n (shiftpos x n).
 Proof.
-  intros. unfold Ple; zify. rewrite shiftpos_eq. xomega.
+  intros. unfold Ple; zify. rewrite shiftpos_eq. extlia.
 Qed.
 
 Lemma shiftpos_not_below:
   forall x n, Plt (shiftpos x n) n -> False.
 Proof.
-  intros. generalize (shiftpos_above x n). xomega.
+  intros. generalize (shiftpos_above x n). extlia.
 Qed.
 
 Lemma shiftpos_below:
   forall x n, Plt (shiftpos x n) (Pos.add x n).
 Proof.
-  intros. unfold Plt; zify. rewrite shiftpos_eq. omega.
+  intros. unfold Plt; zify. rewrite shiftpos_eq. lia.
 Qed.
 
 Lemma shiftpos_le:
   forall x y n, Ple x y -> Ple (shiftpos x n) (shiftpos y n).
 Proof.
-  intros. unfold Ple in *; zify. rewrite ! shiftpos_eq. omega.
+  intros. unfold Ple in *; zify. rewrite ! shiftpos_eq. lia.
 Qed.
 
 
@@ -219,9 +219,9 @@ Proof.
   induction srcs; simpl; intros.
   monadInv H. auto.
   destruct dsts; monadInv H. auto.
-  transitivity (st_code s0)!pc. eapply IHsrcs; eauto. monadInv EQ; simpl. xomega.
+  transitivity (st_code s0)!pc. eapply IHsrcs; eauto. monadInv EQ; simpl. extlia.
   monadInv EQ; simpl. apply PTree.gso.
-  inversion INCR0; simpl in *. xomega.
+  inversion INCR0; simpl in *. extlia.
 Qed.
 
 Lemma add_moves_spec:
@@ -234,13 +234,13 @@ Proof.
   monadInv H. apply tr_moves_nil; auto.
   destruct dsts; monadInv H. apply tr_moves_nil; auto.
   apply tr_moves_cons with x. eapply IHsrcs; eauto.
-  intros. inversion INCR. apply H0; xomega.
+  intros. inversion INCR. apply H0; extlia.
   monadInv EQ.
   rewrite H0. erewrite add_moves_unchanged; eauto.
   simpl. apply PTree.gss.
-  simpl. xomega.
-  xomega.
-  inversion INCR; inversion INCR0; simpl in *; xomega.
+  simpl. extlia.
+  extlia.
+  inversion INCR; inversion INCR0; simpl in *; extlia.
 Qed.
 
 (** ** Relational specification of CFG expansion *)
@@ -386,9 +386,9 @@ Proof.
   monadInv H. unfold inline_function in EQ. monadInv EQ.
   transitivity (s2.(st_code)!pc'). eauto.
   transitivity (s5.(st_code)!pc'). eapply add_moves_unchanged; eauto.
-    left. inversion INCR5. inversion INCR3. monadInv EQ1; simpl in *. xomega.
+    left. inversion INCR5. inversion INCR3. monadInv EQ1; simpl in *. extlia.
   transitivity (s4.(st_code)!pc'). eapply rec_unchanged; eauto.
-    simpl. monadInv EQ; simpl. monadInv EQ1; simpl. xomega.
+    simpl. monadInv EQ; simpl. monadInv EQ1; simpl. extlia.
     simpl. monadInv EQ1; simpl. auto.
   monadInv EQ; simpl. monadInv EQ1; simpl. auto.
 (* tailcall *)
@@ -397,9 +397,9 @@ Proof.
   monadInv H. unfold inline_tail_function in EQ. monadInv EQ.
   transitivity (s2.(st_code)!pc'). eauto.
   transitivity (s5.(st_code)!pc'). eapply add_moves_unchanged; eauto.
-    left. inversion INCR5. inversion INCR3. monadInv EQ1; simpl in *. xomega.
+    left. inversion INCR5. inversion INCR3. monadInv EQ1; simpl in *. extlia.
   transitivity (s4.(st_code)!pc'). eapply rec_unchanged; eauto.
-    simpl. monadInv EQ; simpl. monadInv EQ1; simpl. xomega.
+    simpl. monadInv EQ; simpl. monadInv EQ1; simpl. extlia.
     simpl. monadInv EQ1; simpl. auto.
   monadInv EQ; simpl. monadInv EQ1; simpl. auto.
 (* return *)
@@ -422,7 +422,7 @@ Proof.
   destruct a as [pc1 instr1]; simpl in *.
   monadInv H. inv H3.
   transitivity ((st_code s0)!pc).
-  eapply IHl; eauto. destruct INCR; xomega. destruct INCR; xomega.
+  eapply IHl; eauto. destruct INCR; extlia. destruct INCR; extlia.
   eapply expand_instr_unchanged; eauto.
 Qed.
 
@@ -438,7 +438,7 @@ Proof.
   exploit ptree_mfold_spec; eauto. intros [INCR' ITER].
   eapply iter_expand_instr_unchanged; eauto.
     subst s0; auto.
-    subst s0; simpl. xomega.
+    subst s0; simpl. extlia.
     red; intros. exploit list_in_map_inv; eauto. intros [pc1 [A B]].
     subst pc. unfold spc in H1. eapply shiftpos_not_below; eauto.
     apply PTree.elements_keys_norepet.
@@ -464,7 +464,7 @@ Remark min_alignment_pos:
   forall sz, min_alignment sz > 0.
 Proof.
   intros; unfold min_alignment.
-  destruct (zle sz 1). omega. destruct (zle sz 2). omega. destruct (zle sz 4); omega.
+  destruct (zle sz 1). lia. destruct (zle sz 2). lia. destruct (zle sz 4); lia.
 Qed.
 
 Ltac inv_incr :=
@@ -501,20 +501,20 @@ Proof.
   apply tr_call_inlined with (pc1 := x0) (ctx' := ctx') (f := f); auto.
   eapply BASE; eauto.
   eapply add_moves_spec; eauto.
-    intros. rewrite S1. eapply set_instr_other; eauto. unfold node; xomega.
-    xomega. xomega.
+    intros. rewrite S1. eapply set_instr_other; eauto. unfold node; extlia.
+    extlia. extlia.
   eapply rec_spec; eauto.
     red; intros. rewrite PTree.grspec in H. destruct (PTree.elt_eq id0 id); try discriminate. auto.
-    simpl. subst s2; simpl in *; xomega.
-    simpl. subst s3; simpl in *; xomega.
-    simpl. xomega.
+    simpl. subst s2; simpl in *; extlia.
+    simpl. subst s3; simpl in *; extlia.
+    simpl. extlia.
     simpl. apply align_divides. apply min_alignment_pos.
-    assert (dstk ctx + mstk ctx <= dstk ctx'). simpl. apply align_le. apply min_alignment_pos. omega.
-    omega.
+    assert (dstk ctx + mstk ctx <= dstk ctx'). simpl. apply align_le. apply min_alignment_pos. lia.
+    lia.
     intros. simpl in H. rewrite S1.
-    transitivity (s1.(st_code)!pc0). eapply set_instr_other; eauto. unfold node in *; xomega.
-    eapply add_moves_unchanged; eauto. unfold node in *; xomega. xomega.
-  red; simpl. subst s2; simpl in *. xomega.
+    transitivity (s1.(st_code)!pc0). eapply set_instr_other; eauto. unfold node in *; extlia.
+    eapply add_moves_unchanged; eauto. unfold node in *; extlia. extlia.
+  red; simpl. subst s2; simpl in *. extlia.
   red; simpl. split. auto. apply align_le. apply min_alignment_pos.
 (* tailcall *)
   destruct (can_inline fe s1) as [|id f P Q].
@@ -532,20 +532,20 @@ Proof.
   apply tr_tailcall_inlined with (pc1 := x0) (ctx' := ctx') (f := f); auto.
   eapply BASE; eauto.
   eapply add_moves_spec; eauto.
-    intros. rewrite S1. eapply set_instr_other; eauto. unfold node; xomega. xomega. xomega.
+    intros. rewrite S1. eapply set_instr_other; eauto. unfold node; extlia. extlia. extlia.
   eapply rec_spec; eauto.
     red; intros. rewrite PTree.grspec in H. destruct (PTree.elt_eq id0 id); try discriminate. auto.
-    simpl. subst s3; simpl in *. subst s2; simpl in *. xomega.
-    simpl. subst s3; simpl in *; xomega.
-    simpl. xomega.
+    simpl. subst s3; simpl in *. subst s2; simpl in *. extlia.
+    simpl. subst s3; simpl in *; extlia.
+    simpl. extlia.
     simpl. apply align_divides. apply min_alignment_pos.
-    assert (dstk ctx <= dstk ctx'). simpl. apply align_le. apply min_alignment_pos. omega.
-    omega.
+    assert (dstk ctx <= dstk ctx'). simpl. apply align_le. apply min_alignment_pos. lia.
+    lia.
     intros. simpl in H. rewrite S1.
-    transitivity (s1.(st_code))!pc0. eapply set_instr_other; eauto. unfold node in *; xomega.
-    eapply add_moves_unchanged; eauto. unfold node in *; xomega. xomega.
+    transitivity (s1.(st_code))!pc0. eapply set_instr_other; eauto. unfold node in *; extlia.
+    eapply add_moves_unchanged; eauto. unfold node in *; extlia. extlia.
   red; simpl.
-subst s2; simpl in *; xomega.
+subst s2; simpl in *; extlia.
   red; auto.
 (* builtin *)
   eapply tr_builtin; eauto. destruct b; eauto.
@@ -577,31 +577,31 @@ Proof.
   destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr.
   assert (A: Ple ctx.(dpc) s0.(st_nextnode)).
     assert (B: Plt (spc ctx pc) (st_nextnode s)) by eauto.
-    unfold spc in B. generalize (shiftpos_above pc (dpc ctx)). xomega.
+    unfold spc in B. generalize (shiftpos_above pc (dpc ctx)). extlia.
   destruct H9. inv H.
   (* same pc *)
   eapply expand_instr_spec; eauto.
-  omega.
+  lia.
   intros.
     transitivity ((st_code s')!pc').
-    apply H7. auto. xomega.
+    apply H7. auto. extlia.
     eapply iter_expand_instr_unchanged; eauto.
     red; intros. rewrite list_map_compose in H9. exploit list_in_map_inv; eauto.
     intros [[pc0 instr0] [P Q]]. simpl in P.
-    assert (Plt (spc ctx pc0) (st_nextnode s)) by eauto. xomega.
+    assert (Plt (spc ctx pc0) (st_nextnode s)) by eauto. extlia.
   transitivity ((st_code s')!(spc ctx pc)).
     eapply H8; eauto.
     eapply iter_expand_instr_unchanged; eauto.
-    assert (Plt (spc ctx pc) (st_nextnode s)) by eauto. xomega.
+    assert (Plt (spc ctx pc) (st_nextnode s)) by eauto. extlia.
     red; intros. rewrite list_map_compose in H. exploit list_in_map_inv; eauto.
     intros [[pc0 instr0] [P Q]]. simpl in P.
     assert (pc = pc0) by (eapply shiftpos_inj; eauto). subst pc0.
     elim H12. change pc with (fst (pc, instr0)). apply List.in_map; auto.
   (* older pc *)
   inv_incr. eapply IHl; eauto.
-  intros. eapply Pos.lt_le_trans. eapply H2. right; eauto. xomega.
+  intros. eapply Pos.lt_le_trans. eapply H2. right; eauto. extlia.
   intros; eapply Ple_trans; eauto.
-  intros. apply H7; auto. xomega.
+  intros. apply H7; auto. extlia.
 Qed.
 
 Lemma expand_cfg_rec_spec:
@@ -629,16 +629,16 @@ Proof.
   intros.
     assert (Ple pc0 (max_pc_function f)).
       eapply max_pc_function_sound. eapply PTree.elements_complete; eauto.
-      eapply Pos.lt_le_trans. apply shiftpos_below. subst s0; simpl; xomega.
+      eapply Pos.lt_le_trans. apply shiftpos_below. subst s0; simpl; extlia.
   subst s0; simpl; auto.
-  intros. apply H8; auto. subst s0; simpl in H11; xomega.
+  intros. apply H8; auto. subst s0; simpl in H11; extlia.
   intros. apply H8. apply shiftpos_above.
   assert (Ple pc0 (max_pc_function f)).
     eapply max_pc_function_sound. eapply PTree.elements_complete; eauto.
-  eapply Pos.lt_le_trans. apply shiftpos_below. inversion i; xomega.
+  eapply Pos.lt_le_trans. apply shiftpos_below. inversion i; extlia.
   apply PTree.elements_correct; auto.
   auto. auto. auto.
-  inversion INCR0. subst s0; simpl in STKSIZE; xomega.
+  inversion INCR0. subst s0; simpl in STKSIZE; extlia.
 Qed.
 
 End EXPAND_INSTR.
@@ -721,12 +721,12 @@ Opaque initstate.
   apply funenv_program_compat.
   eapply expand_cfg_spec with (fe := fenv); eauto.
     red; auto.
-    unfold ctx; rewrite <- H1; rewrite <- H2; rewrite <- H3; simpl. xomega.
-    unfold ctx; rewrite <- H0; rewrite <- H1; simpl. xomega.
-    simpl. xomega.
+    unfold ctx; rewrite <- H1; rewrite <- H2; rewrite <- H3; simpl. extlia.
+    unfold ctx; rewrite <- H0; rewrite <- H1; simpl. extlia.
+    simpl. extlia.
     simpl. apply Z.divide_0_r.
-    simpl. omega.
-  simpl. omega.
+    simpl. lia.
+  simpl. lia.
   simpl. split; auto. destruct INCR2. destruct INCR1. destruct INCR0. destruct INCR.
-  simpl. change 0 with (st_stksize initstate). omega.
+  simpl. change 0 with (st_stksize initstate). lia.
 Qed.
diff --git a/backend/JsonAST.ml b/backend/JsonAST.ml
index c73bf30d..2e70aae7 100644
--- a/backend/JsonAST.ml
+++ b/backend/JsonAST.ml
@@ -21,14 +21,22 @@ open Sections
 let pp_storage pp static =
   pp_jstring pp (if static then "Static" else "Extern")
 
+let pp_init pp init =
+  pp_jstring pp
+    (match init with
+      | Uninit -> "Uninit"
+      | Init -> "Init"
+      | Init_reloc -> "Init_reloc")
+
 let pp_section pp sec =
   let pp_simple name =
     pp_jsingle_object pp "Section Name" pp_jstring name
   and pp_complex name init =
     pp_jobject_start pp;
     pp_jmember ~first:true pp "Section Name" pp_jstring name;
-    pp_jmember pp "Init" pp_jbool init;
+    pp_jmember pp "Init" pp_init init;
     pp_jobject_end pp in
+
   match sec with
   | Section_text -> pp_simple "Text"
   | Section_data(init, thread_local) -> pp_complex "Data" init (* FIXME *)
@@ -106,11 +114,17 @@ let pp_program pp pp_inst prog =
   let prog_vars,prog_funs = List.fold_left (fun (vars,funs) (ident,def) ->
       match def with
       | Gfun (Internal f) ->
+        (* No assembly is generated for non static inline functions *)
         if not (atom_is_iso_inline_definition ident) then
           vars,(ident,f)::funs
         else
           vars,funs
-      | Gvar v -> (ident,v)::vars,funs
+      | Gvar v ->
+        (* No assembly is generated for variables without init *)
+        if v.gvar_init <> [] then
+          (ident,v)::vars,funs
+        else
+          vars, funs
       | _ -> vars,funs) ([],[]) prog.prog_defs in
   pp_jobject_start pp;
   pp_jmember ~first:true pp "Global Variables" (pp_jarray pp_vardef) prog_vars;
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index 18dc52a5..c12eab6e 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -658,7 +658,7 @@ Proof.
 
 - (* Lbranch *)
   assert ((reachable f)!!pc = true). apply REACH; simpl; auto.
-  right; split. simpl; omega. split. auto. simpl. econstructor; eauto.
+  right; split. simpl; lia. split. auto. simpl. econstructor; eauto.
 
 - (* Lcond *)
   assert (REACH1: (reachable f)!!pc1 = true) by (apply REACH; simpl; auto).
@@ -675,12 +675,12 @@ Proof.
   rewrite eval_negate_condition. rewrite H. auto. eauto.
   rewrite DC. econstructor; eauto.
   (* cond is false: branch is taken *)
-  right; split. simpl; omega. split. auto.  rewrite <- DC. econstructor; eauto.
+  right; split. simpl; lia. split. auto.  rewrite <- DC. econstructor; eauto.
   rewrite eval_negate_condition. rewrite H. auto.
   (* branch if cond is true *)
   destruct b.
   (* cond is true: branch is taken *)
-  right; split. simpl; omega. split. auto. econstructor; eauto.
+  right; split. simpl; lia. split. auto. econstructor; eauto.
   (* cond is false: no branch *)
   left; econstructor; split.
   apply plus_one. eapply exec_Lcond_false. eauto. eauto.
@@ -689,7 +689,7 @@ Proof.
 - (* Ljumptable *)
   assert (REACH': (reachable f)!!pc = true).
     apply REACH. simpl. eapply list_nth_z_in; eauto.
-  right; split. simpl; omega. split. auto. econstructor; eauto.
+  right; split. simpl; lia. split. auto. econstructor; eauto.
 
 - (* Lreturn *)
   left; econstructor; split.
diff --git a/backend/Locations.v b/backend/Locations.v
index c437df5d..2a3ae1d7 100644
--- a/backend/Locations.v
+++ b/backend/Locations.v
@@ -157,7 +157,7 @@ Module Loc.
     forall l, ~(diff l l).
   Proof.
     destruct l; unfold diff; auto.
-    red; intros. destruct H; auto. generalize (typesize_pos ty); omega.
+    red; intros. destruct H; auto. generalize (typesize_pos ty); lia.
   Qed.
 
   Lemma diff_not_eq:
@@ -184,7 +184,7 @@ Module Loc.
     left; auto.
     destruct (zle (pos0 + typesize ty0) pos).
     left; auto.
-    right; red; intros [P | [P | P]]. congruence. omega. omega.
+    right; red; intros [P | [P | P]]. congruence. lia. lia.
     left; auto.
   Defined.
 
@@ -497,7 +497,7 @@ Module OrderedLoc <: OrderedType.
     destruct x.
     eelim Plt_strict; eauto.
     destruct H. eelim OrderedSlot.lt_not_eq; eauto. red; auto.
-    destruct H. destruct H0. omega.
+    destruct H. destruct H0. lia.
     destruct H0. eelim OrderedTyp.lt_not_eq; eauto. red; auto.
   Qed.
   Definition compare : forall x y : t, Compare lt eq x y.
@@ -545,18 +545,18 @@ Module OrderedLoc <: OrderedType.
       { destruct H. apply not_eq_sym. apply Plt_ne; auto. apply Plt_ne; auto. }
       congruence.
     - assert (RANGE: forall ty, 1 <= typesize ty <= 2).
-      { intros; unfold typesize. destruct ty0; omega.  }
+      { intros; unfold typesize. destruct ty0; lia.  }
       destruct H.
       + destruct H. left. apply not_eq_sym. apply OrderedSlot.lt_not_eq; auto.
         destruct H. right.
-        destruct H0. right. generalize (RANGE ty'); omega.
+        destruct H0. right. generalize (RANGE ty'); lia.
         destruct H0.
         assert (ty' = Tint \/ ty' = Tsingle \/ ty' = Tany32).
         { unfold OrderedTyp.lt in H1. destruct ty'; auto; compute in H1; congruence. }
-        right. destruct H2 as [E|[E|E]]; subst ty'; simpl typesize; omega.
+        right. destruct H2 as [E|[E|E]]; subst ty'; simpl typesize; lia.
       + destruct H. left. apply OrderedSlot.lt_not_eq; auto.
         destruct H. right.
-        destruct H0. left; omega.
+        destruct H0. left; lia.
         destruct H0. exfalso. destruct ty'; compute in H1; congruence.
   Qed.
 
@@ -572,14 +572,14 @@ Module OrderedLoc <: OrderedType.
     - destruct (OrderedSlot.compare sl sl'); auto.
       destruct H. contradiction.
       destruct H.
-      right; right; split; auto. left; omega.
+      right; right; split; auto. left; lia.
       left; right; split; auto.
       assert (EITHER: typesize ty' = 1 /\ OrderedTyp.lt ty' Tany64 \/ typesize ty' = 2).
       { destruct ty'; compute; auto. }
       destruct (zlt ofs' (ofs - 1)). left; auto.
       destruct EITHER as [[P Q] | P].
-      right; split; auto. omega.
-      left; omega.
+      right; split; auto. lia.
+      left; lia.
   Qed.
 
 End OrderedLoc.
diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v
index d9e9e025..62b8ff90 100644
--- a/backend/NeedDomain.v
+++ b/backend/NeedDomain.v
@@ -74,7 +74,7 @@ Proof.
   intros. simpl in H. auto.
 Qed.
 
-Hint Resolve vagree_same vagree_lessdef lessdef_vagree: na.
+Global Hint Resolve vagree_same vagree_lessdef lessdef_vagree: na.
 
 Inductive vagree_list: list val -> list val -> list nval -> Prop :=
   | vagree_list_nil: forall nvl,
@@ -100,7 +100,7 @@ Proof.
   destruct nvl; constructor; auto with na.
 Qed.
 
-Hint Resolve lessdef_vagree_list vagree_lessdef_list: na.
+Global Hint Resolve lessdef_vagree_list vagree_lessdef_list: na.
 
 (** ** Ordering and least upper bound between value needs *)
 
@@ -116,8 +116,8 @@ Proof.
   destruct x; constructor; auto.
 Qed.
 
-Hint Constructors nge: na.
-Hint Resolve nge_refl: na.
+Global Hint Constructors nge: na.
+Global Hint Resolve nge_refl: na.
 
 Lemma nge_trans: forall x y, nge x y -> forall z, nge y z -> nge x z.
 Proof.
@@ -240,9 +240,9 @@ Proof.
   destruct (zlt i (Int.unsigned n)).
 - auto.
 - generalize (Int.unsigned_range n); intros.
-  apply H. omega. rewrite Int.bits_shru by omega.
-  replace (i - Int.unsigned n + Int.unsigned n) with i by omega.
-  rewrite zlt_true by omega. auto.
+  apply H. lia. rewrite Int.bits_shru by lia.
+  replace (i - Int.unsigned n + Int.unsigned n) with i by lia.
+  rewrite zlt_true by lia. auto.
 Qed.
 
 Lemma iagree_shru:
@@ -252,9 +252,9 @@ Proof.
   intros; red; intros. autorewrite with ints; auto.
   destruct (zlt (i + Int.unsigned n) Int.zwordsize).
 - generalize (Int.unsigned_range n); intros.
-  apply H. omega. rewrite Int.bits_shl by omega.
-  replace (i + Int.unsigned n - Int.unsigned n) with i by omega.
-  rewrite zlt_false by omega. auto.
+  apply H. lia. rewrite Int.bits_shl by lia.
+  replace (i + Int.unsigned n - Int.unsigned n) with i by lia.
+  rewrite zlt_false by lia. auto.
 - auto.
 Qed.
 
@@ -266,7 +266,7 @@ Proof.
   intros; red; intros. rewrite <- H in H2. rewrite Int.bits_shru in H2 by auto.
   rewrite ! Int.bits_shr by auto.
   destruct (zlt (i + Int.unsigned n) Int.zwordsize).
-- apply H0; auto. generalize (Int.unsigned_range n); omega.
+- apply H0; auto. generalize (Int.unsigned_range n); lia.
 - discriminate.
 Qed.
 
@@ -281,11 +281,11 @@ Proof.
             then i + Int.unsigned n
             else Int.zwordsize - 1).
   assert (0 <= j < Int.zwordsize).
-  { unfold j; destruct (zlt (i + Int.unsigned n) Int.zwordsize); omega. }
+  { unfold j; destruct (zlt (i + Int.unsigned n) Int.zwordsize); lia. }
   apply H; auto. autorewrite with ints; auto. apply orb_true_intro.
   unfold j; destruct (zlt (i + Int.unsigned n) Int.zwordsize).
-- left. rewrite zlt_false by omega.
-  replace (i + Int.unsigned n - Int.unsigned n) with i by omega.
+- left. rewrite zlt_false by lia.
+  replace (i + Int.unsigned n - Int.unsigned n) with i by lia.
   auto.
 - right. reflexivity.
 Qed.
@@ -303,7 +303,7 @@ Proof.
    mod Int.zwordsize) with i. auto.
   apply eqmod_small_eq with Int.zwordsize; auto.
   apply eqmod_trans with ((i - Int.unsigned amount) + Int.unsigned amount).
-  apply eqmod_refl2; omega.
+  apply eqmod_refl2; lia.
   eapply eqmod_trans. 2: apply eqmod_mod; auto.
   apply eqmod_add.
   apply eqmod_mod; auto.
@@ -330,12 +330,12 @@ Lemma eqmod_iagree:
 Proof.
   intros. set (p := Z.to_nat (Int.size m)).
   generalize (Int.size_range m); intros RANGE.
-  assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply Z2Nat.id. omega. }
+  assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply Z2Nat.id. lia. }
   rewrite EQ in H; rewrite <- two_power_nat_two_p in H.
   red; intros. rewrite ! Int.testbit_repr by auto.
   destruct (zlt i (Int.size m)).
-  eapply same_bits_eqmod; eauto. omega.
-  assert (Int.testbit m i = false) by (eapply Int.bits_size_2; omega).
+  eapply same_bits_eqmod; eauto. lia.
+  assert (Int.testbit m i = false) by (eapply Int.bits_size_2; lia).
   congruence.
 Qed.
 
@@ -348,11 +348,11 @@ Lemma iagree_eqmod:
 Proof.
   intros. set (p := Z.to_nat (Int.size m)).
   generalize (Int.size_range m); intros RANGE.
-  assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply Z2Nat.id. omega. }
+  assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply Z2Nat.id. lia. }
   rewrite EQ; rewrite <- two_power_nat_two_p.
-  apply eqmod_same_bits. intros. apply H. omega.
-  unfold complete_mask. rewrite Int.bits_zero_ext by omega.
-  rewrite zlt_true by omega. rewrite Int.bits_mone by omega. auto.
+  apply eqmod_same_bits. intros. apply H. lia.
+  unfold complete_mask. rewrite Int.bits_zero_ext by lia.
+  rewrite zlt_true by lia. rewrite Int.bits_mone by lia. auto.
 Qed.
 
 Lemma complete_mask_idem:
@@ -363,12 +363,12 @@ Proof.
 + assert (Int.unsigned m <> 0).
   { red; intros; elim n. rewrite <- (Int.repr_unsigned m). rewrite H; auto. }
   assert (0 < Int.size m).
-  { apply Zsize_pos'. generalize (Int.unsigned_range m); omega. }
+  { apply Zsize_pos'. generalize (Int.unsigned_range m); lia. }
   generalize (Int.size_range m); intros.
   f_equal. apply Int.bits_size_4. tauto.
-  rewrite Int.bits_zero_ext by omega. rewrite zlt_true by omega.
-  apply Int.bits_mone; omega.
-  intros. rewrite Int.bits_zero_ext by omega. apply zlt_false; omega.
+  rewrite Int.bits_zero_ext by lia. rewrite zlt_true by lia.
+  apply Int.bits_mone; lia.
+  intros. rewrite Int.bits_zero_ext by lia. apply zlt_false; lia.
 Qed.
 
 (** ** Abstract operations over value needs. *)
@@ -676,12 +676,12 @@ Proof.
   destruct x; simpl in *.
 - auto.
 - unfold Val.zero_ext; InvAgree.
-  red; intros. autorewrite with ints; try omega.
+  red; intros. autorewrite with ints; try lia.
   destruct (zlt i1 n); auto. apply H; auto.
-  autorewrite with ints; try omega. rewrite zlt_true; auto.
+  autorewrite with ints; try lia. rewrite zlt_true; auto.
 - unfold Val.zero_ext; InvAgree; auto. apply Val.lessdef_same. f_equal.
-  Int.bit_solve; try omega. destruct (zlt i1 n); auto. apply H; auto.
-  autorewrite with ints; try omega. apply zlt_true; auto.
+  Int.bit_solve; try lia. destruct (zlt i1 n); auto. apply H; auto.
+  autorewrite with ints; try lia. apply zlt_true; auto.
 Qed.
 
 Definition sign_ext (n: Z) (x: nval) :=
@@ -700,25 +700,25 @@ Proof.
   unfold sign_ext; intros. destruct x; simpl in *.
 - auto.
 - unfold Val.sign_ext; InvAgree.
-  red; intros. autorewrite with ints; try omega.
+  red; intros. autorewrite with ints; try lia.
   set (j := if zlt i1 n then i1 else n - 1).
   assert (0 <= j < Int.zwordsize).
-  { unfold j; destruct (zlt i1 n); omega. }
+  { unfold j; destruct (zlt i1 n); lia. }
   apply H; auto.
-  autorewrite with ints; try omega. apply orb_true_intro.
+  autorewrite with ints; try lia. apply orb_true_intro.
   unfold j; destruct (zlt i1 n).
   left. rewrite zlt_true; auto.
-  right. rewrite Int.unsigned_repr. rewrite zlt_false by omega.
-  replace (n - 1 - (n - 1)) with 0 by omega. reflexivity.
-  generalize Int.wordsize_max_unsigned; omega.
+  right. rewrite Int.unsigned_repr. rewrite zlt_false by lia.
+  replace (n - 1 - (n - 1)) with 0 by lia. reflexivity.
+  generalize Int.wordsize_max_unsigned; lia.
 - unfold Val.sign_ext; InvAgree; auto. apply Val.lessdef_same. f_equal.
-  Int.bit_solve; try omega.
+  Int.bit_solve; try lia.
   set (j := if zlt i1 n then i1 else n - 1).
   assert (0 <= j < Int.zwordsize).
-  { unfold j; destruct (zlt i1 n); omega. }
-  apply H; auto. rewrite Int.bits_zero_ext; try omega.
+  { unfold j; destruct (zlt i1 n); lia. }
+  apply H; auto. rewrite Int.bits_zero_ext; try lia.
   rewrite zlt_true. apply Int.bits_mone; auto.
-  unfold j. destruct (zlt i1 n); omega.
+  unfold j. destruct (zlt i1 n); lia.
 Qed.
 
 (** The needs of a memory store concerning the value being stored. *)
@@ -737,7 +737,7 @@ Lemma store_argument_sound:
 Proof.
   intros.
   assert (UNDEF: list_forall2 memval_lessdef
-                     (list_repeat (size_chunk_nat chunk) Undef)
+                     (List.repeat Undef (size_chunk_nat chunk))
                      (encode_val chunk w)).
   {
      rewrite <- (encode_val_length chunk w).
@@ -778,11 +778,11 @@ Proof.
 - apply sign_ext_sound with (v := Vint i) (w := Vint i0) (x := All) (n := 8).
   auto. compute; auto.
 - apply zero_ext_sound with (v := Vint i) (w := Vint i0) (x := All) (n := 8).
-  auto. omega.
+  auto. lia.
 - apply sign_ext_sound with (v := Vint i) (w := Vint i0) (x := All) (n := 16).
   auto. compute; auto.
 - apply zero_ext_sound with (v := Vint i) (w := Vint i0) (x := All) (n := 16).
-  auto. omega.
+  auto. lia.
 Qed.
 
 (** The needs of a comparison *)
@@ -1014,9 +1014,9 @@ Proof.
   unfold zero_ext_redundant; intros. destruct x; try discriminate.
 - auto.
 - simpl in *; InvAgree. simpl. InvBooleans. rewrite <- H.
-  red; intros; autorewrite with ints; try omega.
+  red; intros; autorewrite with ints; try lia.
   destruct (zlt i1 n). apply H0; auto.
-  rewrite Int.bits_zero_ext in H3 by omega. rewrite zlt_false in H3 by auto. discriminate.
+  rewrite Int.bits_zero_ext in H3 by lia. rewrite zlt_false in H3 by auto. discriminate.
 Qed.
 
 Definition sign_ext_redundant (n: Z) (x: nval) :=
@@ -1036,10 +1036,10 @@ Proof.
   unfold sign_ext_redundant; intros. destruct x; try discriminate.
 - auto.
 - simpl in *; InvAgree. simpl. InvBooleans. rewrite <- H.
-  red; intros; autorewrite with ints; try omega.
+  red; intros; autorewrite with ints; try lia.
   destruct (zlt i1 n). apply H0; auto.
   rewrite Int.bits_or; auto. rewrite H3; auto.
-  rewrite Int.bits_zero_ext in H3 by omega. rewrite zlt_false in H3 by auto. discriminate.
+  rewrite Int.bits_zero_ext in H3 by lia. rewrite zlt_false in H3 by auto. discriminate.
 Qed.
 
 (** * Neededness for register environments *)
@@ -1084,7 +1084,7 @@ Proof.
   intros. apply H.
 Qed.
 
-Hint Resolve nreg_agree: na.
+Global Hint Resolve nreg_agree: na.
 
 Lemma eagree_ge:
   forall e1 e2 ne ne',
@@ -1300,13 +1300,13 @@ Proof.
   split; simpl; auto; intros.
   rewrite PTree.gsspec in H6. destruct (peq id0 id).
 + inv H6. destruct H3. congruence. destruct gl!id as [iv0|] eqn:NG.
-  unfold iv'; rewrite ISet.In_add. intros [P|P]. omega. eelim GL; eauto.
-  unfold iv'; rewrite ISet.In_interval. omega.
+  unfold iv'; rewrite ISet.In_add. intros [P|P]. lia. eelim GL; eauto.
+  unfold iv'; rewrite ISet.In_interval. lia.
 + eauto.
 - (* Stk ofs *)
   split; simpl; auto; intros. destruct H3.
   elim H3. subst b'. eapply bc_stack; eauto.
-  rewrite ISet.In_add. intros [P|P]. omega. eapply STK; eauto.
+  rewrite ISet.In_add. intros [P|P]. lia. eapply STK; eauto.
 Qed.
 
 (** Test (conservatively) whether some locations in the range delimited
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index 0635e32d..7cc386ed 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -121,7 +121,7 @@ module Printer(Target:TARGET) =
           let sec =
             match C2C.atom_sections name with
             | [s] -> s
-            |  _  -> Section_data (true, false)
+            |  _  -> Section_data (Init, false)  (* FIX Sylvain: not sure of this fix *) 
           and align =
             match C2C.atom_alignof name with
             | Some a -> a
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 5cb693af..f1978ad2 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -307,15 +307,32 @@ let print_version_and_options oc comment =
     fprintf oc " %s" Commandline.argv.(i)
   done;
   fprintf oc "\n"
-  
-(** Get the name of the common section if it is used otherwise the given section
-    name, with bss as default *)
 
-let common_section ?(sec = ".bss") () =
-  if !Clflags.option_fcommon then
-    "COMM"
-  else
-    sec;;
+(** Determine the name of the section to use for a variable.
+  - [i] is the initialization status of the variable.
+  - [sec] is the name of the section to use if initialized (with no
+    relocations) or if no other cases apply.
+  - [reloc] is the name of the section to use if initialized and
+    containing relocations.  If not provided, [sec] is used.
+  - [bss] is the name of the section to use if uninitialized and
+    common declarations are not used.  If not provided, [sec] is used.
+  - [common] says whether common declarations can be used for uninitialized
+    variables.  It defaults to the status of the [-fcommon] / [-fno-common]
+    command-line option.  Passing [~common:false] is needed when
+    common declarations cannot be used at all, for example in the context of
+    small data areas.
+*)
+
+let variable_section ~sec ?bss ?reloc ?(common = !Clflags.option_fcommon) i =
+  match i with
+  | Uninit ->
+      if common
+      then "COMM"
+      else begin match bss with Some s -> s | None -> sec end
+  | Init -> sec
+  | Init_reloc ->
+      begin match reloc with Some s -> s | None -> sec end
+
 
 (* Profiling *)
 let profiling_table : (Digest.t, int) Hashtbl.t = Hashtbl.create 1000;;
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index 051225a4..9ca0e3a0 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -6,10 +6,11 @@
 (*                                                                     *)
 (*  Copyright Institut National de Recherche en Informatique et en     *)
 (*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the GNU General Public License as published by  *)
-(*  the Free Software Foundation, either version 2 of the License, or  *)
-(*  (at your option) any later version.  This file is also distributed *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*  under the terms of the GNU Lesser General Public License as        *)
+(*  published by the Free Software Foundation, either version 2.1 of   *)
+(*  the License, or  (at your option) any later version.               *)
+(*  This file is also distributed under the terms of the               *)
+(*  INRIA Non-Commercial License Agreement.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/backend/RTL.v b/backend/RTL.v
index dec59ca2..31b5cf99 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -367,7 +367,7 @@ Proof.
   exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]].
   exists (Returnstate s0 vres2 m2). econstructor; eauto.
 (* trace length *)
-  red; intros; inv H; simpl; try omega.
+  red; intros; inv H; simpl; try lia.
   eapply external_call_trace_length; eauto.
   eapply external_call_trace_length; eauto.
 Qed.
@@ -465,8 +465,8 @@ Proof.
   rewrite PTree.gempty. congruence.
   (* inductive case *)
   intros. rewrite PTree.gsspec in H2. destruct (peq pc k).
-  inv H2. xomega.
-  apply Ple_trans with a. auto. xomega.
+  inv H2. extlia.
+  apply Ple_trans with a. auto. extlia.
 Qed.
 
 (** Maximum pseudo-register mentioned in a function.  All results or arguments
@@ -504,9 +504,9 @@ Proof.
   assert (X: forall l n, Ple m n -> Ple m (fold_left Pos.max l n)).
   { induction l; simpl; intros.
     auto.
-    apply IHl. xomega. }
-  destruct i; simpl; try (destruct s0); repeat (apply X); try xomega.
-  destruct o; xomega.
+    apply IHl. extlia. }
+  destruct i; simpl; try (destruct s0); repeat (apply X); try extlia.
+  destruct o; extlia.
 Qed.
 
 Remark max_reg_instr_def:
@@ -514,12 +514,12 @@ Remark max_reg_instr_def:
 Proof.
   intros.
   assert (X: forall l n, Ple r n -> Ple r (fold_left Pos.max l n)).
-  { induction l; simpl; intros. xomega. apply IHl. xomega. }
+  { induction l; simpl; intros. extlia. apply IHl. extlia. }
   destruct i; simpl in *; inv H.
-- apply X. xomega.
-- apply X. xomega.
-- destruct s0; apply X; xomega.
-- destruct b; inv H1. apply X. simpl. xomega.
+- apply X. extlia.
+- apply X. extlia.
+- destruct s0; apply X; extlia.
+- destruct b; inv H1. apply X. simpl. extlia.
 Qed.
 
 Remark max_reg_instr_uses:
@@ -529,14 +529,14 @@ Proof.
   assert (X: forall l n, In r l \/ Ple r n -> Ple r (fold_left Pos.max l n)).
   { induction l; simpl; intros.
     tauto.
-    apply IHl. destruct H0 as [[A|A]|A]. right; subst; xomega. auto. right; xomega. }
+    apply IHl. destruct H0 as [[A|A]|A]. right; subst; extlia. auto. right; extlia. }
   destruct i; simpl in *; try (destruct s0); try (apply X; auto).
 - contradiction.
-- destruct H. right; subst; xomega. auto.
-- destruct H. right; subst; xomega. auto.
-- destruct H. right; subst; xomega. auto.
-- intuition. subst; xomega.
-- destruct o; simpl in H; intuition. subst; xomega.
+- destruct H. right; subst; extlia. auto.
+- destruct H. right; subst; extlia. auto.
+- destruct H. right; subst; extlia. auto.
+- intuition. subst; extlia.
+- destruct o; simpl in H; intuition. subst; extlia.
 Qed.
 
 Lemma max_reg_function_def:
@@ -554,7 +554,7 @@ Proof.
      + inv H3. eapply max_reg_instr_def; eauto.
      + apply Ple_trans with a. auto. apply max_reg_instr_ge.
   }
-  unfold max_reg_function. xomega.
+  unfold max_reg_function. extlia.
 Qed.
 
 Lemma max_reg_function_use:
@@ -572,7 +572,7 @@ Proof.
      + inv H3. eapply max_reg_instr_uses; eauto.
      + apply Ple_trans with a. auto. apply max_reg_instr_ge.
   }
-  unfold max_reg_function. xomega.
+  unfold max_reg_function. extlia.
 Qed.
 
 Lemma max_reg_function_params:
@@ -582,8 +582,8 @@ Proof.
   assert (X: forall l n, In r l \/ Ple r n -> Ple r (fold_left Pos.max l n)).
   { induction l; simpl; intros.
     tauto.
-    apply IHl. destruct H0 as [[A|A]|A]. right; subst; xomega. auto. right; xomega. }
+    apply IHl. destruct H0 as [[A|A]|A]. right; subst; extlia. auto. right; extlia. }
   assert (Y: Ple r (fold_left Pos.max f.(fn_params) 1%positive)).
   { apply X; auto. }
-  unfold max_reg_function. xomega.
+  unfold max_reg_function. extlia.
 Qed.
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index e62aff22..d07dc968 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -165,7 +165,7 @@ Proof.
   subst r0; contradiction.
   apply Regmap.gso; auto.
 Qed.
-Hint Resolve match_env_update_temp: rtlg.
+Global Hint Resolve match_env_update_temp: rtlg.
 
 (** Matching between environments is preserved by simultaneous
   assignment to a Cminor local variable (in the Cminor environments)
@@ -205,7 +205,7 @@ Proof.
   eapply match_env_update_temp; eauto.
   eapply match_env_update_var; eauto.
 Qed.
-Hint Resolve match_env_update_dest: rtlg.
+Global Hint Resolve match_env_update_dest: rtlg.
 
 (** A variant of [match_env_update_var] corresponding to the assignment
   of the result of a builtin. *)
@@ -1145,7 +1145,7 @@ Proof.
 Qed.
 
 Ltac Lt_state :=
-  apply lt_state_intro; simpl; try omega.
+  apply lt_state_intro; simpl; try lia.
 
 Lemma lt_state_wf:
   well_founded lt_state.
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index 36b8409d..0210aa5b 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -128,7 +128,7 @@ Ltac monadInv H :=
 
 (** * Monotonicity properties of the state *)
 
-Hint Resolve state_incr_refl: rtlg.
+Global Hint Resolve state_incr_refl: rtlg.
 
 Lemma instr_at_incr:
   forall s1 s2 n i,
@@ -137,7 +137,7 @@ Proof.
   intros. inv H.
   destruct (H3 n); congruence.
 Qed.
-Hint Resolve instr_at_incr: rtlg.
+Global Hint Resolve instr_at_incr: rtlg.
 
 (** The following tactic saturates the hypotheses with
   [state_incr] properties that follow by transitivity from
@@ -174,14 +174,14 @@ Lemma valid_fresh_absurd:
 Proof.
   intros r s. unfold reg_valid, reg_fresh; case r; tauto.
 Qed.
-Hint Resolve valid_fresh_absurd: rtlg.
+Global Hint Resolve valid_fresh_absurd: rtlg.
 
 Lemma valid_fresh_different:
   forall r1 r2 s, reg_valid r1 s -> reg_fresh r2 s -> r1 <> r2.
 Proof.
   unfold not; intros. subst r2. eauto with rtlg.
 Qed.
-Hint Resolve valid_fresh_different: rtlg.
+Global Hint Resolve valid_fresh_different: rtlg.
 
 Lemma reg_valid_incr:
   forall r s1 s2, state_incr s1 s2 -> reg_valid r s1 -> reg_valid r s2.
@@ -190,7 +190,7 @@ Proof.
   inversion INCR.
   unfold reg_valid. intros; apply Plt_Ple_trans with (st_nextreg s1); auto.
 Qed.
-Hint Resolve reg_valid_incr: rtlg.
+Global Hint Resolve reg_valid_incr: rtlg.
 
 Lemma reg_fresh_decr:
   forall r s1 s2, state_incr s1 s2 -> reg_fresh r s2 -> reg_fresh r s1.
@@ -199,7 +199,7 @@ Proof.
   unfold reg_fresh; unfold not; intros.
   apply H4. apply Plt_Ple_trans with (st_nextreg s1); auto.
 Qed.
-Hint Resolve reg_fresh_decr: rtlg.
+Global Hint Resolve reg_fresh_decr: rtlg.
 
 (** Validity of a list of registers. *)
 
@@ -211,7 +211,7 @@ Lemma regs_valid_nil:
 Proof.
   intros; red; intros. elim H.
 Qed.
-Hint Resolve regs_valid_nil: rtlg.
+Global Hint Resolve regs_valid_nil: rtlg.
 
 Lemma regs_valid_cons:
   forall r1 rl s,
@@ -232,7 +232,7 @@ Lemma regs_valid_incr:
 Proof.
   unfold regs_valid; intros; eauto with rtlg.
 Qed.
-Hint Resolve regs_valid_incr: rtlg.
+Global Hint Resolve regs_valid_incr: rtlg.
 
 (** A register is ``in'' a mapping if it is associated with a Cminor
   local or let-bound variable. *)
@@ -253,7 +253,7 @@ Lemma map_valid_incr:
 Proof.
   unfold map_valid; intros; eauto with rtlg.
 Qed.
-Hint Resolve map_valid_incr: rtlg.
+Global Hint Resolve map_valid_incr: rtlg.
 
 (** * Properties of basic operations over the state *)
 
@@ -265,7 +265,7 @@ Lemma add_instr_at:
 Proof.
   intros. monadInv H. simpl. apply PTree.gss.
 Qed.
-Hint Resolve add_instr_at: rtlg.
+Global Hint Resolve add_instr_at: rtlg.
 
 (** Properties of [update_instr]. *)
 
@@ -278,7 +278,7 @@ Proof.
   destruct (check_empty_node s1 n); try discriminate.
   inv H. simpl. apply PTree.gss.
 Qed.
-Hint Resolve update_instr_at: rtlg.
+Global Hint Resolve update_instr_at: rtlg.
 
 (** Properties of [new_reg]. *)
 
@@ -289,7 +289,7 @@ Proof.
   intros. monadInv H.
   unfold reg_valid; simpl. apply Plt_succ.
 Qed.
-Hint Resolve new_reg_valid: rtlg.
+Global Hint Resolve new_reg_valid: rtlg.
 
 Lemma new_reg_fresh:
   forall s1 s2 r i,
@@ -299,7 +299,7 @@ Proof.
   unfold reg_fresh; simpl.
   exact (Plt_strict _).
 Qed.
-Hint Resolve new_reg_fresh: rtlg.
+Global Hint Resolve new_reg_fresh: rtlg.
 
 Lemma new_reg_not_in_map:
   forall s1 s2 m r i,
@@ -307,7 +307,7 @@ Lemma new_reg_not_in_map:
 Proof.
   unfold not; intros; eauto with rtlg.
 Qed.
-Hint Resolve new_reg_not_in_map: rtlg.
+Global Hint Resolve new_reg_not_in_map: rtlg.
 
 (** * Properties of operations over compilation environments *)
 
@@ -330,7 +330,7 @@ Proof.
   intros. inv H0. left; exists name; auto.
   intros. inv H0.
 Qed.
-Hint Resolve find_var_in_map: rtlg.
+Global Hint Resolve find_var_in_map: rtlg.
 
 Lemma find_var_valid:
   forall s1 s2 map name r i,
@@ -338,7 +338,7 @@ Lemma find_var_valid:
 Proof.
   eauto with rtlg.
 Qed.
-Hint Resolve find_var_valid: rtlg.
+Global Hint Resolve find_var_valid: rtlg.
 
 (** Properties of [find_letvar]. *)
 
@@ -350,7 +350,7 @@ Proof.
   caseEq (nth_error (map_letvars map) idx); intros; monadInv H0.
   right; apply nth_error_in with idx; auto.
 Qed.
-Hint Resolve find_letvar_in_map: rtlg.
+Global Hint Resolve find_letvar_in_map: rtlg.
 
 Lemma find_letvar_valid:
   forall s1 s2 map idx r i,
@@ -358,7 +358,7 @@ Lemma find_letvar_valid:
 Proof.
   eauto with rtlg.
 Qed.
-Hint Resolve find_letvar_valid: rtlg.
+Global Hint Resolve find_letvar_valid: rtlg.
 
 (** Properties of [add_var]. *)
 
@@ -445,7 +445,7 @@ Proof.
   intros until r.  unfold alloc_reg.
   case a; eauto with rtlg.
 Qed.
-Hint Resolve alloc_reg_valid: rtlg.
+Global Hint Resolve alloc_reg_valid: rtlg.
 
 Lemma alloc_reg_fresh_or_in_map:
   forall map a s r s' i,
@@ -469,7 +469,7 @@ Proof.
   apply regs_valid_nil.
   apply regs_valid_cons. eauto with rtlg. eauto with rtlg.
 Qed.
-Hint Resolve alloc_regs_valid: rtlg.
+Global Hint Resolve alloc_regs_valid: rtlg.
 
 Lemma alloc_regs_fresh_or_in_map:
   forall map al s rl s' i,
@@ -494,7 +494,7 @@ Proof.
   intros until r.  unfold alloc_reg.
   case dest; eauto with rtlg.
 Qed.
-Hint Resolve alloc_optreg_valid: rtlg.
+Global Hint Resolve alloc_optreg_valid: rtlg.
 
 Lemma alloc_optreg_fresh_or_in_map:
   forall map dest s r s' i,
@@ -609,7 +609,7 @@ Proof.
   apply regs_valid_cons; eauto with rtlg.
 Qed.
 
-Hint Resolve new_reg_target_ok alloc_reg_target_ok
+Global Hint Resolve new_reg_target_ok alloc_reg_target_ok
              alloc_regs_target_ok: rtlg.
 
 (** The following predicate is a variant of [target_reg_ok] used
@@ -631,7 +631,7 @@ Lemma return_reg_ok_incr:
 Proof.
   induction 1; intros; econstructor; eauto with rtlg.
 Qed.
-Hint Resolve return_reg_ok_incr: rtlg.
+Global Hint Resolve return_reg_ok_incr: rtlg.
 
 Lemma new_reg_return_ok:
   forall s1 r s2 map sig i,
@@ -676,7 +676,7 @@ Inductive reg_map_ok: mapping -> reg -> option ident -> Prop :=
       map.(map_vars)!id = Some rd ->
       reg_map_ok map rd (Some id).
 
-Hint Resolve reg_map_ok_novar: rtlg.
+Global Hint Resolve reg_map_ok_novar: rtlg.
 
 (** [tr_expr c map pr expr ns nd rd optid] holds if the graph [c],
   between nodes [ns] and [nd], contains instructions that compute the
diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v
index 1873da4d..3f91b1ba 100644
--- a/backend/SelectDivproof.v
+++ b/backend/SelectDivproof.v
@@ -45,55 +45,55 @@ Proof.
   set (r := n mod d).
   intro EUCL.
   assert (0 <= r <= d - 1).
-    unfold r. generalize (Z_mod_lt n d d_pos). omega.
+    unfold r. generalize (Z_mod_lt n d d_pos). lia.
   assert (0 <= m).
     apply Zmult_le_0_reg_r with d. auto.
-    exploit (two_p_gt_ZERO (N + l)). omega. omega.
+    exploit (two_p_gt_ZERO (N + l)). lia. lia.
   set (k := m * d - two_p (N + l)).
   assert (0 <= k <= two_p l).
-    unfold k; omega.
+    unfold k; lia.
   assert ((m * n - two_p (N + l) * q) * d = k * n + two_p (N + l) * r).
     unfold k. rewrite EUCL. ring.
   assert (0 <= k * n).
-    apply Z.mul_nonneg_nonneg; omega.
+    apply Z.mul_nonneg_nonneg; lia.
   assert (k * n <= two_p (N + l) - two_p l).
     apply Z.le_trans with (two_p l * n).
-    apply Z.mul_le_mono_nonneg_r; omega.
-    replace (N + l) with (l + N) by omega.
+    apply Z.mul_le_mono_nonneg_r; lia.
+    replace (N + l) with (l + N) by lia.
     rewrite two_p_is_exp.
     replace (two_p l * two_p N - two_p l)
        with (two_p l * (two_p N - 1))
          by ring.
-    apply Z.mul_le_mono_nonneg_l. omega. exploit (two_p_gt_ZERO l). omega. omega.
-    omega. omega.
+    apply Z.mul_le_mono_nonneg_l. lia. exploit (two_p_gt_ZERO l). lia. lia.
+    lia. lia.
   assert (0 <= two_p (N + l) * r).
     apply Z.mul_nonneg_nonneg.
-    exploit (two_p_gt_ZERO (N + l)). omega. omega.
-    omega.
+    exploit (two_p_gt_ZERO (N + l)). lia. lia.
+    lia.
   assert (two_p (N + l) * r <= two_p (N + l) * d - two_p (N + l)).
     replace (two_p (N + l) * d - two_p (N + l))
        with (two_p (N + l) * (d - 1)) by ring.
     apply Z.mul_le_mono_nonneg_l. 
-    omega.
-    exploit (two_p_gt_ZERO (N + l)). omega. omega.
+    lia.
+    exploit (two_p_gt_ZERO (N + l)). lia. lia.
   assert (0 <= m * n - two_p (N + l) * q).
     apply Zmult_le_reg_r with d. auto.
-    replace (0 * d) with 0 by ring.  rewrite H2. omega.
+    replace (0 * d) with 0 by ring.  rewrite H2. lia.
   assert (m * n - two_p (N + l) * q < two_p (N + l)).
-    apply Zmult_lt_reg_r with d. omega.
+    apply Zmult_lt_reg_r with d. lia.
     rewrite H2.
     apply Z.le_lt_trans with (two_p (N + l) * d - two_p l).
-    omega.
-    exploit (two_p_gt_ZERO l). omega. omega.
+    lia.
+    exploit (two_p_gt_ZERO l). lia. lia.
   symmetry. apply Zdiv_unique with (m * n - two_p (N + l) * q).
-  ring. omega.
+  ring. lia.
 Qed.
 
 Lemma Zdiv_unique_2:
   forall x y q, y > 0 -> 0 < y * q - x <= y -> Z.div x y = q - 1.
 Proof.
   intros. apply Zdiv_unique with (x - (q - 1) * y). ring.
-  replace ((q - 1) * y) with (y * q - y) by ring. omega.
+  replace ((q - 1) * y) with (y * q - y) by ring. lia.
 Qed.
 
 Lemma Zdiv_mul_opp:
@@ -111,42 +111,42 @@ Proof.
   set (r := n mod d).
   intro EUCL.
   assert (0 <= r <= d - 1).
-    unfold r. generalize (Z_mod_lt n d d_pos). omega.
+    unfold r. generalize (Z_mod_lt n d d_pos). lia.
   assert (0 <= m).
     apply Zmult_le_0_reg_r with d. auto.
-    exploit (two_p_gt_ZERO (N + l)). omega. omega.
+    exploit (two_p_gt_ZERO (N + l)). lia. lia.
   cut (Z.div (- (m * n)) (two_p (N + l)) = -q - 1).
-    omega.
+    lia.
   apply Zdiv_unique_2.
-  apply two_p_gt_ZERO. omega.
+  apply two_p_gt_ZERO. lia.
   replace (two_p (N + l) * - q - - (m * n))
      with (m * n - two_p (N + l) * q)
        by ring.
   set (k := m * d - two_p (N + l)).
   assert (0 < k <= two_p l).
-    unfold k; omega.
+    unfold k; lia.
   assert ((m * n - two_p (N + l) * q) * d = k * n + two_p (N + l) * r).
     unfold k. rewrite EUCL. ring.
   split.
-  apply Zmult_lt_reg_r with d. omega.
-  replace (0 * d) with 0 by omega.
+  apply Zmult_lt_reg_r with d. lia.
+  replace (0 * d) with 0 by lia.
   rewrite H2.
-  assert (0 < k * n). apply Z.mul_pos_pos; omega.
+  assert (0 < k * n). apply Z.mul_pos_pos; lia.
   assert (0 <= two_p (N + l) * r).
-    apply Z.mul_nonneg_nonneg. exploit (two_p_gt_ZERO (N + l)); omega. omega.
-  omega.
-  apply Zmult_le_reg_r with d. omega.
+    apply Z.mul_nonneg_nonneg. exploit (two_p_gt_ZERO (N + l)); lia. lia.
+  lia.
+  apply Zmult_le_reg_r with d. lia.
   rewrite H2.
   assert (k * n <= two_p (N + l)).
-    rewrite Z.add_comm. rewrite two_p_is_exp; try omega.
-    apply Z.le_trans with (two_p l * n). apply Z.mul_le_mono_nonneg_r; omega.
-    apply Z.mul_le_mono_nonneg_l. omega. exploit (two_p_gt_ZERO l). omega. omega.
+    rewrite Z.add_comm. rewrite two_p_is_exp; try lia.
+    apply Z.le_trans with (two_p l * n). apply Z.mul_le_mono_nonneg_r; lia.
+    apply Z.mul_le_mono_nonneg_l. lia. exploit (two_p_gt_ZERO l). lia. lia.
   assert (two_p (N + l) * r <= two_p (N + l) * d - two_p (N + l)).
     replace (two_p (N + l) * d - two_p (N + l))
        with (two_p (N + l) * (d - 1))
          by ring.
-    apply Z.mul_le_mono_nonneg_l. exploit (two_p_gt_ZERO (N + l)). omega. omega. omega.
-  omega.
+    apply Z.mul_le_mono_nonneg_l. exploit (two_p_gt_ZERO (N + l)). lia. lia. lia.
+  lia.
 Qed.
 
 (** This is theorem 5.1 from Granlund and Montgomery, PLDI 1994. *)
@@ -160,13 +160,13 @@ Lemma Zquot_mul:
   Z.quot n d = Z.div (m * n) (two_p (N + l)) + (if zlt n 0 then 1 else 0).
 Proof.
   intros. destruct (zlt n 0).
-  exploit (Zdiv_mul_opp m l H H0 (-n)). omega.
+  exploit (Zdiv_mul_opp m l H H0 (-n)). lia.
   replace (- - n) with n by ring.
   replace (Z.quot n d) with (- Z.quot (-n) d).
-  rewrite Zquot_Zdiv_pos by omega. omega.
-  rewrite Z.quot_opp_l by omega. ring.
-  rewrite Z.add_0_r. rewrite Zquot_Zdiv_pos by omega.
-  apply Zdiv_mul_pos; omega.
+  rewrite Zquot_Zdiv_pos by lia. lia.
+  rewrite Z.quot_opp_l by lia. ring.
+  rewrite Z.add_0_r. rewrite Zquot_Zdiv_pos by lia.
+  apply Zdiv_mul_pos; lia.
 Qed.
 
 End Z_DIV_MUL.
@@ -195,11 +195,11 @@ Proof with (try discriminate).
   destruct (zlt p1 32)...
   intros EQ; inv EQ.
   split. auto. split. auto. intros.
-  replace (32 + p') with (31 + (p' + 1)) by omega.
-  apply Zquot_mul; try omega.
-  replace (31 + (p' + 1)) with (32 + p') by omega. omega.
+  replace (32 + p') with (31 + (p' + 1)) by lia.
+  apply Zquot_mul; try lia.
+  replace (31 + (p' + 1)) with (32 + p') by lia. lia.
   change (Int.min_signed <= n < Int.half_modulus).
-  unfold Int.max_signed in H. omega.
+  unfold Int.max_signed in H. lia.
 Qed.
 
 Lemma divu_mul_params_sound:
@@ -224,7 +224,7 @@ Proof with (try discriminate).
   destruct (zlt p1 32)...
   intros EQ; inv EQ.
   split. auto. split. auto. intros.
-  apply Zdiv_mul_pos; try omega. assumption.
+  apply Zdiv_mul_pos; try lia. assumption.
 Qed.
 
 Lemma divs_mul_shift_gen:
@@ -238,25 +238,25 @@ Proof.
   exploit divs_mul_params_sound; eauto. intros (A & B & C).
   split. auto. split. auto.
   unfold Int.divs. fold n; fold d. rewrite C by (apply Int.signed_range).
-  rewrite two_p_is_exp by omega. rewrite <- Zdiv_Zdiv.
+  rewrite two_p_is_exp by lia. rewrite <- Zdiv_Zdiv.
   rewrite Int.shru_lt_zero. unfold Int.add. apply Int.eqm_samerepr. apply Int.eqm_add.
   rewrite Int.shr_div_two_p. apply Int.eqm_unsigned_repr_r. apply Int.eqm_refl2.
   rewrite Int.unsigned_repr. f_equal.
   rewrite Int.signed_repr. rewrite Int.modulus_power. f_equal. ring.
   cut (Int.min_signed <= n * m / Int.modulus < Int.half_modulus).
-  unfold Int.max_signed; omega.
-  apply Zdiv_interval_1. generalize Int.min_signed_neg; omega. apply Int.half_modulus_pos.
+  unfold Int.max_signed; lia.
+  apply Zdiv_interval_1. generalize Int.min_signed_neg; lia. apply Int.half_modulus_pos.
   apply Int.modulus_pos.
   split. apply Z.le_trans with (Int.min_signed * m). 
-  apply Z.mul_le_mono_nonpos_l. generalize Int.min_signed_neg; omega. omega.
-  apply Z.mul_le_mono_nonneg_r. omega. unfold n; generalize (Int.signed_range x); tauto.
+  apply Z.mul_le_mono_nonpos_l. generalize Int.min_signed_neg; lia. lia.
+  apply Z.mul_le_mono_nonneg_r. lia. unfold n; generalize (Int.signed_range x); tauto.
   apply Z.le_lt_trans with (Int.half_modulus * m).
-  apply Z.mul_le_mono_nonneg_r. tauto. generalize (Int.signed_range x); unfold n, Int.max_signed; omega.
-  apply Zmult_lt_compat_l. generalize Int.half_modulus_pos; omega. tauto.
-  assert (32 < Int.max_unsigned) by (compute; auto). omega.
+  apply Z.mul_le_mono_nonneg_r. tauto. generalize (Int.signed_range x); unfold n, Int.max_signed; lia.
+  apply Zmult_lt_compat_l. generalize Int.half_modulus_pos; lia. tauto.
+  assert (32 < Int.max_unsigned) by (compute; auto). lia.
   unfold Int.lt; fold n. rewrite Int.signed_zero. destruct (zlt n 0); apply Int.eqm_unsigned_repr.
-  apply two_p_gt_ZERO. omega.
-  apply two_p_gt_ZERO. omega.
+  apply two_p_gt_ZERO. lia.
+  apply two_p_gt_ZERO. lia.
 Qed.
 
 Theorem divs_mul_shift_1:
@@ -270,7 +270,7 @@ Proof.
   intros. exploit divs_mul_shift_gen; eauto. instantiate (1 := x).
   intros (A & B & C). split. auto. rewrite C.
   unfold Int.mulhs. rewrite Int.signed_repr. auto.
-  generalize Int.min_signed_neg; unfold Int.max_signed; omega.
+  generalize Int.min_signed_neg; unfold Int.max_signed; lia.
 Qed.
 
 Theorem divs_mul_shift_2:
@@ -306,18 +306,18 @@ Proof.
   split. auto.
   rewrite Int.shru_div_two_p. rewrite Int.unsigned_repr.
   unfold Int.divu, Int.mulhu. f_equal. rewrite C by apply Int.unsigned_range.
-  rewrite two_p_is_exp by omega. rewrite <- Zdiv_Zdiv by (apply two_p_gt_ZERO; omega).
+  rewrite two_p_is_exp by lia. rewrite <- Zdiv_Zdiv by (apply two_p_gt_ZERO; lia).
   f_equal. rewrite (Int.unsigned_repr m).
   rewrite Int.unsigned_repr. f_equal. ring.
   cut (0 <= Int.unsigned x * m / Int.modulus < Int.modulus).
-  unfold Int.max_unsigned; omega.
-  apply Zdiv_interval_1. omega. compute; auto. compute; auto.
-  split. simpl. apply Z.mul_nonneg_nonneg. generalize (Int.unsigned_range x); omega. omega.
+  unfold Int.max_unsigned; lia.
+  apply Zdiv_interval_1. lia. compute; auto. compute; auto.
+  split. simpl. apply Z.mul_nonneg_nonneg. generalize (Int.unsigned_range x); lia. lia.
   apply Z.le_lt_trans with (Int.modulus * m).
-  apply Zmult_le_compat_r. generalize (Int.unsigned_range x); omega. omega.
-  apply Zmult_lt_compat_l. compute; auto. omega.
-  unfold Int.max_unsigned; omega.
-  assert (32 < Int.max_unsigned) by (compute; auto). omega.
+  apply Zmult_le_compat_r. generalize (Int.unsigned_range x); lia. lia.
+  apply Zmult_lt_compat_l. compute; auto. lia.
+  unfold Int.max_unsigned; lia.
+  assert (32 < Int.max_unsigned) by (compute; auto). lia.
 Qed.
 
 (** Same, for 64-bit integers *)
@@ -344,11 +344,11 @@ Proof with (try discriminate).
   destruct (zlt p1 64)...
   intros EQ; inv EQ.
   split. auto. split. auto. intros.
-  replace (64 + p') with (63 + (p' + 1)) by omega.
-  apply Zquot_mul; try omega.
-  replace (63 + (p' + 1)) with (64 + p') by omega. omega.
+  replace (64 + p') with (63 + (p' + 1)) by lia.
+  apply Zquot_mul; try lia.
+  replace (63 + (p' + 1)) with (64 + p') by lia. lia.
   change (Int64.min_signed <= n < Int64.half_modulus).
-  unfold Int64.max_signed in H. omega.
+  unfold Int64.max_signed in H. lia.
 Qed.
 
 Lemma divlu_mul_params_sound:
@@ -373,13 +373,13 @@ Proof with (try discriminate).
   destruct (zlt p1 64)...
   intros EQ; inv EQ.
   split. auto. split. auto. intros.
-  apply Zdiv_mul_pos; try omega. assumption.
+  apply Zdiv_mul_pos; try lia. assumption.
 Qed.
 
 Remark int64_shr'_div_two_p:
   forall x y, Int64.shr' x y = Int64.repr (Int64.signed x / two_p (Int.unsigned y)).
 Proof.
-  intros; unfold Int64.shr'. rewrite Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); omega.
+  intros; unfold Int64.shr'. rewrite Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); lia.
 Qed.
 
 Lemma divls_mul_shift_gen:
@@ -393,25 +393,25 @@ Proof.
   exploit divls_mul_params_sound; eauto. intros (A & B & C).
   split. auto. split. auto.
   unfold Int64.divs. fold n; fold d. rewrite C by (apply Int64.signed_range).
-  rewrite two_p_is_exp by omega. rewrite <- Zdiv_Zdiv.
+  rewrite two_p_is_exp by lia. rewrite <- Zdiv_Zdiv.
   rewrite Int64.shru_lt_zero. unfold Int64.add. apply Int64.eqm_samerepr. apply Int64.eqm_add.
   rewrite int64_shr'_div_two_p. apply Int64.eqm_unsigned_repr_r. apply Int64.eqm_refl2.
   rewrite Int.unsigned_repr. f_equal.
   rewrite Int64.signed_repr. rewrite Int64.modulus_power. f_equal. ring.
   cut (Int64.min_signed <= n * m / Int64.modulus < Int64.half_modulus).
-  unfold Int64.max_signed; omega.
-  apply Zdiv_interval_1. generalize Int64.min_signed_neg; omega. apply Int64.half_modulus_pos.
+  unfold Int64.max_signed; lia.
+  apply Zdiv_interval_1. generalize Int64.min_signed_neg; lia. apply Int64.half_modulus_pos.
   apply Int64.modulus_pos.
   split. apply Z.le_trans with (Int64.min_signed * m).
-  apply Z.mul_le_mono_nonpos_l. generalize Int64.min_signed_neg; omega. omega.
+  apply Z.mul_le_mono_nonpos_l. generalize Int64.min_signed_neg; lia. lia.
   apply Z.mul_le_mono_nonneg_r. tauto. unfold n; generalize (Int64.signed_range x); tauto.
   apply Z.le_lt_trans with (Int64.half_modulus * m).
-  apply Zmult_le_compat_r. generalize (Int64.signed_range x); unfold n, Int64.max_signed; omega. tauto.
-  apply Zmult_lt_compat_l. generalize Int64.half_modulus_pos; omega. tauto.
-  assert (64 < Int.max_unsigned) by (compute; auto). omega.
+  apply Zmult_le_compat_r. generalize (Int64.signed_range x); unfold n, Int64.max_signed; lia. tauto.
+  apply Zmult_lt_compat_l. generalize Int64.half_modulus_pos; lia. tauto.
+  assert (64 < Int.max_unsigned) by (compute; auto). lia.
   unfold Int64.lt; fold n. rewrite Int64.signed_zero. destruct (zlt n 0); apply Int64.eqm_unsigned_repr.
-  apply two_p_gt_ZERO. omega.
-  apply two_p_gt_ZERO. omega.
+  apply two_p_gt_ZERO. lia.
+  apply two_p_gt_ZERO. lia.
 Qed.
 
 Theorem divls_mul_shift_1:
@@ -425,7 +425,7 @@ Proof.
   intros. exploit divls_mul_shift_gen; eauto. instantiate (1 := x).
   intros (A & B & C). split. auto. rewrite C.
   unfold Int64.mulhs. rewrite Int64.signed_repr. auto.
-  generalize Int64.min_signed_neg; unfold Int64.max_signed; omega.
+  generalize Int64.min_signed_neg; unfold Int64.max_signed; lia.
 Qed.
 
 Theorem divls_mul_shift_2:
@@ -454,7 +454,7 @@ Qed.
 Remark int64_shru'_div_two_p:
   forall x y, Int64.shru' x y = Int64.repr (Int64.unsigned x / two_p (Int.unsigned y)).
 Proof.
-  intros; unfold Int64.shru'. rewrite Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); omega.
+  intros; unfold Int64.shru'. rewrite Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); lia.
 Qed.
 
 Theorem divlu_mul_shift:
@@ -467,18 +467,18 @@ Proof.
   split. auto.
   rewrite int64_shru'_div_two_p. rewrite Int.unsigned_repr.
   unfold Int64.divu, Int64.mulhu. f_equal. rewrite C by apply Int64.unsigned_range.
-  rewrite two_p_is_exp by omega. rewrite <- Zdiv_Zdiv by (apply two_p_gt_ZERO; omega).
+  rewrite two_p_is_exp by lia. rewrite <- Zdiv_Zdiv by (apply two_p_gt_ZERO; lia).
   f_equal. rewrite (Int64.unsigned_repr m).
   rewrite Int64.unsigned_repr. f_equal. ring.
   cut (0 <= Int64.unsigned x * m / Int64.modulus < Int64.modulus).
-  unfold Int64.max_unsigned; omega.
-  apply Zdiv_interval_1. omega. compute; auto. compute; auto.
-  split. simpl. apply Z.mul_nonneg_nonneg. generalize (Int64.unsigned_range x); omega. omega.
+  unfold Int64.max_unsigned; lia.
+  apply Zdiv_interval_1. lia. compute; auto. compute; auto.
+  split. simpl. apply Z.mul_nonneg_nonneg. generalize (Int64.unsigned_range x); lia. lia.
   apply Z.le_lt_trans with (Int64.modulus * m).
-  apply Zmult_le_compat_r. generalize (Int64.unsigned_range x); omega. omega.
-  apply Zmult_lt_compat_l. compute; auto. omega.
-  unfold Int64.max_unsigned; omega.
-  assert (64 < Int.max_unsigned) by (compute; auto). omega.
+  apply Zmult_le_compat_r. generalize (Int64.unsigned_range x); lia. lia.
+  apply Zmult_lt_compat_l. compute; auto. lia.
+  unfold Int64.max_unsigned; lia.
+  assert (64 < Int.max_unsigned) by (compute; auto). lia.
 Qed.
 
 (** * Correctness of the smart constructors for division and modulus *)
@@ -516,7 +516,7 @@ Proof.
   replace (Int.ltu (Int.repr p) Int.iwordsize) with true in Q.
   inv Q. rewrite B. auto.
   unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true; auto. tauto.
-  assert (32 < Int.max_unsigned) by (compute; auto). omega.
+  assert (32 < Int.max_unsigned) by (compute; auto). lia.
 Qed.
 
 Theorem eval_divuimm:
@@ -631,7 +631,7 @@ Proof.
   simpl in LD. inv LD.
   assert (RANGE: 0 <= p < 32 -> Int.ltu (Int.repr p) Int.iwordsize = true).
   { intros. unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true by tauto. auto.
-    assert (32 < Int.max_unsigned) by (compute; auto). omega. }
+    assert (32 < Int.max_unsigned) by (compute; auto). lia. }
   destruct (zlt M Int.half_modulus).
 - exploit (divs_mul_shift_1 x); eauto. intros [A B].
   exploit eval_shrimm. eexact X. instantiate (1 := Int.repr p). intros [v1 [Z LD]].
@@ -769,7 +769,7 @@ Proof.
   simpl in B1; inv B1. simpl in B2. replace (Int.ltu (Int.repr p) Int64.iwordsize') with true in B2. inv B2.
   rewrite B. assumption.
   unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true; auto. tauto.
-  assert (64 < Int.max_unsigned) by (compute; auto). omega.
+  assert (64 < Int.max_unsigned) by (compute; auto). lia.
 Qed.
 
 Theorem eval_divlu:
@@ -848,10 +848,10 @@ Proof.
   exploit eval_addl. auto. eexact A5. eexact A3. intros (v6 & A6 & B6).
   assert (RANGE: forall x, 0 <= x < 64 -> Int.ltu (Int.repr x) Int64.iwordsize' = true).
   { intros. unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true by tauto. auto.
-    assert (64 < Int.max_unsigned) by (compute; auto). omega. }
+    assert (64 < Int.max_unsigned) by (compute; auto). lia. }
   simpl in B1; inv B1.
   simpl in B2; inv B2.
-  simpl in B3; rewrite RANGE in B3 by omega; inv B3.
+  simpl in B3; rewrite RANGE in B3 by lia; inv B3.
   destruct (zlt M Int64.half_modulus).
 - exploit (divls_mul_shift_1 x); eauto. intros [A B].
   simpl in B5; rewrite RANGE in B5 by auto; inv B5.
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 8f3f5f00..e737ba4b 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -533,7 +533,7 @@ Lemma sel_switch_correct:
      (XElet arg (sel_switch make_cmp_eq make_cmp_ltu make_sub make_to_int O t))
      (switch_target i dfl cases).
 Proof.
-  intros. exploit validate_switch_correct; eauto. omega. intros [A B].
+  intros. exploit validate_switch_correct; eauto. lia. intros [A B].
   econstructor. eauto. eapply sel_switch_correct_rec; eauto.
 Qed.
 
@@ -566,7 +566,7 @@ Proof.
   inv R. unfold Val.cmp in B. simpl in B. revert B.
   predSpec Int.eq Int.eq_spec n0 (Int.repr n); intros B; inv B.
   rewrite Int.unsigned_repr. unfold proj_sumbool; rewrite zeq_true; auto.
-  unfold Int.max_unsigned; omega.
+  unfold Int.max_unsigned; lia.
   unfold proj_sumbool; rewrite zeq_false; auto.
   red; intros; elim H1. rewrite <- (Int.repr_unsigned n0). congruence.
 - intros until n; intros EVAL R RANGE.
@@ -575,7 +575,7 @@ Proof.
   inv R. unfold Val.cmpu in B. simpl in B.
   unfold Int.ltu in B. rewrite Int.unsigned_repr in B.
   destruct (zlt (Int.unsigned n0) n); inv B; auto.
-  unfold Int.max_unsigned; omega.
+  unfold Int.max_unsigned; lia.
 - intros until n; intros EVAL R RANGE.
   exploit eval_sub. eexact EVAL. apply (INTCONST (Int.repr n)). intros (vb & A & B).
   inv R. simpl in B. inv B. econstructor; split; eauto.
@@ -583,7 +583,7 @@ Proof.
      with (Int.unsigned (Int.sub n0 (Int.repr n))).
   constructor.
   unfold Int.sub. rewrite Int.unsigned_repr_eq. f_equal. f_equal.
-  apply Int.unsigned_repr. unfold Int.max_unsigned; omega.
+  apply Int.unsigned_repr. unfold Int.max_unsigned; lia.
 - intros until i0; intros EVAL R. exists v; split; auto.
   inv R. rewrite Z.mod_small by (apply Int.unsigned_range). constructor.
 - constructor.
@@ -601,12 +601,12 @@ Proof.
   eapply eval_cmpl. eexact EVAL. apply eval_longconst with (n := Int64.repr n).
   inv R. unfold Val.cmpl. simpl. f_equal; f_equal. unfold Int64.eq.
   rewrite Int64.unsigned_repr. destruct (zeq (Int64.unsigned n0) n); auto.
-  unfold Int64.max_unsigned; omega.
+  unfold Int64.max_unsigned; lia.
 - intros until n; intros EVAL R RANGE.
   eapply eval_cmplu; auto. eexact EVAL. apply eval_longconst with (n := Int64.repr n).
   inv R. unfold Val.cmplu. simpl. f_equal; f_equal. unfold Int64.ltu.
   rewrite Int64.unsigned_repr. destruct (zlt (Int64.unsigned n0) n); auto.
-  unfold Int64.max_unsigned; omega.
+  unfold Int64.max_unsigned; lia.
 - intros until n; intros EVAL R RANGE.
   exploit eval_subl; auto; try apply HF'. eexact EVAL. apply eval_longconst with (n := Int64.repr n).
   intros (vb & A & B).
@@ -615,7 +615,7 @@ Proof.
      with (Int64.unsigned (Int64.sub n0 (Int64.repr n))).
   constructor.
   unfold Int64.sub. rewrite Int64.unsigned_repr_eq. f_equal. f_equal.
-  apply Int64.unsigned_repr. unfold Int64.max_unsigned; omega.
+  apply Int64.unsigned_repr. unfold Int64.max_unsigned; lia.
 - intros until i0; intros EVAL R.
   exploit eval_lowlong. eexact EVAL. intros (vb & A & B).
   inv R. simpl in B. inv B. econstructor; split; eauto.
@@ -1299,7 +1299,7 @@ Proof.
   eapply match_cont_call with (cunit := cunit) (hf := hf); eauto.
 + (* turned into Sbuiltin *)
   intros EQ. subst fd.
-  right; left; split. simpl; omega. split; auto. econstructor; eauto.
+  right; left; split. simpl; lia. split; auto. econstructor; eauto.
 - (* Stailcall *)
   exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]].
   erewrite <- stackspace_function_translated in P by eauto.
@@ -1417,7 +1417,7 @@ Proof.
   apply plus_one; econstructor.
   econstructor; eauto. destruct optid; simpl; auto. apply set_var_lessdef; auto.
 - (* return of an external call turned into a Sbuiltin *)
-  right; left; split. simpl; omega. split. auto. econstructor; eauto.
+  right; left; split. simpl; lia. split. auto. econstructor; eauto.
 Qed.
 
 Lemma sel_initial_states:
diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v
index c8e3b94c..e45c3a34 100644
--- a/backend/SplitLongproof.v
+++ b/backend/SplitLongproof.v
@@ -318,7 +318,7 @@ Proof.
   fold (Int.testbit i i0).
   destruct (zlt i0 Int.zwordsize).
   auto.
-  rewrite Int.bits_zero. rewrite Int.bits_above by omega. auto.
+  rewrite Int.bits_zero. rewrite Int.bits_above by lia. auto.
 Qed.
 
 Theorem eval_longofint: unary_constructor_sound longofint Val.longofint.
@@ -335,13 +335,13 @@ Proof.
   apply Int64.same_bits_eq; intros.
   rewrite Int64.testbit_repr by auto.
   rewrite Int64.bits_ofwords by auto.
-  rewrite Int.bits_signed by omega.
+  rewrite Int.bits_signed by lia.
   destruct (zlt i0 Int.zwordsize).
   auto.
   assert (Int64.zwordsize = 2 * Int.zwordsize) by reflexivity.
-  rewrite Int.bits_shr by omega.
+  rewrite Int.bits_shr by lia.
   change (Int.unsigned (Int.repr 31)) with (Int.zwordsize - 1).
-  f_equal. destruct (zlt (i0 - Int.zwordsize + (Int.zwordsize - 1)) Int.zwordsize); omega.
+  f_equal. destruct (zlt (i0 - Int.zwordsize + (Int.zwordsize - 1)) Int.zwordsize); lia.
 Qed.
 
 Theorem eval_negl: unary_constructor_sound negl Val.negl.
@@ -528,24 +528,24 @@ Proof.
   { red; intros. elim H. rewrite <- (Int.repr_unsigned n). rewrite H0. auto. }
   destruct (Int.ltu n Int.iwordsize) eqn:LT.
   exploit Int.ltu_iwordsize_inv; eauto. intros RANGE.
-  assert (0 <= Int.zwordsize - Int.unsigned n < Int.zwordsize) by omega.
+  assert (0 <= Int.zwordsize - Int.unsigned n < Int.zwordsize) by lia.
   apply A1. auto. auto.
   unfold Int.ltu, Int.sub. rewrite Int.unsigned_repr_wordsize.
-  rewrite Int.unsigned_repr. rewrite zlt_true; auto. omega.
-  generalize Int.wordsize_max_unsigned; omega.
+  rewrite Int.unsigned_repr. rewrite zlt_true; auto. lia.
+  generalize Int.wordsize_max_unsigned; lia.
   unfold Int.ltu. rewrite zlt_true; auto.
   change (Int.unsigned Int64.iwordsize') with 64.
-  change Int.zwordsize with 32 in RANGE. omega.
+  change Int.zwordsize with 32 in RANGE. lia.
   destruct (Int.ltu n Int64.iwordsize') eqn:LT'.
   exploit Int.ltu_inv; eauto.
   change (Int.unsigned Int64.iwordsize') with (Int.zwordsize * 2).
   intros RANGE.
   assert (Int.zwordsize <= Int.unsigned n).
     unfold Int.ltu in LT. rewrite Int.unsigned_repr_wordsize in LT.
-    destruct (zlt (Int.unsigned n) Int.zwordsize). discriminate. omega.
+    destruct (zlt (Int.unsigned n) Int.zwordsize). discriminate. lia.
   apply A2. tauto. unfold Int.ltu, Int.sub. rewrite Int.unsigned_repr_wordsize.
-  rewrite Int.unsigned_repr. rewrite zlt_true; auto. omega.
-  generalize Int.wordsize_max_unsigned; omega.
+  rewrite Int.unsigned_repr. rewrite zlt_true; auto. lia.
+  generalize Int.wordsize_max_unsigned; lia.
   auto.
 Qed.
 
@@ -901,19 +901,19 @@ Proof.
   rewrite Int.bits_zero. rewrite Int.bits_or by auto.
   symmetry. apply orb_false_intro.
   transitivity (Int64.testbit (Int64.ofwords h l) (i + Int.zwordsize)).
-  rewrite Int64.bits_ofwords by omega. rewrite zlt_false by omega. f_equal; omega.
+  rewrite Int64.bits_ofwords by lia. rewrite zlt_false by lia. f_equal; lia.
   rewrite H0. apply Int64.bits_zero.
   transitivity (Int64.testbit (Int64.ofwords h l) i).
-  rewrite Int64.bits_ofwords by omega. rewrite zlt_true by omega. auto.
+  rewrite Int64.bits_ofwords by lia. rewrite zlt_true by lia. auto.
   rewrite H0. apply Int64.bits_zero.
   symmetry. apply Int.eq_false. red; intros; elim H0.
   apply Int64.same_bits_eq; intros.
   rewrite Int64.bits_zero. rewrite Int64.bits_ofwords by auto.
   destruct (zlt i Int.zwordsize).
   assert (Int.testbit (Int.or h l) i = false) by (rewrite H1; apply Int.bits_zero).
-  rewrite Int.bits_or in H3 by omega. exploit orb_false_elim; eauto. tauto.
+  rewrite Int.bits_or in H3 by lia. exploit orb_false_elim; eauto. tauto.
   assert (Int.testbit (Int.or h l) (i - Int.zwordsize) = false) by (rewrite H1; apply Int.bits_zero).
-  rewrite Int.bits_or in H3 by omega. exploit orb_false_elim; eauto. tauto.
+  rewrite Int.bits_or in H3 by lia. exploit orb_false_elim; eauto. tauto.
 Qed.
 
 Lemma eval_cmpl_eq_zero:
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index a5aa5177..6d793961 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -58,7 +58,7 @@ Lemma slot_outgoing_argument_valid:
 Proof.
   intros. exploit loc_arguments_acceptable_2; eauto. intros [A B].
   unfold slot_valid. unfold proj_sumbool.
-  rewrite zle_true by omega.
+  rewrite zle_true by lia.
   rewrite pred_dec_true by auto.
   auto.
 Qed.
@@ -126,7 +126,7 @@ Proof.
   destruct (wt_function f); simpl negb.
   destruct (zlt Ptrofs.max_unsigned (fe_size (make_env (function_bounds f)))).
   intros; discriminate.
-  intros. unfold fe. unfold b. omega.
+  intros. unfold fe. unfold b. lia.
   intros; discriminate.
 Qed.
 
@@ -200,7 +200,7 @@ Next Obligation.
 - exploit H4; eauto. intros (v & A & B). exists v; split; auto.
   eapply Mem.load_unchanged_on; eauto.
   simpl; intros. rewrite size_type_chunk, typesize_typesize in H8.
-  split; auto. omega.
+  split; auto. lia.
 Qed.
 Next Obligation.
   eauto with mem.
@@ -215,7 +215,7 @@ Remark valid_access_location:
 Proof.
   intros; split.
 - red; intros. apply Mem.perm_implies with Freeable; auto with mem.
-  apply H0. rewrite size_type_chunk, typesize_typesize in H4. omega.
+  apply H0. rewrite size_type_chunk, typesize_typesize in H4. lia.
 - rewrite align_type_chunk. apply Z.divide_add_r.
   apply Z.divide_trans with 8; auto.
   exists (8 / (4 * typealign ty)); destruct ty; reflexivity.
@@ -233,7 +233,7 @@ Proof.
   intros. destruct H as (D & E & F & G & H).
   exploit H; eauto. intros (v & U & V). exists v; split; auto.
   unfold load_stack; simpl. rewrite Ptrofs.add_zero_l, Ptrofs.unsigned_repr; auto.
-  unfold Ptrofs.max_unsigned. generalize (typesize_pos ty). omega.
+  unfold Ptrofs.max_unsigned. generalize (typesize_pos ty). lia.
 Qed.
 
 Lemma set_location:
@@ -252,19 +252,19 @@ Proof.
   { red; intros; eauto with mem. }
   exists m'; split.
 - unfold store_stack; simpl. rewrite Ptrofs.add_zero_l, Ptrofs.unsigned_repr; eauto.
-  unfold Ptrofs.max_unsigned. generalize (typesize_pos ty). omega.
+  unfold Ptrofs.max_unsigned. generalize (typesize_pos ty). lia.
 - simpl. intuition auto.
 + unfold Locmap.set.
   destruct (Loc.eq (S sl ofs ty) (S sl ofs0 ty0)); [|destruct (Loc.diff_dec (S sl ofs ty) (S sl ofs0 ty0))].
 * (* same location *)
   inv e. rename ofs0 into ofs. rename ty0 into ty.
   exists (Val.load_result (chunk_of_type ty) v'); split.
-  eapply Mem.load_store_similar_2; eauto. omega.
+  eapply Mem.load_store_similar_2; eauto. lia.
   apply Val.load_result_inject; auto.
 * (* different locations *)
   exploit H; eauto. intros (v0 & X & Y). exists v0; split; auto.
   rewrite <- X; eapply Mem.load_store_other; eauto.
-  destruct d. congruence. right. rewrite ! size_type_chunk, ! typesize_typesize. omega.
+  destruct d. congruence. right. rewrite ! size_type_chunk, ! typesize_typesize. lia.
 * (* overlapping locations *)
   destruct (Mem.valid_access_load m' (chunk_of_type ty0) sp (pos + 4 * ofs0)) as [v'' LOAD].
   apply Mem.valid_access_implies with Writable; auto with mem.
@@ -273,7 +273,7 @@ Proof.
 + apply (m_invar P) with m; auto.
   eapply Mem.store_unchanged_on; eauto.
   intros i; rewrite size_type_chunk, typesize_typesize. intros; red; intros.
-  eelim C; eauto. simpl. split; auto. omega.
+  eelim C; eauto. simpl. split; auto. lia.
 Qed.
 
 Lemma initial_locations:
@@ -933,8 +933,8 @@ Local Opaque mreg_type.
   { unfold pos1. apply Z.divide_trans with sz.
     unfold sz; rewrite <- size_type_chunk. apply align_size_chunk_divides.
     apply align_divides; auto. }
-  apply range_drop_left with (mid := pos1) in SEP; [ | omega ].
-  apply range_split with (mid := pos1 + sz) in SEP; [ | omega ].
+  apply range_drop_left with (mid := pos1) in SEP; [ | lia ].
+  apply range_split with (mid := pos1 + sz) in SEP; [ | lia ].
   unfold sz at 1 in SEP. rewrite <- size_type_chunk in SEP.
   apply range_contains in SEP; auto.
   exploit (contains_set_stack (fun v' => Val.inject j (ls (R r)) v') (rs r)).
@@ -1073,7 +1073,7 @@ Local Opaque b fe.
   instantiate (1 := fe_stack_data fe). tauto.
   reflexivity.
   instantiate (1 := fe_stack_data fe + bound_stack_data b). rewrite Z.max_comm. reflexivity.
-  generalize (bound_stack_data_pos b) size_no_overflow; omega.
+  generalize (bound_stack_data_pos b) size_no_overflow; lia.
   tauto.
   tauto.
   clear SEP. intros (j' & SEP & INCR & SAME).
@@ -1607,7 +1607,7 @@ Proof.
 + simpl in SEP. unfold parent_sp.
   assert (slot_valid f Outgoing pos ty = true).
   { destruct H0. unfold slot_valid, proj_sumbool.
-    rewrite zle_true by omega. rewrite pred_dec_true by auto. reflexivity. }
+    rewrite zle_true by lia. rewrite pred_dec_true by auto. reflexivity. }
   assert (slot_within_bounds (function_bounds f) Outgoing pos ty) by eauto.
   exploit frame_get_outgoing; eauto. intros (v & A & B).
   exists v; split.
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
index 79a5c1cf..80a68327 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -47,11 +47,11 @@ Proof.
   intro f.
   assert (forall n pc, (return_measure_rec n f pc <= n)%nat).
     induction n; intros; simpl.
-    omega.
-    destruct (f!pc); try omega.
-    destruct i; try omega.
-    generalize (IHn n0). omega.
-    generalize (IHn n0). omega.
+    lia.
+    destruct (f!pc); try lia.
+    destruct i; try lia.
+    generalize (IHn n0). lia.
+    generalize (IHn n0). lia.
   intros. unfold return_measure. apply H.
 Qed.
 
@@ -61,11 +61,11 @@ Remark return_measure_rec_incr:
   (return_measure_rec n1 f pc <= return_measure_rec n2 f pc)%nat.
 Proof.
   induction n1; intros; simpl.
-  omega.
-  destruct n2. omegaContradiction. assert (n1 <= n2)%nat by omega.
-  simpl. destruct f!pc; try omega. destruct i; try omega.
-  generalize (IHn1 n2 n H0). omega.
-  generalize (IHn1 n2 n H0). omega.
+  lia.
+  destruct n2. extlia. assert (n1 <= n2)%nat by lia.
+  simpl. destruct f!pc; try lia. destruct i; try lia.
+  generalize (IHn1 n2 n H0). lia.
+  generalize (IHn1 n2 n H0). lia.
 Qed.
 
 Lemma is_return_measure_rec:
@@ -75,13 +75,13 @@ Lemma is_return_measure_rec:
 Proof.
   induction n; simpl; intros.
   congruence.
-  destruct n'. omegaContradiction. simpl.
+  destruct n'. extlia. simpl.
   destruct (fn_code f)!pc; try congruence.
   destruct i; try congruence.
-  decEq. apply IHn with r. auto. omega.
+  decEq. apply IHn with r. auto. lia.
   destruct (is_move_operation o l); try congruence.
   destruct (Reg.eq r r1); try congruence.
-  decEq. apply IHn with r0. auto. omega.
+  decEq. apply IHn with r0. auto. lia.
 Qed.
 
 (** ** Relational characterization of the code transformation *)
@@ -117,22 +117,22 @@ Proof.
   generalize H. simpl.
   caseEq ((fn_code f)!pc); try congruence.
   intro i. caseEq i; try congruence.
-  intros s; intros. eapply is_return_nop; eauto. eapply IHn; eauto. omega.
+  intros s; intros. eapply is_return_nop; eauto. eapply IHn; eauto. lia.
   unfold return_measure.
   rewrite <- (is_return_measure_rec f (S n) niter pc rret); auto.
   rewrite <- (is_return_measure_rec f n niter s rret); auto.
-  simpl. rewrite H2. omega. omega.
+  simpl. rewrite H2. lia. lia.
 
   intros op args dst s EQ1 EQ2.
   caseEq (is_move_operation op args); try congruence.
   intros src IMO. destruct (Reg.eq rret src); try congruence.
   subst rret. intro.
   exploit is_move_operation_correct; eauto. intros [A B]. subst.
-  eapply is_return_move; eauto. eapply IHn; eauto. omega.
+  eapply is_return_move; eauto. eapply IHn; eauto. lia.
   unfold return_measure.
   rewrite <- (is_return_measure_rec f (S n) niter pc src); auto.
   rewrite <- (is_return_measure_rec f n niter s dst); auto.
-  simpl. rewrite EQ2. omega. omega.
+  simpl. rewrite EQ2. lia. lia.
 
   intros or EQ1 EQ2. destruct or; intros.
   assert (r = rret). eapply proj_sumbool_true; eauto. subst r.
@@ -407,7 +407,7 @@ Proof.
   eapply exec_Inop; eauto. constructor; auto.
 - (* eliminated nop *)
   assert (s0 = pc') by congruence. subst s0.
-  right. split. simpl. omega. split. auto.
+  right. split. simpl. lia. split. auto.
   econstructor; eauto.
 
 - (* op *)
@@ -421,7 +421,7 @@ Proof.
   econstructor; eauto. apply set_reg_lessdef; auto.
 - (* eliminated move *)
   rewrite H1 in H. clear H1. inv H.
-  right. split. simpl. omega. split. auto.
+  right. split. simpl. lia. split. auto.
   econstructor; eauto. simpl in H0. rewrite PMap.gss. congruence.
 
 - (* load *)
@@ -492,13 +492,13 @@ Proof.
 + (* call turned tailcall *)
   assert ({ m'' | Mem.free m' sp0 0 (fn_stacksize (transf_function f)) = Some m''}).
     apply Mem.range_perm_free. rewrite stacksize_preserved. rewrite H7.
-    red; intros; omegaContradiction.
+    red; intros; extlia.
   destruct X as [m'' FREE].
   left. exists (Callstate s' (transf_fundef fd) (rs'##args) m''); split.
   eapply exec_Itailcall; eauto. apply sig_preserved.
   constructor. eapply match_stackframes_tail; eauto. apply regs_lessdef_regs; auto.
   eapply Mem.free_right_extends; eauto.
-  rewrite stacksize_preserved. rewrite H7. intros. omegaContradiction.
+  rewrite stacksize_preserved. rewrite H7. intros. extlia.
 + (* call that remains a call *)
   left. exists (Callstate (Stackframe res (transf_function f) (Vptr sp0 Ptrofs.zero) pc' rs' :: s')
                           (transf_fundef fd) (rs'##args) m'); split.
@@ -551,22 +551,22 @@ Proof.
 
 - (* eliminated return None *)
   assert (or = None) by congruence. subst or.
-  right. split. simpl. omega. split. auto.
+  right. split. simpl. lia. split. auto.
   constructor. auto.
   simpl. constructor.
   eapply Mem.free_left_extends; eauto.
 
 - (* eliminated return Some *)
   assert (or = Some r) by congruence. subst or.
-  right. split. simpl. omega. split. auto.
+  right. split. simpl. lia. split. auto.
   constructor. auto.
   simpl. auto.
   eapply Mem.free_left_extends; eauto.
 
 - (* internal call *)
   exploit Mem.alloc_extends; eauto.
-    instantiate (1 := 0). omega.
-    instantiate (1 := fn_stacksize f). omega.
+    instantiate (1 := 0). lia.
+    instantiate (1 := fn_stacksize f). lia.
   intros [m'1 [ALLOC EXT]].
   assert (fn_stacksize (transf_function f) = fn_stacksize f /\
           fn_entrypoint (transf_function f) = fn_entrypoint f /\
@@ -596,7 +596,7 @@ Proof.
   right. split. unfold measure. simpl length.
   change (S (length s) * (niter + 2))%nat
    with ((niter + 2) + (length s) * (niter + 2))%nat.
-  generalize (return_measure_bounds (fn_code f) pc). omega.
+  generalize (return_measure_bounds (fn_code f) pc). lia.
   split. auto.
   econstructor; eauto.
   rewrite Regmap.gss. auto.
diff --git a/backend/Tunneling.v b/backend/Tunneling.v
index 269ebb6f..c849ea92 100644
--- a/backend/Tunneling.v
+++ b/backend/Tunneling.v
@@ -34,8 +34,8 @@ Require Import LTL.
   computations or useless moves), therefore there are more
   opportunities for tunneling after allocation than before.
   Symmetrically, prior tunneling helps linearization to produce
-  better code, e.g. by revealing that some [nop] instructions are
-  dead code (as the "nop L3" in the example above).
+  better code, e.g. by revealing that some [branch] instructions are
+  dead code (as the "branch L3" in the example above).
 *)
 
 (** The implementation consists in two passes: the first pass
@@ -51,7 +51,7 @@ Naively, we may define [branch_t f pc] as follows:
   However, this definition can fail to terminate if
   the program can contain loops consisting only of branches, as in
 <<
-     L1: nop L1;
+     L1: branch L1;
 >>
   or
 <<
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index 126b7b87..3bc92f75 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -66,7 +66,7 @@ Local Hint Resolve target_None Z.abs_nonneg: core.
 
 Lemma get_nonneg td pc t d: get td pc = (t, d) -> (0 <= d)%Z.
 Proof.
-  unfold get. destruct (td!_) as [(t0&d0)|]; intros H; inversion H; subst; simpl; omega || auto.
+  unfold get. destruct (td!_) as [(t0&d0)|]; intros H; inversion H; subst; simpl; lia || auto.
 Qed.
 Local Hint Resolve get_nonneg: core.
 
@@ -469,11 +469,10 @@ Proof.
     * econstructor; eauto.
   + (* FT_branch *)
     simpl; right.
-    rewrite EQ; repeat (econstructor; omega || eauto).
+    rewrite EQ; repeat (econstructor; lia || eauto).
   + (* FT_cond *)
     simpl; right.
-    repeat (econstructor; omega || eauto); simpl.
-    apply Nat.max_case; omega.
+    repeat (econstructor; lia || eauto); simpl.
     destruct (peq _ _); try congruence.
 - (* Lop *)
   exploit eval_operation_lessdef. apply reglist_lessdef; eauto. eauto. eauto. 
@@ -568,7 +567,7 @@ Proof.
   eapply exec_Lbranch; eauto.
   fold (branch_target f pc). econstructor; eauto.
 - (* Lbranch (eliminated) *)
-  right; split. simpl. omega. split. auto. constructor; auto.
+  right; split. simpl. lia. split. auto. constructor; auto.
 - (* Lcond (preserved) *)
   simpl; left; destruct (peq _ _) eqn: EQ.
   + econstructor; split.
@@ -583,8 +582,8 @@ Proof.
   destruct (peq _ _) eqn: EQ; try inv H1.
   right; split; simpl. 
   + destruct b.
-    generalize (Nat.le_max_l (bound (branch_target f) pc1) (bound (branch_target f) pc2)); omega.
-    generalize (Nat.le_max_r (bound (branch_target f) pc1) (bound (branch_target f) pc2)); omega.
+    generalize (Nat.le_max_l (bound (branch_target f) pc1) (bound (branch_target f) pc2)); lia.
+    generalize (Nat.le_max_r (bound (branch_target f) pc1) (bound (branch_target f) pc2)); lia.
   + destruct b.
     -- repeat (constructor; auto).
     -- rewrite e; repeat (constructor; auto).
diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v
index 160c0b18..aaacf9d1 100644
--- a/backend/Unusedglobproof.v
+++ b/backend/Unusedglobproof.v
@@ -1012,7 +1012,7 @@ Proof.
   intros. exploit G; eauto. intros [U V].
   assert (Mem.valid_block m sp0) by (eapply Mem.valid_block_inject_1; eauto).
   assert (Mem.valid_block tm tsp) by (eapply Mem.valid_block_inject_2; eauto).
-  unfold Mem.valid_block in *; xomega.
+  unfold Mem.valid_block in *; extlia.
   apply set_res_inject; auto. apply regset_inject_incr with j; auto.
 
 - (* cond *)
@@ -1066,7 +1066,7 @@ Proof.
   apply match_stacks_bound with (Mem.nextblock m) (Mem.nextblock tm).
   apply match_stacks_incr with j; auto.
   intros. exploit G; eauto. intros [P Q].
-  unfold Mem.valid_block in *; xomega.
+  unfold Mem.valid_block in *; extlia.
   eapply external_call_nextblock; eauto.
   eapply external_call_nextblock; eauto.
 
@@ -1093,7 +1093,7 @@ Proof.
   - apply IHl. unfold Genv.add_global, P; simpl. intros LT. apply Plt_succ_inv in LT. destruct LT.
   + rewrite PTree.gso. apply H; auto. apply Plt_ne; auto.
   + rewrite H0. rewrite PTree.gss. exists g1; auto. }
-  apply H. red; simpl; intros. exfalso; xomega.
+  apply H. red; simpl; intros. exfalso; extlia.
 Qed.
 *)
 
@@ -1153,10 +1153,10 @@ Lemma Mem_getN_forall2:
   P (ZMap.get i c1) (ZMap.get i c2).
 Proof.
   induction n; simpl Mem.getN; intros.
-- simpl in H1. omegaContradiction.
+- simpl in H1. extlia.
 - inv H. rewrite Nat2Z.inj_succ in H1. destruct (zeq i p0).
 + congruence.
-+ apply IHn with (p0 + 1); auto. omega. omega.
++ apply IHn with (p0 + 1); auto. lia. lia.
 Qed.
 
 Lemma init_mem_inj_1:
@@ -1173,7 +1173,7 @@ Proof.
 + intros (P2 & Q2 & R2 & S2) (P1 & Q1 & R1 & S1).
   apply Q1 in H0. destruct H0. subst.
   apply Mem.perm_cur. eapply Mem.perm_implies; eauto.
-  apply P2. omega.
+  apply P2. lia.
 - exploit init_meminj_invert; eauto. intros (A & id & B & C).
   subst delta. apply Z.divide_0_r.
 - exploit init_meminj_invert_strong; eauto. intros (A & id & gd & B & C & D & E & F).
@@ -1192,8 +1192,8 @@ Local Transparent Mem.loadbytes.
   rewrite Z.add_0_r.
   apply Mem_getN_forall2 with (p := 0) (n := Z.to_nat (init_data_list_size (gvar_init v))).
   rewrite H3, H4. apply bytes_of_init_inject. auto.
-  omega.
-  rewrite Z2Nat.id by (apply Z.ge_le; apply init_data_list_size_pos). omega.
+  lia.
+  rewrite Z2Nat.id by (apply Z.ge_le; apply init_data_list_size_pos). lia.
 Qed.
 
 Lemma init_mem_inj_2:
@@ -1211,18 +1211,18 @@ Proof.
   exploit init_meminj_invert. eexact H1. intros (A2 & id2 & B2 & C2).
   destruct (ident_eq id1 id2). congruence. left; eapply Genv.global_addresses_distinct; eauto.
 - exploit init_meminj_invert; eauto. intros (A & id & B & C). subst delta.
-  split. omega. generalize (Ptrofs.unsigned_range_2 ofs). omega.
+  split. lia. generalize (Ptrofs.unsigned_range_2 ofs). lia.
 - exploit init_meminj_invert_strong; eauto. intros (A & id & gd & B & C & D & E & F).
   exploit (Genv.init_mem_characterization_gen p); eauto.
   exploit (Genv.init_mem_characterization_gen tp); eauto.
   destruct gd as [f|v].
 + intros (P2 & Q2) (P1 & Q1).
-  apply Q2 in H0. destruct H0. subst. replace ofs with 0 by omega.
+  apply Q2 in H0. destruct H0. subst. replace ofs with 0 by lia.
   left; apply Mem.perm_cur; auto.
 + intros (P2 & Q2 & R2 & S2) (P1 & Q1 & R1 & S1).
   apply Q2 in H0. destruct H0. subst.
   left. apply Mem.perm_cur. eapply Mem.perm_implies; eauto.
-  apply P1. omega.
+  apply P1. lia.
 Qed.
 
 End INIT_MEM.
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 2e79d1a9..561e94c9 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -347,7 +347,7 @@ Proof.
   induction rl; simpl; intros. constructor. constructor; auto. apply areg_sound; auto.
 Qed.
 
-Hint Resolve areg_sound aregs_sound: va.
+Global Hint Resolve areg_sound aregs_sound: va.
 
 Lemma abuiltin_arg_sound:
   forall bc ge rs sp m ae rm am,
@@ -549,8 +549,8 @@ Proof.
     eapply SM; auto. eapply mmatch_top; eauto.
   + (* below *)
     red; simpl; intros. rewrite NB. destruct (eq_block b sp).
-    subst b; rewrite SP; xomega.
-    exploit mmatch_below; eauto. xomega.
+    subst b; rewrite SP; extlia.
+    exploit mmatch_below; eauto. extlia.
 - (* unchanged *)
   simpl; intros. apply dec_eq_false. apply Plt_ne. auto.
 - (* values *)
@@ -1152,11 +1152,11 @@ Proof.
 - constructor.
 - assert (Plt sp bound') by eauto with va.
   eapply sound_stack_public_call; eauto. apply IHsound_stack; intros.
-  apply INV. xomega. rewrite SAME; auto with ordered_type. xomega. auto. auto.
+  apply INV. extlia. rewrite SAME; auto with ordered_type. extlia. auto. auto.
 - assert (Plt sp bound') by eauto with va.
   eapply sound_stack_private_call; eauto. apply IHsound_stack; intros.
-  apply INV. xomega. rewrite SAME; auto with ordered_type. xomega. auto. auto.
-  apply bmatch_ext with m; auto. intros. apply INV. xomega. auto. auto. auto.
+  apply INV. extlia. rewrite SAME; auto with ordered_type. extlia. auto. auto.
+  apply bmatch_ext with m; auto. intros. apply INV. extlia. auto. auto. auto.
 Qed.
 
 Lemma sound_stack_inv:
@@ -1215,8 +1215,8 @@ Lemma sound_stack_new_bound:
 Proof.
   intros. inv H.
 - constructor.
-- eapply sound_stack_public_call with (bound' := bound'0); eauto. xomega.
-- eapply sound_stack_private_call with (bound' := bound'0); eauto. xomega.
+- eapply sound_stack_public_call with (bound' := bound'0); eauto. extlia.
+- eapply sound_stack_private_call with (bound' := bound'0); eauto. extlia.
 Qed.
 
 Lemma sound_stack_exten:
@@ -1229,12 +1229,12 @@ Proof.
 - constructor.
 - assert (Plt sp bound') by eauto with va.
   eapply sound_stack_public_call; eauto.
-  rewrite H0; auto. xomega.
-  intros. rewrite H0; auto. xomega.
+  rewrite H0; auto. extlia.
+  intros. rewrite H0; auto. extlia.
 - assert (Plt sp bound') by eauto with va.
   eapply sound_stack_private_call; eauto.
-  rewrite H0; auto. xomega.
-  intros. rewrite H0; auto. xomega.
+  rewrite H0; auto. extlia.
+  intros. rewrite H0; auto. extlia.
 Qed.
 
 (** ** Preservation of the semantic invariant by one step of execution *)
@@ -1935,7 +1935,7 @@ Proof.
 - exact NOSTACK.
 Qed.
 
-Hint Resolve areg_sound aregs_sound: va.
+Global Hint Resolve areg_sound aregs_sound: va.
 
 (** * Interface with other optimizations *)
 
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index f1a46baa..5a7cfc12 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -15,6 +15,7 @@ Require Import Zwf Coqlib Maps Zbits Integers Floats Lattice.
 Require Import Compopts AST.
 Require Import Values Memory Globalenvs Builtins Events.
 Require Import Registers RTL.
+Require Import Lia.
 
 (** The abstract domains for value analysis *)
 
@@ -43,12 +44,12 @@ Proof.
   elim H. apply H0; auto.
 Qed.
 
-Hint Extern 2 (_ = _) => congruence : va.
-Hint Extern 2 (_ <> _) => congruence : va.
-Hint Extern 2 (_ < _) => xomega : va.
-Hint Extern 2 (_ <= _) => xomega : va.
-Hint Extern 2 (_ > _) => xomega : va.
-Hint Extern 2 (_ >= _) => xomega : va.
+Global Hint Extern 2 (_ = _) => congruence : va.
+Global Hint Extern 2 (_ <> _) => congruence : va.
+Global Hint Extern 2 (_ < _) => extlia : va.
+Global Hint Extern 2 (_ <= _) => extlia : va.
+Global Hint Extern 2 (_ > _) => extlia : va.
+Global Hint Extern 2 (_ >= _) => extlia : va.
 
 Section MATCH.
 
@@ -595,17 +596,17 @@ Hint Extern 1 (vmatch _ _) => constructor : va.
 
 Lemma is_uns_mon: forall n1 n2 i, is_uns n1 i -> n1 <= n2 -> is_uns n2 i.
 Proof.
-  intros; red; intros. apply H; omega.
+  intros; red; intros. apply H; lia.
 Qed.
 
 Lemma is_sgn_mon: forall n1 n2 i, is_sgn n1 i -> n1 <= n2 -> is_sgn n2 i.
 Proof.
-  intros; red; intros. apply H; omega.
+  intros; red; intros. apply H; lia.
 Qed.
 
 Lemma is_uns_sgn: forall n1 n2 i, is_uns n1 i -> n1 < n2 -> is_sgn n2 i.
 Proof.
-  intros; red; intros. rewrite ! H by omega. auto.
+  intros; red; intros. rewrite ! H by lia. auto.
 Qed.
 
 Definition usize := Int.size.
@@ -616,7 +617,7 @@ Lemma is_uns_usize:
   forall i, is_uns (usize i) i.
 Proof.
   unfold usize; intros; red; intros.
-  apply Int.bits_size_2. omega.
+  apply Int.bits_size_2. lia.
 Qed.
 
 Lemma is_sgn_ssize:
@@ -628,10 +629,10 @@ Proof.
   rewrite <- (negb_involutive (Int.testbit i (Int.zwordsize - 1))).
   f_equal.
   generalize (Int.size_range (Int.not i)); intros RANGE.
-  rewrite <- ! Int.bits_not by omega.
-  rewrite ! Int.bits_size_2 by omega.
+  rewrite <- ! Int.bits_not by lia.
+  rewrite ! Int.bits_size_2 by lia.
   auto.
-- rewrite ! Int.bits_size_2 by omega.
+- rewrite ! Int.bits_size_2 by lia.
   auto.
 Qed.
 
@@ -639,8 +640,8 @@ Lemma is_uns_zero_ext:
   forall n i, is_uns n i <-> Int.zero_ext n i = i.
 Proof.
   intros; split; intros.
-  Int.bit_solve. destruct (zlt i0 n); auto. symmetry; apply H; auto. omega.
-  rewrite <- H. red; intros. rewrite Int.bits_zero_ext by omega. rewrite zlt_false by omega. auto.
+  Int.bit_solve. destruct (zlt i0 n); auto. symmetry; apply H; auto. lia.
+  rewrite <- H. red; intros. rewrite Int.bits_zero_ext by lia. rewrite zlt_false by lia. auto.
 Qed.
 
 Lemma is_sgn_sign_ext:
@@ -649,18 +650,18 @@ Proof.
   intros; split; intros.
   Int.bit_solve. destruct (zlt i0 n); auto.
   transitivity (Int.testbit i (Int.zwordsize - 1)).
-  apply H0; omega. symmetry; apply H0; omega.
-  rewrite <- H0. red; intros. rewrite ! Int.bits_sign_ext by omega.
-  f_equal. transitivity (n-1). destruct (zlt m n); omega.
-  destruct (zlt (Int.zwordsize - 1) n); omega.
+  apply H0; lia. symmetry; apply H0; lia.
+  rewrite <- H0. red; intros. rewrite ! Int.bits_sign_ext by lia.
+  f_equal. transitivity (n-1). destruct (zlt m n); lia.
+  destruct (zlt (Int.zwordsize - 1) n); lia.
 Qed.
 
 Lemma is_zero_ext_uns:
   forall i n m,
   is_uns m i \/ n <= m -> is_uns m (Int.zero_ext n i).
 Proof.
-  intros. red; intros. rewrite Int.bits_zero_ext by omega.
-  destruct (zlt m0 n); auto. destruct H. apply H; omega. omegaContradiction.
+  intros. red; intros. rewrite Int.bits_zero_ext by lia.
+  destruct (zlt m0 n); auto. destruct H. apply H; lia. extlia.
 Qed.
 
 Lemma is_zero_ext_sgn:
@@ -668,9 +669,9 @@ Lemma is_zero_ext_sgn:
   n < m ->
   is_sgn m (Int.zero_ext n i).
 Proof.
-  intros. red; intros. rewrite ! Int.bits_zero_ext by omega.
-  transitivity false. apply zlt_false; omega.
-  symmetry; apply zlt_false; omega.
+  intros. red; intros. rewrite ! Int.bits_zero_ext by lia.
+  transitivity false. apply zlt_false; lia.
+  symmetry; apply zlt_false; lia.
 Qed.
 
 Lemma is_sign_ext_uns:
@@ -679,8 +680,8 @@ Lemma is_sign_ext_uns:
   is_uns m i ->
   is_uns m (Int.sign_ext n i).
 Proof.
-  intros; red; intros. rewrite Int.bits_sign_ext by omega.
-  apply H0. destruct (zlt m0 n); omega. destruct (zlt m0 n); omega.
+  intros; red; intros. rewrite Int.bits_sign_ext by lia.
+  apply H0. destruct (zlt m0 n); lia. destruct (zlt m0 n); lia.
 Qed.
 
 Lemma is_sign_ext_sgn:
@@ -690,9 +691,9 @@ Lemma is_sign_ext_sgn:
 Proof.
   intros. apply is_sgn_sign_ext; auto.
   destruct (zlt m n). destruct H1. apply is_sgn_sign_ext in H1; auto.
-  rewrite <- H1. rewrite (Int.sign_ext_widen i) by omega. apply Int.sign_ext_idem; auto.
-  omegaContradiction.
-  apply Int.sign_ext_widen; omega.
+  rewrite <- H1. rewrite (Int.sign_ext_widen i) by lia. apply Int.sign_ext_idem; auto.
+  extlia.
+  apply Int.sign_ext_widen; lia.
 Qed.
 
 Hint Resolve is_uns_mon is_sgn_mon is_uns_sgn is_uns_usize is_sgn_ssize : va.
@@ -701,8 +702,8 @@ Lemma is_uns_1:
   forall n, is_uns 1 n -> n = Int.zero \/ n = Int.one.
 Proof.
   intros. destruct (Int.testbit n 0) eqn:B0; [right|left]; apply Int.same_bits_eq; intros.
-  rewrite Int.bits_one. destruct (zeq i 0). subst i; auto. apply H; omega.
-  rewrite Int.bits_zero. destruct (zeq i 0). subst i; auto. apply H; omega.
+  rewrite Int.bits_one. destruct (zeq i 0). subst i; auto. apply H; lia.
+  rewrite Int.bits_zero. destruct (zeq i 0). subst i; auto. apply H; lia.
 Qed.
 
 (** Tracking leakage of pointers through arithmetic operations.
@@ -958,13 +959,13 @@ Hint Resolve vge_uns_uns' vge_uns_i' vge_sgn_sgn' vge_sgn_i' : va.
 
 Lemma usize_pos: forall n, 0 <= usize n.
 Proof.
-  unfold usize; intros. generalize (Int.size_range n); omega.
+  unfold usize; intros. generalize (Int.size_range n); lia.
 Qed.
 
 Lemma ssize_pos: forall n, 0 < ssize n.
 Proof.
   unfold ssize; intros.
-  generalize (Int.size_range (if Int.lt n Int.zero then Int.not n else n)); omega.
+  generalize (Int.size_range (if Int.lt n Int.zero then Int.not n else n)); lia.
 Qed.
 
 Lemma vge_lub_l:
@@ -975,12 +976,12 @@ Proof.
   unfold vlub; destruct x, y; eauto using pge_lub_l with va.
 - predSpec Int.eq Int.eq_spec n n0. auto with va.
   destruct (Int.lt n Int.zero || Int.lt n0 Int.zero).
-  apply vge_sgn_i'. generalize (ssize_pos n); xomega. eauto with va.
-  apply vge_uns_i'. generalize (usize_pos n); xomega. eauto with va.
+  apply vge_sgn_i'. generalize (ssize_pos n); extlia. eauto with va.
+  apply vge_uns_i'. generalize (usize_pos n); extlia. eauto with va.
 - destruct (Int.lt n Int.zero).
-  apply vge_sgn_i'. generalize (ssize_pos n); xomega. eauto with va.
-  apply vge_uns_i'. generalize (usize_pos n); xomega. eauto with va.
-- apply vge_sgn_i'. generalize (ssize_pos n); xomega. eauto with va.
+  apply vge_sgn_i'. generalize (ssize_pos n); extlia. eauto with va.
+  apply vge_uns_i'. generalize (usize_pos n); extlia. eauto with va.
+- apply vge_sgn_i'. generalize (ssize_pos n); extlia. eauto with va.
 - destruct (Int.lt n0 Int.zero).
   eapply vge_trans. apply vge_sgn_sgn'.
   apply vge_trans with (Sgn p (n + 1)); eauto with va.
@@ -1269,12 +1270,12 @@ Proof.
   destruct (Int.ltu n Int.iwordsize) eqn:LTU; auto.
   exploit Int.ltu_inv; eauto. intros RANGE.
   inv H; auto with va.
-- apply vmatch_uns'. red; intros. rewrite Int.bits_shl by omega.
-  destruct (zlt m (Int.unsigned n)). auto. apply H1; xomega.
+- apply vmatch_uns'. red; intros. rewrite Int.bits_shl by lia.
+  destruct (zlt m (Int.unsigned n)). auto. apply H1; extlia.
 - apply vmatch_sgn'. red; intros. zify.
-  rewrite ! Int.bits_shl by omega.
-  rewrite ! zlt_false by omega.
-  rewrite H1 by omega. symmetry. rewrite H1 by omega. auto.
+  rewrite ! Int.bits_shl by lia.
+  rewrite ! zlt_false by lia.
+  rewrite H1 by lia. symmetry. rewrite H1 by lia. auto.
 - destruct v; constructor.
 Qed.
 
@@ -1306,13 +1307,13 @@ Proof.
   assert (DEFAULT2: forall i, vmatch (Vint (Int.shru i n)) (uns (provenance x) (Int.zwordsize - Int.unsigned n))).
   {
     intros. apply vmatch_uns. red; intros.
-    rewrite Int.bits_shru by omega. apply zlt_false. omega.
+    rewrite Int.bits_shru by lia. apply zlt_false. lia.
   }
   inv H; auto with va.
 - apply vmatch_uns'. red; intros. zify.
-  rewrite Int.bits_shru by omega.
+  rewrite Int.bits_shru by lia.
   destruct (zlt (m + Int.unsigned n) Int.zwordsize); auto.
-  apply H1; omega.
+  apply H1; lia.
 - destruct v; constructor.
 Qed.
 
@@ -1345,22 +1346,22 @@ Proof.
   assert (DEFAULT2: forall i, vmatch (Vint (Int.shr i n)) (sgn (provenance x) (Int.zwordsize - Int.unsigned n))).
   {
     intros. apply vmatch_sgn. red; intros.
-    rewrite ! Int.bits_shr by omega. f_equal.
+    rewrite ! Int.bits_shr by lia. f_equal.
     destruct (zlt (m + Int.unsigned n) Int.zwordsize);
     destruct (zlt (Int.zwordsize - 1 + Int.unsigned n) Int.zwordsize);
-    omega.
+    lia.
   }
   assert (SGN: forall q i p, is_sgn p i -> 0 < p -> vmatch (Vint (Int.shr i n)) (sgn q (p - Int.unsigned n))).
   {
     intros. apply vmatch_sgn'. red; intros. zify.
-    rewrite ! Int.bits_shr by omega.
+    rewrite ! Int.bits_shr by lia.
     transitivity (Int.testbit i (Int.zwordsize - 1)).
     destruct (zlt (m + Int.unsigned n) Int.zwordsize).
-    apply H0; omega.
+    apply H0; lia.
     auto.
     symmetry.
     destruct (zlt (Int.zwordsize - 1 + Int.unsigned n) Int.zwordsize).
-    apply H0; omega.
+    apply H0; lia.
     auto.
   }
   inv H; eauto with va.
@@ -1418,12 +1419,12 @@ Proof.
   assert (UNS: forall i j n m, is_uns n i -> is_uns m j -> is_uns (Z.max n m) (Int.or i j)).
   {
     intros; red; intros. rewrite Int.bits_or by auto.
-    rewrite H by xomega. rewrite H0 by xomega. auto.
+    rewrite H by extlia. rewrite H0 by extlia. auto.
   }
   assert (SGN: forall i j n m, is_sgn n i -> is_sgn m j -> is_sgn (Z.max n m) (Int.or i j)).
   {
-    intros; red; intros. rewrite ! Int.bits_or by xomega.
-    rewrite H by xomega. rewrite H0 by xomega. auto.
+    intros; red; intros. rewrite ! Int.bits_or by extlia.
+    rewrite H by extlia. rewrite H0 by extlia. auto.
   }
   intros. unfold or, Val.or; inv H; eauto with va; inv H0; eauto with va.
 Qed.
@@ -1443,12 +1444,12 @@ Proof.
   assert (UNS: forall i j n m, is_uns n i -> is_uns m j -> is_uns (Z.max n m) (Int.xor i j)).
   {
     intros; red; intros. rewrite Int.bits_xor by auto.
-    rewrite H by xomega. rewrite H0 by xomega. auto.
+    rewrite H by extlia. rewrite H0 by extlia. auto.
   }
   assert (SGN: forall i j n m, is_sgn n i -> is_sgn m j -> is_sgn (Z.max n m) (Int.xor i j)).
   {
-    intros; red; intros. rewrite ! Int.bits_xor by xomega.
-    rewrite H by xomega. rewrite H0 by xomega. auto.
+    intros; red; intros. rewrite ! Int.bits_xor by extlia.
+    rewrite H by extlia. rewrite H0 by extlia. auto.
   }
   intros. unfold xor, Val.xor; inv H; eauto with va; inv H0; eauto with va.
 Qed.
@@ -1466,7 +1467,7 @@ Lemma notint_sound:
 Proof.
   assert (SGN: forall n i, is_sgn n i -> is_sgn n (Int.not i)).
   {
-    intros; red; intros. rewrite ! Int.bits_not by omega.
+    intros; red; intros. rewrite ! Int.bits_not by lia.
     f_equal. apply H; auto.
   }
   intros. unfold Val.notint, notint; inv H; eauto with va.
@@ -1492,13 +1493,13 @@ Proof.
   inv H; auto with va.
 - apply vmatch_uns. red; intros. rewrite Int.bits_rol by auto.
   generalize (Int.unsigned_range n); intros.
-  rewrite Z.mod_small by omega.
-  apply H1. omega. omega.
+  rewrite Z.mod_small by lia.
+  apply H1. lia. lia.
 - destruct (zlt n0 Int.zwordsize); auto with va.
-  apply vmatch_sgn. red; intros. rewrite ! Int.bits_rol by omega.
+  apply vmatch_sgn. red; intros. rewrite ! Int.bits_rol by lia.
   generalize (Int.unsigned_range n); intros.
-  rewrite ! Z.mod_small by omega.
-  rewrite H1 by omega. symmetry. rewrite H1 by omega. auto.
+  rewrite ! Z.mod_small by lia.
+  rewrite H1 by lia. symmetry. rewrite H1 by lia. auto.
 - destruct (zlt n0 Int.zwordsize); auto with va.
 Qed.
 
@@ -1674,8 +1675,8 @@ Proof.
     generalize (Int.unsigned_range_2 j); intros RANGE.
     assert (Int.unsigned j <> 0).
     { red; intros; elim H. rewrite <- (Int.repr_unsigned j). rewrite H0. auto. }
-    exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). omega. intros MOD.
-    unfold Int.modu. rewrite Int.unsigned_repr. omega. omega.
+    exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). lia. intros MOD.
+    unfold Int.modu. rewrite Int.unsigned_repr. lia. lia.
   }
   intros. destruct v; destruct w; try discriminate; simpl in H1.
   destruct (Int.eq i0 Int.zero) eqn:Z; inv H1.
@@ -2083,12 +2084,12 @@ Lemma zero_ext_sound:
 Proof.
   assert (DFL: forall nbits i, is_uns nbits (Int.zero_ext nbits i)).
   {
-    intros; red; intros. rewrite Int.bits_zero_ext by omega. apply zlt_false; auto.
+    intros; red; intros. rewrite Int.bits_zero_ext by lia. apply zlt_false; auto.
   }
   intros. inv H; simpl; auto with va. apply vmatch_uns.
   red; intros. zify.
-  rewrite Int.bits_zero_ext by omega.
-  destruct (zlt m nbits); auto. apply H1; omega.
+  rewrite Int.bits_zero_ext by lia.
+  destruct (zlt m nbits); auto. apply H1; lia.
 Qed.
 
 Definition sign_ext (nbits: Z) (v: aval) :=
@@ -2108,7 +2109,7 @@ Proof.
     intros. apply vmatch_sgn. apply is_sign_ext_sgn; auto with va.
   }
   intros. unfold sign_ext. destruct (zle nbits 0).
-- destruct v; simpl; auto with va. constructor. omega. 
+- destruct v; simpl; auto with va. constructor. lia. 
   rewrite Int.sign_ext_below by auto. red; intros; apply Int.bits_zero.
 - inv H; simpl; auto with va.
 + destruct (zlt n nbits); eauto with va.
@@ -2822,8 +2823,8 @@ Proof.
     generalize (Int.unsigned_range_2 j); intros RANGE.
     assert (Int.unsigned j <> 0).
     { red; intros; elim H. rewrite <- (Int.repr_unsigned j). rewrite H0. auto. }
-    exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). omega. intros MOD.
-    unfold Int.modu. rewrite Int.unsigned_repr. omega. omega.
+    exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). lia. intros MOD.
+    unfold Int.modu. rewrite Int.unsigned_repr. lia. lia.
   }
   intros until y.
   intros HX HY.
@@ -2975,26 +2976,26 @@ Proof.
   intros c [lo hi] x n; simpl; intros R.
   destruct c; unfold zcmp, proj_sumbool.
 - (* eq *)
-  destruct (zlt n lo). rewrite zeq_false by omega. constructor.
-  destruct (zlt hi n). rewrite zeq_false by omega. constructor.
+  destruct (zlt n lo). rewrite zeq_false by lia. constructor.
+  destruct (zlt hi n). rewrite zeq_false by lia. constructor.
   constructor.
 - (* ne *)
   constructor.
 - (* lt *)
-  destruct (zlt hi n). rewrite zlt_true by omega. constructor.
-  destruct (zle n lo). rewrite zlt_false by omega. constructor.
+  destruct (zlt hi n). rewrite zlt_true by lia. constructor.
+  destruct (zle n lo). rewrite zlt_false by lia. constructor.
   constructor.
 - (* le *)
-  destruct (zle hi n). rewrite zle_true by omega. constructor.
-  destruct (zlt n lo). rewrite zle_false by omega. constructor.
+  destruct (zle hi n). rewrite zle_true by lia. constructor.
+  destruct (zlt n lo). rewrite zle_false by lia. constructor.
   constructor.
 - (* gt *)
-  destruct (zlt n lo). rewrite zlt_true by omega. constructor.
-  destruct (zle hi n). rewrite zlt_false by omega. constructor.
+  destruct (zlt n lo). rewrite zlt_true by lia. constructor.
+  destruct (zle hi n). rewrite zlt_false by lia. constructor.
   constructor.
 - (* ge *)
-  destruct (zle n lo). rewrite zle_true by omega. constructor.
-  destruct (zlt hi n). rewrite zle_false by omega. constructor.
+  destruct (zle n lo). rewrite zle_true by lia. constructor.
+  destruct (zlt hi n). rewrite zle_false by lia. constructor.
   constructor.
 Qed.
 
@@ -3028,10 +3029,10 @@ Lemma uintv_sound:
   forall n v, vmatch (Vint n) v -> fst (uintv v) <= Int.unsigned n <= snd (uintv v).
 Proof.
   intros. inv H; simpl; try (apply Int.unsigned_range_2).
-- omega.
+- lia.
 - destruct (zlt n0 Int.zwordsize); simpl.
-+ rewrite is_uns_zero_ext in H2. rewrite <- H2. rewrite Int.zero_ext_mod by omega.
-  exploit (Z_mod_lt (Int.unsigned n) (two_p n0)). apply two_p_gt_ZERO; auto. omega.
++ rewrite is_uns_zero_ext in H2. rewrite <- H2. rewrite Int.zero_ext_mod by lia.
+  exploit (Z_mod_lt (Int.unsigned n) (two_p n0)). apply two_p_gt_ZERO; auto. lia.
 + apply Int.unsigned_range_2.
 Qed.
 
@@ -3043,8 +3044,8 @@ Proof.
   intros. simpl. replace (Int.cmpu c n1 n2) with (zcmp c (Int.unsigned n1) (Int.unsigned n2)).
   apply zcmp_intv_sound; apply uintv_sound; auto.
   destruct c; simpl; auto.
-  unfold Int.ltu. destruct (zle (Int.unsigned n1) (Int.unsigned n2)); [rewrite zlt_false|rewrite zlt_true]; auto; omega.
-  unfold Int.ltu. destruct (zle (Int.unsigned n2) (Int.unsigned n1)); [rewrite zlt_false|rewrite zlt_true]; auto; omega.
+  unfold Int.ltu. destruct (zle (Int.unsigned n1) (Int.unsigned n2)); [rewrite zlt_false|rewrite zlt_true]; auto; lia.
+  unfold Int.ltu. destruct (zle (Int.unsigned n2) (Int.unsigned n1)); [rewrite zlt_false|rewrite zlt_true]; auto; lia.
 Qed.
 
 Lemma cmpu_intv_sound_2:
@@ -3071,22 +3072,22 @@ Lemma sintv_sound:
   forall n v, vmatch (Vint n) v -> fst (sintv v) <= Int.signed n <= snd (sintv v).
 Proof.
   intros. inv H; simpl; try (apply Int.signed_range).
-- omega.
+- lia.
 - destruct (zlt n0 Int.zwordsize); simpl.
 + rewrite is_uns_zero_ext in H2. rewrite <- H2.
-  assert (Int.unsigned (Int.zero_ext n0 n) = Int.unsigned n mod two_p n0) by (apply Int.zero_ext_mod; omega).
+  assert (Int.unsigned (Int.zero_ext n0 n) = Int.unsigned n mod two_p n0) by (apply Int.zero_ext_mod; lia).
   exploit (Z_mod_lt (Int.unsigned n) (two_p n0)). apply two_p_gt_ZERO; auto. intros.
   replace (Int.signed (Int.zero_ext n0 n)) with (Int.unsigned (Int.zero_ext n0 n)).
-  rewrite H. omega.
+  rewrite H. lia.
   unfold Int.signed. rewrite zlt_true. auto.
   assert (two_p n0 <= Int.half_modulus).
   { change Int.half_modulus with (two_p (Int.zwordsize - 1)).
-    apply two_p_monotone. omega. }
-  omega.
+    apply two_p_monotone. lia. }
+  lia.
 + apply Int.signed_range.
 - destruct (zlt n0 (Int.zwordsize)); simpl.
 + rewrite is_sgn_sign_ext in H2 by auto. rewrite <- H2.
-  exploit (Int.sign_ext_range n0 n). omega. omega.
+  exploit (Int.sign_ext_range n0 n). lia. lia.
 + apply Int.signed_range.
 Qed.
 
@@ -3098,8 +3099,8 @@ Proof.
   intros. simpl. replace (Int.cmp c n1 n2) with (zcmp c (Int.signed n1) (Int.signed n2)).
   apply zcmp_intv_sound; apply sintv_sound; auto.
   destruct c; simpl; rewrite ? Int.eq_signed; auto.
-  unfold Int.lt. destruct (zle (Int.signed n1) (Int.signed n2)); [rewrite zlt_false|rewrite zlt_true]; auto; omega.
-  unfold Int.lt. destruct (zle (Int.signed n2) (Int.signed n1)); [rewrite zlt_false|rewrite zlt_true]; auto; omega.
+  unfold Int.lt. destruct (zle (Int.signed n1) (Int.signed n2)); [rewrite zlt_false|rewrite zlt_true]; auto; lia.
+  unfold Int.lt. destruct (zle (Int.signed n2) (Int.signed n1)); [rewrite zlt_false|rewrite zlt_true]; auto; lia.
 Qed.
 
 Lemma cmp_intv_sound_2:
@@ -3284,7 +3285,7 @@ Proof.
   assert (DEFAULT: vmatch (Val.of_optbool ob) (Uns Pbot 1)).
   {
     destruct ob; simpl; auto with va.
-    destruct b; constructor; try omega.
+    destruct b; constructor; try lia.
     change 1 with (usize Int.one). apply is_uns_usize.
     red; intros. apply Int.bits_zero.
   }
@@ -3403,27 +3404,27 @@ Proof.
 - destruct (zlt n 8); constructor; auto with va.
   apply is_sign_ext_uns; auto.
   apply is_sign_ext_sgn; auto with va.
-- constructor. xomega. apply is_zero_ext_uns. apply Z.min_case; auto with va.
+- constructor. extlia. apply is_zero_ext_uns. apply Z.min_case; auto with va.
 - destruct (zlt n 16); constructor; auto with va.
   apply is_sign_ext_uns; auto.
   apply is_sign_ext_sgn; auto with va.
-- constructor. xomega. apply is_zero_ext_uns. apply Z.min_case; auto with va.
+- constructor. extlia. apply is_zero_ext_uns. apply Z.min_case; auto with va.
 - destruct (zlt n 8); auto with va.
 - destruct (zlt n 16); auto with va.
-- constructor. xomega. apply is_sign_ext_sgn; auto with va. apply Z.min_case; auto with va.
-- constructor. omega. apply is_zero_ext_uns; auto with va.
-- constructor. xomega. apply is_sign_ext_sgn; auto with va. apply Z.min_case; auto with va.
-- constructor. omega. apply is_zero_ext_uns; auto with va.
+- constructor. extlia. apply is_sign_ext_sgn; auto with va. apply Z.min_case; auto with va.
+- constructor. lia. apply is_zero_ext_uns; auto with va.
+- constructor. extlia. apply is_sign_ext_sgn; auto with va. apply Z.min_case; auto with va.
+- constructor. lia. apply is_zero_ext_uns; auto with va.
 - destruct ptr64; auto with va.
 - destruct ptr64; auto with va.
 - destruct ptr64; auto with va.
 - destruct ptr64; auto with va.
 - destruct ptr64; auto with va.
 - destruct ptr64; auto with va.
-- constructor. omega. apply is_sign_ext_sgn; auto with va.
-- constructor. omega. apply is_zero_ext_uns; auto with va.
-- constructor. omega. apply is_sign_ext_sgn; auto with va.
-- constructor. omega. apply is_zero_ext_uns; auto with va.
+- constructor. lia. apply is_sign_ext_sgn; auto with va.
+- constructor. lia. apply is_zero_ext_uns; auto with va.
+- constructor. lia. apply is_sign_ext_sgn; auto with va.
+- constructor. lia. apply is_zero_ext_uns; auto with va.
 - destruct ptr64; auto with va.
 - destruct ptr64; auto with va.
 - destruct ptr64; auto with va.
@@ -3438,13 +3439,13 @@ Proof.
   intros. exploit Mem.load_cast; eauto. exploit Mem.load_type; eauto.
   destruct chunk; simpl; intros.
 - (* int8signed *)
-  rewrite H2. destruct v; simpl; constructor. omega. apply is_sign_ext_sgn; auto with va.
+  rewrite H2. destruct v; simpl; constructor. lia. apply is_sign_ext_sgn; auto with va.
 - (* int8unsigned *)
-  rewrite H2. destruct v; simpl; constructor. omega. apply is_zero_ext_uns; auto with va.
+  rewrite H2. destruct v; simpl; constructor. lia. apply is_zero_ext_uns; auto with va.
 - (* int16signed *)
-  rewrite H2. destruct v; simpl; constructor. omega. apply is_sign_ext_sgn; auto with va.
+  rewrite H2. destruct v; simpl; constructor. lia. apply is_sign_ext_sgn; auto with va.
 - (* int16unsigned *)
-  rewrite H2. destruct v; simpl; constructor. omega. apply is_zero_ext_uns; auto with va.
+  rewrite H2. destruct v; simpl; constructor. lia. apply is_zero_ext_uns; auto with va.
 - (* int32 *)
   auto.
 - (* int64 *)
@@ -3486,9 +3487,9 @@ Proof with (auto using provenance_monotone with va).
   apply is_sign_ext_sgn...
 - constructor... apply is_zero_ext_uns... apply Z.min_case...
 - unfold provenance; destruct (va_strict tt)...
-- destruct (zlt n1 8). rewrite zlt_true by omega...
+- destruct (zlt n1 8). rewrite zlt_true by lia...
   destruct (zlt n2 8)...
-- destruct (zlt n1 16). rewrite zlt_true by omega...
+- destruct (zlt n1 16). rewrite zlt_true by lia...
   destruct (zlt n2 16)...
 - constructor... apply is_sign_ext_sgn... apply Z.min_case...
 - constructor... apply is_zero_ext_uns...
@@ -3609,7 +3610,7 @@ Function inval_after (lo: Z) (hi: Z) (c: ZTree.t acontent) { wf (Zwf lo) hi } :
   then inval_after lo (hi - 1) (ZTree.remove hi c)
   else c.
 Proof.
-  intros; red; omega.
+  intros; red; lia.
   apply Zwf_well_founded.
 Qed.
 
@@ -3624,7 +3625,7 @@ Function inval_before (hi: Z) (lo: Z) (c: ZTree.t acontent) { wf (Zwf_up hi) lo
   then inval_before hi (lo + 1) (inval_if hi lo c)
   else c.
 Proof.
-  intros; red; omega.
+  intros; red; lia.
   apply Zwf_up_well_founded.
 Qed.
 
@@ -3662,7 +3663,7 @@ Remark loadbytes_load_ext:
 Proof.
   intros. exploit Mem.load_loadbytes; eauto. intros [bytes [A B]].
   exploit Mem.load_valid_access; eauto. intros [C D].
-  subst v. apply Mem.loadbytes_load; auto. apply H; auto. generalize (size_chunk_pos chunk); omega.
+  subst v. apply Mem.loadbytes_load; auto. apply H; auto. generalize (size_chunk_pos chunk); lia.
 Qed.
 
 Lemma smatch_ext:
@@ -3673,7 +3674,7 @@ Lemma smatch_ext:
 Proof.
   intros. destruct H. split; intros.
   eapply H; eauto. eapply loadbytes_load_ext; eauto.
-  eapply H1; eauto. apply H0; eauto. omega.
+  eapply H1; eauto. apply H0; eauto. lia.
 Qed.
 
 Lemma smatch_inv:
@@ -3708,19 +3709,19 @@ Proof.
   + rewrite (Mem.loadbytes_empty m b ofs sz) in LOAD by auto.
     inv LOAD. contradiction.
   + exploit (Mem.loadbytes_split m b ofs 1 (sz - 1) bytes).
-    replace (1 + (sz - 1)) with sz by omega. auto.
-    omega.
-    omega.
+    replace (1 + (sz - 1)) with sz by lia. auto.
+    lia.
+    lia.
     intros (bytes1 & bytes2 & LOAD1 & LOAD2 & CONCAT).
     subst bytes.
     exploit Mem.loadbytes_length. eexact LOAD1. change (Z.to_nat 1) with 1%nat. intros LENGTH1.
     rewrite in_app_iff in IN. destruct IN.
   * destruct bytes1; try discriminate. destruct bytes1; try discriminate.
     simpl in H. destruct H; try contradiction. subst m0.
-    exists ofs; split. omega. auto.
-  * exploit (REC (sz - 1)). red; omega. eexact LOAD2. auto.
+    exists ofs; split. lia. auto.
+  * exploit (REC (sz - 1)). red; lia. eexact LOAD2. auto.
     intros (ofs' & A & B).
-    exists ofs'; split. omega. auto.
+    exists ofs'; split. lia. auto.
 Qed.
 
 Lemma smatch_loadbytes:
@@ -3746,13 +3747,13 @@ Proof.
 - apply Zwf_well_founded.
 - intros sz REC ofs bytes LOAD LOAD1 IN.
   exploit (Mem.loadbytes_split m b ofs 1 (sz - 1) bytes).
-  replace (1 + (sz - 1)) with sz by omega. auto.
-  omega.
-  omega.
+  replace (1 + (sz - 1)) with sz by lia. auto.
+  lia.
+  lia.
   intros (bytes1 & bytes2 & LOAD3 & LOAD4 & CONCAT). subst bytes. rewrite in_app_iff.
   destruct (zeq ofs ofs').
 + subst ofs'. rewrite LOAD1 in LOAD3; inv LOAD3. left; simpl; auto.
-+ right. eapply (REC (sz - 1)). red; omega. eexact LOAD4. auto. omega.
++ right. eapply (REC (sz - 1)). red; lia. eexact LOAD4. auto. lia.
 Qed.
 
 Lemma storebytes_provenance:
@@ -3770,10 +3771,10 @@ Proof.
     destruct (eq_block b' b); auto.
     destruct (zle (ofs' + 1) ofs); auto.
     destruct (zle (ofs + Z.of_nat (length bytes)) ofs'); auto.
-    right. split. auto. omega.
+    right. split. auto. lia.
   }
   destruct EITHER as [A | (A & B)].
-- right. rewrite <- H0. symmetry. eapply Mem.loadbytes_storebytes_other; eauto. omega.
+- right. rewrite <- H0. symmetry. eapply Mem.loadbytes_storebytes_other; eauto. lia.
 - subst b'. left.
   eapply loadbytes_provenance; eauto.
   eapply Mem.loadbytes_storebytes_same; eauto.
@@ -3918,7 +3919,7 @@ Remark inval_after_outside:
   forall i lo hi c, i < lo \/ i > hi -> (inval_after lo hi c)##i = c##i.
 Proof.
   intros until c. functional induction (inval_after lo hi c); intros.
-  rewrite IHt by omega. apply ZTree.gro. unfold ZTree.elt, ZIndexed.t; omega.
+  rewrite IHt by lia. apply ZTree.gro. unfold ZTree.elt, ZIndexed.t; lia.
   auto.
 Qed.
 
@@ -3929,18 +3930,18 @@ Remark inval_after_contents:
 Proof.
   intros until c. functional induction (inval_after lo hi c); intros.
   destruct (zeq i hi).
-  subst i. rewrite inval_after_outside in H by omega. rewrite ZTree.grs in H. discriminate.
-  exploit IHt; eauto. intros [A B]. rewrite ZTree.gro in A by auto. split. auto. omega.
-  split. auto. omega.
+  subst i. rewrite inval_after_outside in H by lia. rewrite ZTree.grs in H. discriminate.
+  exploit IHt; eauto. intros [A B]. rewrite ZTree.gro in A by auto. split. auto. lia.
+  split. auto. lia.
 Qed.
 
 Remark inval_before_outside:
   forall i hi lo c, i < lo \/ i >= hi -> (inval_before hi lo c)##i = c##i.
 Proof.
   intros until c. functional induction (inval_before hi lo c); intros.
-  rewrite IHt by omega. unfold inval_if. destruct (c##lo) as [[chunk av]|]; auto.
+  rewrite IHt by lia. unfold inval_if. destruct (c##lo) as [[chunk av]|]; auto.
   destruct (zle (lo + size_chunk chunk) hi); auto.
-  apply ZTree.gro. unfold ZTree.elt, ZIndexed.t; omega.
+  apply ZTree.gro. unfold ZTree.elt, ZIndexed.t; lia.
   auto.
 Qed.
 
@@ -3951,16 +3952,21 @@ Remark inval_before_contents_1:
 Proof.
   intros until c. functional induction (inval_before hi lo c); intros.
 - destruct (zeq lo i).
-+ subst i. rewrite inval_before_outside in H0 by omega.
++ subst i. rewrite inval_before_outside in H0 by lia.
   unfold inval_if in H0. destruct (c##lo) as [[chunk0 v0]|] eqn:C; try congruence.
   destruct (zle (lo + size_chunk chunk0) hi).
   rewrite C in H0; inv H0. auto.
   rewrite ZTree.grs in H0. congruence.
-+ exploit IHt. omega. auto. intros [A B]; split; auto.
++ exploit IHt. lia. auto. intros [A B]; split; auto.
   unfold inval_if in A. destruct (c##lo) as [[chunk0 v0]|] eqn:C; auto.
   destruct (zle (lo + size_chunk chunk0) hi); auto.
   rewrite ZTree.gro in A; auto.
-- omegaContradiction.
+- extlia.
+Qed.
+
+Lemma max_size_chunk: forall chunk, size_chunk chunk <= 8.
+Proof.
+  destruct chunk; simpl; lia.
 Qed.
 
 Remark inval_before_contents:
@@ -3969,12 +3975,12 @@ Remark inval_before_contents:
   c##j = Some (ACval chunk' av') /\ (j + size_chunk chunk' <= i \/ i <= j).
 Proof.
   intros. destruct (zlt j (i - 7)).
-  rewrite inval_before_outside in H by omega.
-  split. auto. left. generalize (max_size_chunk chunk'); omega.
+  rewrite inval_before_outside in H by lia.
+  split. auto. left. generalize (max_size_chunk chunk'); lia.
   destruct (zlt j i).
-  exploit inval_before_contents_1; eauto. omega. tauto.
-  rewrite inval_before_outside in H by omega.
-  split. auto. omega.
+  exploit inval_before_contents_1; eauto. lia. tauto.
+  rewrite inval_before_outside in H by lia.
+  split. auto. lia.
 Qed.
 
 Lemma ablock_store_contents:
@@ -3990,7 +3996,7 @@ Proof.
   right. rewrite ZTree.gso in H by auto.
   exploit inval_before_contents; eauto. intros [A B].
   exploit inval_after_contents; eauto. intros [C D].
-  split. auto. omega.
+  split. auto. lia.
 Qed.
 
 Lemma chunk_compat_true:
@@ -4060,7 +4066,7 @@ Proof.
   unfold ablock_storebytes; simpl; intros.
   exploit inval_before_contents; eauto. clear H. intros [A B].
   exploit inval_after_contents; eauto. clear A. intros [C D].
-  split. auto. xomega.
+  split. auto. extlia.
 Qed.
 
 Lemma ablock_storebytes_sound:
@@ -4083,7 +4089,7 @@ Proof.
   exploit ablock_storebytes_contents; eauto. intros [A B].
   assert (Mem.load chunk' m b ofs' = Some v').
   { rewrite <- LOAD'; symmetry. eapply Mem.load_storebytes_other; eauto.
-    rewrite U. rewrite LENGTH. rewrite Z_to_nat_max. right; omega. }
+    rewrite U. rewrite LENGTH. rewrite Z_to_nat_max. right; lia. }
   exploit BM2; eauto. unfold ablock_load. rewrite A. rewrite COMPAT. auto.
 Qed.
 
@@ -4211,7 +4217,7 @@ Proof.
   apply bmatch_inv with m; auto.
 + intros. eapply Mem.loadbytes_store_other; eauto.
   left. red; intros; subst b0. elim (C ofs). apply Mem.perm_cur_max.
-  apply P. generalize (size_chunk_pos chunk); omega.
+  apply P. generalize (size_chunk_pos chunk); lia.
 - intros; red; intros; elim (C ofs0). eauto with mem.
 Qed.
 
@@ -4640,7 +4646,7 @@ Proof.
 - apply bmatch_ext with m; eauto with va.
 - apply smatch_ext with m; auto with va.
 - apply smatch_ext with m; auto with va.
-- red; intros. exploit mmatch_below0; eauto. xomega.
+- red; intros. exploit mmatch_below0; eauto. extlia.
 Qed.
 
 Lemma mmatch_free:
@@ -4651,7 +4657,7 @@ Lemma mmatch_free:
 Proof.
   intros. apply mmatch_ext with m; auto.
   intros. eapply Mem.loadbytes_free_2; eauto.
-  erewrite <- Mem.nextblock_free by eauto. xomega.
+  erewrite <- Mem.nextblock_free by eauto. extlia.
 Qed.
 
 Lemma mmatch_top':
@@ -4875,7 +4881,7 @@ Proof.
   {
     Local Transparent Mem.loadbytes.
     unfold Mem.loadbytes. rewrite pred_dec_true. reflexivity.
-    red; intros. replace ofs0 with ofs by omega. auto.
+    red; intros. replace ofs0 with ofs by lia. auto.
   }
   destruct mv; econstructor. destruct v; econstructor.
   apply inj_of_bc_valid.
@@ -4896,7 +4902,7 @@ Proof.
   auto.
 - (* overflow *)
   intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst.
-  rewrite Z.add_0_r. split. omega. apply Ptrofs.unsigned_range_2.
+  rewrite Z.add_0_r. split. lia. apply Ptrofs.unsigned_range_2.
 - (* perm inv *)
   intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst.
   rewrite Z.add_0_r in H2. auto.
@@ -5167,10 +5173,10 @@ Module VA <: SEMILATTICE.
 
 End VA.
 
-Hint Constructors cmatch : va.
-Hint Constructors pmatch: va.
-Hint Constructors vmatch: va.
-Hint Resolve cnot_sound symbol_address_sound
+Global Hint Constructors cmatch : va.
+Global Hint Constructors pmatch: va.
+Global Hint Constructors vmatch: va.
+Global Hint Resolve cnot_sound symbol_address_sound
        shl_sound shru_sound shr_sound
        and_sound or_sound xor_sound notint_sound
        ror_sound rolm_sound