Merge branch 'kvx-work' into BTL

22 files changed, 598 insertions, 540 deletions

diff --git a/common/AST.v b/common/AST.v
index 979db4b9..868364cd 100644
--- a/common/AST.v
+++ b/common/AST.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
@@ -61,7 +62,7 @@ Definition typesize (ty: typ) : Z :=
   end.
 
 Lemma typesize_pos: forall ty, typesize ty > 0.
-Proof. destruct ty; simpl; omega. Qed.
+Proof. destruct ty; simpl; lia. Qed.
 
 Lemma typesize_Tptr: typesize Tptr = if Archi.ptr64 then 8 else 4.
 Proof. unfold Tptr; destruct Archi.ptr64; auto. Qed.
@@ -122,17 +123,17 @@ These signatures are used in particular to determine appropriate
 calling conventions for the function. *)
 
 Record calling_convention : Type := mkcallconv {
-  cc_vararg: bool;                      (**r variable-arity function *)
-  cc_unproto: bool;                     (**r old-style unprototyped function *)
-  cc_structret: bool                    (**r function returning a struct  *)
+  cc_vararg: option Z;  (**r variable-arity function (+ number of fixed args) *)
+  cc_unproto: bool;     (**r old-style unprototyped function *)
+  cc_structret: bool    (**r function returning a struct  *)
 }.
 
 Definition cc_default :=
-  {| cc_vararg := false; cc_unproto := false; cc_structret := false |}.
+  {| cc_vararg := None; cc_unproto := false; cc_structret := false |}.
 
 Definition calling_convention_eq (x y: calling_convention) : {x=y} + {x<>y}.
 Proof.
-  decide equality; apply bool_dec.
+  decide equality; try (apply bool_dec). decide equality; apply Z.eq_dec.
 Defined.
 Global Opaque calling_convention_eq.
 
@@ -275,13 +276,13 @@ Fixpoint init_data_list_size (il: list init_data) {struct il} : Z :=
 Lemma init_data_size_pos:
   forall i, init_data_size i >= 0.
 Proof.
-  destruct i; simpl; try xomega. destruct Archi.ptr64; omega.
+  destruct i; simpl; try extlia. destruct Archi.ptr64; lia.
 Qed.
 
 Lemma init_data_list_size_pos:
   forall il, init_data_list_size il >= 0.
 Proof.
-  induction il; simpl. omega. generalize (init_data_size_pos a); omega.
+  induction il; simpl. lia. generalize (init_data_size_pos a); lia.
 Qed.
 
 (** Information attached to global variables. *)
diff --git a/common/Behaviors.v b/common/Behaviors.v
index 92bd708f..023b33e2 100644
--- a/common/Behaviors.v
+++ b/common/Behaviors.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/common/Builtins.v b/common/Builtins.v
index 476b541e..facff726 100644
--- a/common/Builtins.v
+++ b/common/Builtins.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/common/Builtins0.v b/common/Builtins0.v
index d84c9112..384dde1e 100644
--- a/common/Builtins0.v
+++ b/common/Builtins0.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
@@ -341,6 +342,7 @@ Inductive standard_builtin : Type :=
   | BI_i16_bswap
   | BI_i32_bswap
   | BI_i64_bswap
+  | BI_unreachable
   | BI_i64_umulh
   | BI_i64_smulh
   | BI_i64_sdiv
@@ -376,6 +378,7 @@ Definition standard_builtin_table : list (string * standard_builtin) :=
  :: ("__builtin_bswap", BI_i32_bswap)
  :: ("__builtin_bswap32", BI_i32_bswap)
  :: ("__builtin_bswap64", BI_i64_bswap)
+ :: ("__builtin_unreachable", BI_unreachable)
  :: ("__compcert_i64_umulh", BI_i64_umulh)
  :: ("__compcert_i64_smulh", BI_i64_smulh)
  :: ("__compcert_i64_sdiv", BI_i64_sdiv)
@@ -414,6 +417,8 @@ Definition standard_builtin_sig (b: standard_builtin) : signature :=
       mksignature (Tlong :: nil) Tlong cc_default
   | BI_i16_bswap =>
       mksignature (Tint :: nil) Tint cc_default
+  | BI_unreachable =>
+      mksignature nil Tvoid cc_default
   | BI_i64_shl  | BI_i64_shr | BI_i64_sar =>
       mksignature (Tlong :: Tint :: nil) Tlong cc_default
   | BI_i64_dtos | BI_i64_dtou =>
@@ -448,6 +453,7 @@ Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (sig
   | BI_i64_bswap =>
     mkbuiltin_n1t Tlong Tlong
                   (fun n => Int64.repr (decode_int (List.rev (encode_int 8%nat (Int64.unsigned n)))))
+  | BI_unreachable => mkbuiltin Tvoid (fun vargs => None) _ _
   | BI_i64_umulh => mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhu
   | BI_i64_smulh => mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhs
   | BI_i64_sdiv => mkbuiltin_v2p Tlong Val.divls _ _
diff --git a/common/Determinism.v b/common/Determinism.v
index 7fa01c2d..c8c90782 100644
--- a/common/Determinism.v
+++ b/common/Determinism.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/common/Errors.v b/common/Errors.v
index 6807735a..bf72f12b 100644
--- a/common/Errors.v
+++ b/common/Errors.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/common/Events.v b/common/Events.v
index 033e2e03..360da52f 100644
--- a/common/Events.v
+++ b/common/Events.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
@@ -25,6 +26,7 @@ Require Import Values.
 Require Import Memory.
 Require Import Globalenvs.
 Require Import Builtins.
+Require Import Lia.
 
 (** * Events and traces *)
 
@@ -798,7 +800,7 @@ Proof.
   exists f; exists v'; exists m1'; intuition. constructor; auto.
   red; intros. congruence.
 (* trace length *)
-- inv H; inv H0; simpl; omega.
+- inv H; inv H0; simpl; lia.
 (* receptive *)
 - inv H. exploit volatile_load_receptive; eauto. intros [v2 A].
   exists v2; exists m1; constructor; auto.
@@ -925,7 +927,7 @@ Proof.
   eelim H3; eauto.
   exploit Mem.store_valid_access_3. eexact H0. intros [X Y].
   apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem.
-  apply X. omega.
+  apply X. lia.
 Qed.
 
 Lemma volatile_store_receptive:
@@ -960,7 +962,7 @@ Proof.
   exploit volatile_store_inject; eauto. intros [m2' [A [B [C D]]]].
   exists f; exists Vundef; exists m2'; intuition. constructor; auto. red; intros; congruence.
 (* trace length *)
-- inv H; inv H0; simpl; omega.
+- inv H; inv H0; simpl; lia.
 (* receptive *)
 - assert (t1 = t2). inv H. eapply volatile_store_receptive; eauto.
   subst t2; exists vres1; exists m1; auto.
@@ -1042,7 +1044,7 @@ Proof.
   subst b1. rewrite C in H2. inv H2. eauto with mem.
   rewrite D in H2 by auto. congruence.
 (* trace length *)
-- inv H; simpl; omega.
+- inv H; simpl; lia.
 (* receptive *)
 - assert (t1 = t2). inv H; inv H0; auto. subst t2.
   exists vres1; exists m1; auto.
@@ -1122,21 +1124,21 @@ Proof.
   exploit Mem.address_inject; eauto.
     apply Mem.perm_implies with Freeable; auto with mem.
     apply P. instantiate (1 := lo).
-    generalize (size_chunk_pos Mptr); omega.
+    generalize (size_chunk_pos Mptr); lia.
   intro EQ.
   exploit Mem.free_parallel_inject; eauto. intros (m2' & C & D).
   exists f, Vundef, m2'; split.
   apply extcall_free_sem_ptr with (sz := sz) (m' := m2').
-    rewrite EQ. rewrite <- A. f_equal. omega.
+    rewrite EQ. rewrite <- A. f_equal. lia.
     auto. auto.
-    rewrite ! EQ. rewrite <- C. f_equal; omega.
+    rewrite ! EQ. rewrite <- C. f_equal; lia.
   split. auto.
   split. auto.
   split. eapply Mem.free_unchanged_on; eauto. unfold loc_unmapped. intros; congruence.
   split. eapply Mem.free_unchanged_on; eauto. unfold loc_out_of_reach.
     intros. red; intros. eelim H2; eauto.
     apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
-    apply P. omega.
+    apply P. lia.
   split. auto.
   red; intros. congruence.
 + inv H2. inv H6. replace v' with Vnullptr.
@@ -1145,7 +1147,7 @@ Proof.
   red; intros; congruence.
   unfold Vnullptr in *; destruct Archi.ptr64; inv H4; auto.
 (* trace length *)
-- inv H; simpl; omega.
+- inv H; simpl; lia.
 (* receptive *)
 - assert (t1 = t2) by (inv H; inv H0; auto). subst t2.
   exists vres1; exists m1; auto.
@@ -1217,23 +1219,23 @@ Proof.
   destruct (zeq sz 0).
 + (* special case sz = 0 *)
   assert (bytes = nil).
-  { exploit (Mem.loadbytes_empty m1 bsrc (Ptrofs.unsigned osrc) sz). omega. congruence. }
+  { exploit (Mem.loadbytes_empty m1 bsrc (Ptrofs.unsigned osrc) sz). lia. congruence. }
   subst.
   destruct (Mem.range_perm_storebytes m1' b0 (Ptrofs.unsigned (Ptrofs.add odst (Ptrofs.repr delta0))) nil)
   as [m2' SB].
-  simpl. red; intros; omegaContradiction.
+  simpl. red; intros; extlia.
   exists f, Vundef, m2'.
   split. econstructor; eauto.
-  intros; omegaContradiction.
-  intros; omegaContradiction.
-  right; omega.
-  apply Mem.loadbytes_empty. omega.
+  intros; extlia.
+  intros; extlia.
+  right; lia.
+  apply Mem.loadbytes_empty. lia.
   split. auto.
   split. eapply Mem.storebytes_empty_inject; eauto.
   split. eapply Mem.storebytes_unchanged_on; eauto. unfold loc_unmapped; intros.
   congruence.
   split. eapply Mem.storebytes_unchanged_on; eauto.
-  simpl; intros; omegaContradiction.
+  simpl; intros; extlia.
   split. apply inject_incr_refl.
   red; intros; congruence.
 + (* general case sz > 0 *)
@@ -1243,11 +1245,11 @@ Proof.
   assert (RPDST: Mem.range_perm m1 bdst (Ptrofs.unsigned odst) (Ptrofs.unsigned odst + sz) Cur Nonempty).
     replace sz with (Z.of_nat (length bytes)).
     eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem.
-    rewrite LEN. apply Z2Nat.id. omega.
+    rewrite LEN. apply Z2Nat.id. lia.
   assert (PSRC: Mem.perm m1 bsrc (Ptrofs.unsigned osrc) Cur Nonempty).
-    apply RPSRC. omega.
+    apply RPSRC. lia.
   assert (PDST: Mem.perm m1 bdst (Ptrofs.unsigned odst) Cur Nonempty).
-    apply RPDST. omega.
+    apply RPDST. lia.
   exploit Mem.address_inject.  eauto. eexact PSRC. eauto. intros EQ1.
   exploit Mem.address_inject.  eauto. eexact PDST. eauto. intros EQ2.
   exploit Mem.loadbytes_inject; eauto. intros [bytes2 [A B]].
@@ -1258,7 +1260,7 @@ Proof.
   intros; eapply Mem.aligned_area_inject with (m := m1); eauto.
   eapply Mem.disjoint_or_equal_inject with (m := m1); eauto.
   apply Mem.range_perm_max with Cur; auto.
-  apply Mem.range_perm_max with Cur; auto. omega.
+  apply Mem.range_perm_max with Cur; auto. lia.
   split. constructor.
   split. auto.
   split. eapply Mem.storebytes_unchanged_on; eauto. unfold loc_unmapped; intros.
@@ -1268,11 +1270,11 @@ Proof.
   apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem.
   eapply Mem.storebytes_range_perm; eauto.
   erewrite list_forall2_length; eauto.
-  omega.
+  lia.
   split. apply inject_incr_refl.
   red; intros; congruence.
 - (* trace length *)
-  intros; inv H. simpl; omega.
+  intros; inv H. simpl; lia.
 - (* receptive *)
   intros.
   assert (t1 = t2). inv H; inv H0; auto. subst t2.
@@ -1318,7 +1320,7 @@ Proof.
   eapply eventval_list_match_inject; eauto.
   red; intros; congruence.
 (* trace length *)
-- inv H; simpl; omega.
+- inv H; simpl; lia.
 (* receptive *)
 - assert (t1 = t2). inv H; inv H0; auto.
   exists vres1; exists m1; congruence.
@@ -1363,7 +1365,7 @@ Proof.
   eapply eventval_match_inject; eauto.
   red; intros; congruence.
 (* trace length *)
-- inv H; simpl; omega.
+- inv H; simpl; lia.
 (* receptive *)
 - assert (t1 = t2). inv H; inv H0; auto. subst t2.
   exists vres1; exists m1; auto.
@@ -1409,7 +1411,7 @@ Proof.
   econstructor; eauto.
   red; intros; congruence.
 (* trace length *)
-- inv H; simpl; omega.
+- inv H; simpl; lia.
 (* receptive *)
 - inv H; inv H0. exists Vundef, m1; constructor.
 (* determ *)
@@ -1443,7 +1445,7 @@ Proof.
   econstructor; eauto.
   red; intros; congruence.
 (* trace length *)
-- inv H; simpl; omega.
+- inv H; simpl; lia.
 (* receptive *)
 - inv H; inv H0. exists Vundef, m1; constructor.
 (* determ *)
@@ -1497,7 +1499,7 @@ Proof.
   constructor; auto.
   red; intros; congruence.
 (* trace length *)
-- inv H; simpl; omega.
+- inv H; simpl; lia.
 (* receptive *)
 - inv H; inv H0. exists vres1, m1; constructor; auto. 
 (* determ *)
@@ -1623,7 +1625,7 @@ Proof.
   intros. destruct (plt (Mem.nextblock m2) (Mem.nextblock m1)).
   exploit external_call_valid_block; eauto. intros.
   eelim Plt_strict; eauto.
-  unfold Plt, Ple in *; zify; omega.
+  unfold Plt, Ple in *; zify; lia.
 Qed.
 
 (** Special case of [external_call_mem_inject_gen] (for backward compatibility) *)
@@ -1738,7 +1740,7 @@ Qed.
 
 End EVAL_BUILTIN_ARG.
 
-Hint Constructors eval_builtin_arg: barg.
+Global Hint Constructors eval_builtin_arg: barg.
 
 (** Invariance by change of global environment. *)
 
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index d37fbd46..4c9e7889 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
@@ -55,7 +56,7 @@ Function store_zeros (m: mem) (b: block) (p: Z) (n: Z) {wf (Zwf 0) n}: option me
     | None => None
     end.
 Proof.
-  intros. red. omega.
+  intros. red. lia.
   apply Zwf_well_founded.
 Qed.
 
@@ -849,8 +850,8 @@ Proof.
   intros until n. functional induction (store_zeros m b p n); intros.
 - inv H; apply Mem.unchanged_on_refl.
 - apply Mem.unchanged_on_trans with m'.
-+ eapply Mem.store_unchanged_on; eauto. simpl. intros. apply H0. omega.
-+ apply IHo; auto. intros; apply H0; omega.
++ eapply Mem.store_unchanged_on; eauto. simpl. intros. apply H0. lia.
++ apply IHo; auto. intros; apply H0; lia.
 - discriminate.
 Qed.
 
@@ -879,7 +880,7 @@ Proof.
 - destruct (store_init_data m b p a) as [m1|] eqn:?; try congruence.
   apply Mem.unchanged_on_trans with m1.
   eapply store_init_data_unchanged; eauto. intros; apply H0; tauto.
-  eapply IHil; eauto. intros; apply H0. generalize (init_data_size_pos a); omega.
+  eapply IHil; eauto. intros; apply H0. generalize (init_data_size_pos a); lia.
 Qed.
 
 (** Properties related to [loadbytes] *)
@@ -887,7 +888,7 @@ Qed.
 Definition readbytes_as_zero (m: mem) (b: block) (ofs len: Z) : Prop :=
   forall p n,
   ofs <= p -> p + Z.of_nat n <= ofs + len ->
-  Mem.loadbytes m b p (Z.of_nat n) = Some (list_repeat n (Byte Byte.zero)).
+  Mem.loadbytes m b p (Z.of_nat n) = Some (List.repeat (Byte Byte.zero) n).
 
 Lemma store_zeros_loadbytes:
   forall m b p n m',
@@ -895,24 +896,24 @@ Lemma store_zeros_loadbytes:
   readbytes_as_zero m' b p n.
 Proof.
   intros until n; functional induction (store_zeros m b p n); red; intros.
-- destruct n0. simpl. apply Mem.loadbytes_empty. omega.
-  rewrite Nat2Z.inj_succ in H1. omegaContradiction.
+- destruct n0. simpl. apply Mem.loadbytes_empty. lia.
+  rewrite Nat2Z.inj_succ in H1. extlia.
 - destruct (zeq p0 p).
-  + subst p0. destruct n0. simpl. apply Mem.loadbytes_empty. omega.
+  + subst p0. destruct n0. simpl. apply Mem.loadbytes_empty. lia.
     rewrite Nat2Z.inj_succ in H1. rewrite Nat2Z.inj_succ.
-    replace (Z.succ (Z.of_nat n0)) with (1 + Z.of_nat n0) by omega.
-    change (list_repeat (S n0) (Byte Byte.zero))
-      with ((Byte Byte.zero :: nil) ++ list_repeat n0 (Byte Byte.zero)).
+    replace (Z.succ (Z.of_nat n0)) with (1 + Z.of_nat n0) by lia.
+    change (List.repeat (Byte Byte.zero) (S n0))
+      with ((Byte Byte.zero :: nil) ++ List.repeat (Byte Byte.zero) n0).
     apply Mem.loadbytes_concat.
     eapply Mem.loadbytes_unchanged_on with (P := fun b1 ofs1 => ofs1 = p).
-    eapply store_zeros_unchanged; eauto. intros; omega.
-    intros; omega.
+    eapply store_zeros_unchanged; eauto. intros; lia.
+    intros; lia.
     replace (Byte Byte.zero :: nil) with (encode_val Mint8unsigned Vzero).
     change 1 with (size_chunk Mint8unsigned).
     eapply Mem.loadbytes_store_same; eauto.
     unfold encode_val; unfold encode_int; unfold rev_if_be; destruct Archi.big_endian; reflexivity.
-    eapply IHo; eauto. omega. omega. omega. omega.
-  + eapply IHo; eauto. omega. omega.
+    eapply IHo; eauto. lia. lia. lia. lia.
+  + eapply IHo; eauto. lia. lia.
 - discriminate.
 Qed.
 
@@ -924,11 +925,11 @@ Definition bytes_of_init_data (i: init_data): list memval :=
   | Init_int64 n => inj_bytes (encode_int 8%nat (Int64.unsigned n))
   | Init_float32 n => inj_bytes (encode_int 4%nat (Int.unsigned (Float32.to_bits n)))
   | Init_float64 n => inj_bytes (encode_int 8%nat (Int64.unsigned (Float.to_bits n)))
-  | Init_space n => list_repeat (Z.to_nat n) (Byte Byte.zero)
+  | Init_space n => List.repeat (Byte Byte.zero) (Z.to_nat n)
   | Init_addrof id ofs =>
       match find_symbol ge id with
       | Some b => inj_value (if Archi.ptr64 then Q64 else Q32) (Vptr b ofs)
-      | None   => list_repeat (if Archi.ptr64 then 8%nat else 4%nat) Undef
+      | None   => List.repeat Undef (if Archi.ptr64 then 8%nat else 4%nat)
       end
   end.
 
@@ -947,8 +948,8 @@ Proof.
   intros; destruct i; simpl in H; try apply (Mem.loadbytes_store_same _ _ _ _ _ _ H).
 - inv H. simpl.
   assert (EQ: Z.of_nat (Z.to_nat z) = Z.max z 0).
-  { destruct (zle 0 z). rewrite Z2Nat.id; xomega. destruct z; try discriminate. simpl. xomega. }
-  rewrite <- EQ. apply H0. omega. simpl. omega.
+  { destruct (zle 0 z). rewrite Z2Nat.id; extlia. destruct z; try discriminate. simpl. extlia. }
+  rewrite <- EQ. apply H0. lia. simpl. lia.
 - rewrite init_data_size_addrof. simpl.
   destruct (find_symbol ge i) as [b'|]; try discriminate.
   rewrite (Mem.loadbytes_store_same _ _ _ _ _ _ H).
@@ -968,23 +969,23 @@ Lemma store_init_data_list_loadbytes:
   Mem.loadbytes m' b p (init_data_list_size il) = Some (bytes_of_init_data_list il).
 Proof.
   induction il as [ | i1 il]; simpl; intros.
-- apply Mem.loadbytes_empty. omega.
+- apply Mem.loadbytes_empty. lia.
 - generalize (init_data_size_pos i1) (init_data_list_size_pos il); intros P1 PL.
   destruct (store_init_data m b p i1) as [m1|] eqn:S; try discriminate.
   apply Mem.loadbytes_concat.
   eapply Mem.loadbytes_unchanged_on with (P := fun b1 ofs1 => ofs1 < p + init_data_size i1).
   eapply store_init_data_list_unchanged; eauto.
-  intros; omega.
-  intros; omega.
+  intros; lia.
+  intros; lia.
   eapply store_init_data_loadbytes; eauto.
-  red; intros; apply H0. omega. omega.
+  red; intros; apply H0. lia. lia.
   apply IHil with m1; auto.
   red; intros.
   eapply Mem.loadbytes_unchanged_on with (P := fun b1 ofs1 => p + init_data_size i1 <= ofs1).
   eapply store_init_data_unchanged; eauto.
-  intros; omega.
-  intros; omega.
-  apply H0. omega. omega.
+  intros; lia.
+  intros; lia.
+  apply H0. lia. lia.
   auto. auto.
 Qed.
 
@@ -1011,7 +1012,7 @@ Remark read_as_zero_unchanged:
   read_as_zero m' b ofs len.
 Proof.
   intros; red; intros. eapply Mem.load_unchanged_on; eauto.
-  intros; apply H1. omega.
+  intros; apply H1. lia.
 Qed.
 
 Lemma store_zeros_read_as_zero:
@@ -1020,7 +1021,7 @@ Lemma store_zeros_read_as_zero:
   read_as_zero m' b p n.
 Proof.
   intros; red; intros.
-  transitivity (Some(decode_val chunk (list_repeat (size_chunk_nat chunk) (Byte Byte.zero)))).
+  transitivity (Some(decode_val chunk (List.repeat (Byte Byte.zero) (size_chunk_nat chunk)))).
   apply Mem.loadbytes_load; auto. rewrite size_chunk_conv.
   eapply store_zeros_loadbytes; eauto. rewrite <- size_chunk_conv; auto.
   f_equal. destruct chunk; unfold decode_val; unfold decode_int; unfold rev_if_be; destruct Archi.big_endian; reflexivity.
@@ -1068,7 +1069,7 @@ Proof.
   {
     intros.
     eapply Mem.load_unchanged_on with (P := fun b' ofs' => ofs' < p + size_chunk chunk).
-    eapply store_init_data_list_unchanged; eauto. intros; omega.
+    eapply store_init_data_list_unchanged; eauto. intros; lia.
     intros; tauto.
     eapply Mem.load_store_same; eauto.
   }
@@ -1078,10 +1079,10 @@ Proof.
   exploit IHil; eauto.
   set (P := fun (b': block) ofs' => p + init_data_size a <= ofs').
   apply read_as_zero_unchanged with (m := m) (P := P).
-  red; intros; apply H0; auto. generalize (init_data_size_pos a); omega. omega.
+  red; intros; apply H0; auto. generalize (init_data_size_pos a); lia. lia.
   eapply store_init_data_unchanged with (P := P); eauto.
-  intros; unfold P. omega.
-  intros; unfold P. omega.
+  intros; unfold P. lia.
+  intros; unfold P. lia.
   intro D.
   destruct a; simpl in Heqo.
 + split; auto. eapply (A Mint8unsigned (Vint i)); eauto.
@@ -1093,10 +1094,10 @@ Proof.
 + split; auto.
   set (P := fun (b': block) ofs' => ofs' < p + init_data_size (Init_space z)).
   inv Heqo. apply read_as_zero_unchanged with (m := m1) (P := P).
-  red; intros. apply H0; auto. simpl. generalize (init_data_list_size_pos il); xomega.
+  red; intros. apply H0; auto. simpl. generalize (init_data_list_size_pos il); extlia.
   eapply store_init_data_list_unchanged; eauto.
-  intros; unfold P. omega.
-  intros; unfold P. simpl; xomega.
+  intros; unfold P. lia.
+  intros; unfold P. simpl; extlia.
 + rewrite init_data_size_addrof in *.
   split; auto.
   destruct (find_symbol ge i); try congruence.
@@ -1195,11 +1196,11 @@ Proof.
 * destruct (Mem.alloc m 0 1) as [m1 b] eqn:ALLOC.
   exploit Mem.alloc_result; eauto. intros RES.
   rewrite H, <- RES. split.
-  eapply Mem.perm_drop_1; eauto. omega.
+  eapply Mem.perm_drop_1; eauto. lia.
   intros.
   assert (0 <= ofs < 1). { eapply Mem.perm_alloc_3; eauto. eapply Mem.perm_drop_4; eauto. }
   exploit Mem.perm_drop_2; eauto. intros ORD.
-  split. omega. inv ORD; auto.
+  split. lia. inv ORD; auto.
 * set (init := gvar_init v) in *.
   set (sz := init_data_list_size init) in *.
   destruct (Mem.alloc m 0 sz) as [m1 b] eqn:?.
@@ -1442,7 +1443,7 @@ Proof.
   exploit alloc_global_neutral; eauto.
   assert (Ple (Pos.succ (Mem.nextblock m)) (Mem.nextblock m')).
   { rewrite EQ. apply advance_next_le. }
-  unfold Plt, Ple in *; zify; omega.
+  unfold Plt, Ple in *; zify; lia.
 Qed.
 
 End INITMEM_INJ.
@@ -1563,9 +1564,9 @@ Lemma store_zeros_exists:
 Proof.
   intros until n. functional induction (store_zeros m b p n); intros PERM.
 - exists m; auto.
-- apply IHo. red; intros. eapply Mem.perm_store_1; eauto. apply PERM. omega.
+- apply IHo. red; intros. eapply Mem.perm_store_1; eauto. apply PERM. lia.
 - destruct (Mem.valid_access_store m Mint8unsigned b p Vzero) as (m' & STORE).
-  split. red; intros. apply Mem.perm_cur. apply PERM. simpl in H. omega.
+  split. red; intros. apply Mem.perm_cur. apply PERM. simpl in H. lia.
   simpl. apply Z.divide_1_l.
   congruence.
 Qed.
@@ -1603,10 +1604,10 @@ Proof.
 - exists m; auto.
 - destruct H0.
   destruct (@store_init_data_exists m b p i1) as (m1 & S1); eauto.
-  red; intros. apply H. generalize (init_data_list_size_pos il); omega.
+  red; intros. apply H. generalize (init_data_list_size_pos il); lia.
   rewrite S1.
   apply IHil; eauto.
-  red; intros. erewrite <- store_init_data_perm by eauto. apply H. generalize (init_data_size_pos i1); omega.
+  red; intros. erewrite <- store_init_data_perm by eauto. apply H. generalize (init_data_size_pos i1); lia.
 Qed.
 
 Lemma alloc_global_exists:
diff --git a/common/Linking.v b/common/Linking.v
index ec828ea4..089f4fd2 100644
--- a/common/Linking.v
+++ b/common/Linking.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
@@ -123,7 +124,7 @@ Defined.
 Next Obligation.
   inv H; inv H0; constructor; auto.
   congruence.
-  simpl. generalize (init_data_list_size_pos z). xomega.
+  simpl. generalize (init_data_list_size_pos z). extlia.
 Defined.
 Next Obligation.
   revert H; unfold link_varinit.
diff --git a/common/Memdata.v b/common/Memdata.v
index a09b90f5..c80b3754 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -7,10 +7,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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
@@ -23,6 +24,7 @@ Require Import AST.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
+Require Import Lia.
 
 (** * Properties of memory chunks *)
 
@@ -48,13 +50,13 @@ Definition largest_size_chunk := 8.
 
 Lemma max_size_chunk: forall chunk, size_chunk chunk <= 8.
 Proof.
-  destruct chunk; simpl; omega.
+  destruct chunk; simpl; lia.
 Qed.
 
 Lemma size_chunk_pos:
   forall chunk, size_chunk chunk > 0.
 Proof.
-  intros. destruct chunk; simpl; omega.
+  intros. destruct chunk; simpl; lia.
 Qed.
 
 Definition size_chunk_nat (chunk: memory_chunk) : nat :=
@@ -72,7 +74,7 @@ Proof.
   intros.
   generalize (size_chunk_pos chunk). rewrite size_chunk_conv.
   destruct (size_chunk_nat chunk).
-  simpl; intros; omegaContradiction.
+  simpl; intros; extlia.
   intros; exists n; auto.
 Qed.
 
@@ -108,7 +110,7 @@ Definition align_chunk (chunk: memory_chunk) : Z :=
 Lemma align_chunk_pos:
   forall chunk, align_chunk chunk > 0.
 Proof.
-  intro. destruct chunk; simpl; omega.
+  intro. destruct chunk; simpl; lia.
 Qed.
 
 Lemma align_chunk_Mptr: align_chunk Mptr = if Archi.ptr64 then 8 else 4.
@@ -127,7 +129,7 @@ Lemma align_le_divides:
   align_chunk chunk1 <= align_chunk chunk2 -> (align_chunk chunk1 | align_chunk chunk2).
 Proof.
   intros. destruct chunk1; destruct chunk2; simpl in *;
-  solve [ omegaContradiction
+  solve [ extlia
         | apply Z.divide_refl
         | exists 2; reflexivity
         | exists 4; reflexivity
@@ -223,12 +225,12 @@ Proof.
   simpl. rewrite Zmod_1_r. auto.
 Opaque Byte.wordsize.
   rewrite Nat2Z.inj_succ. simpl.
-  replace (Z.succ (Z.of_nat n) * 8) with (Z.of_nat n * 8 + 8) by omega.
-  rewrite two_p_is_exp; try omega.
+  replace (Z.succ (Z.of_nat n) * 8) with (Z.of_nat n * 8 + 8) by lia.
+  rewrite two_p_is_exp; try lia.
   rewrite Zmod_recombine. rewrite IHn. rewrite Z.add_comm.
   change (Byte.unsigned (Byte.repr x)) with (Byte.Z_mod_modulus x).
   rewrite Byte.Z_mod_modulus_eq. reflexivity.
-  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.
 
 Lemma rev_if_be_involutive:
@@ -287,15 +289,15 @@ Proof.
   intros; simpl; auto.
   intros until y.
   rewrite Nat2Z.inj_succ.
-  replace (Z.succ (Z.of_nat n) * 8) with (Z.of_nat n * 8 + 8) by omega.
-  rewrite two_p_is_exp; try omega.
+  replace (Z.succ (Z.of_nat n) * 8) with (Z.of_nat n * 8 + 8) by lia.
+  rewrite two_p_is_exp; try lia.
   intro EQM.
   simpl; decEq.
   apply Byte.eqm_samerepr. red.
   eapply eqmod_divides; eauto. apply Z.divide_factor_r.
   apply IHn.
   destruct EQM as [k EQ]. exists k. rewrite EQ.
-  rewrite <- Z_div_plus_full_l. decEq. change (two_p 8) with 256. ring. omega.
+  rewrite <- Z_div_plus_full_l. decEq. change (two_p 8) with 256. ring. lia.
 Qed.
 
 Lemma encode_int_8_mod:
@@ -378,14 +380,14 @@ Definition encode_val (chunk: memory_chunk) (v: val) : list memval :=
   | Vint n, (Mint8signed | Mint8unsigned) => inj_bytes (encode_int 1%nat (Int.unsigned n))
   | Vint n, (Mint16signed | Mint16unsigned) => inj_bytes (encode_int 2%nat (Int.unsigned n))
   | Vint n, Mint32 => inj_bytes (encode_int 4%nat (Int.unsigned n))
-  | Vptr b ofs, Mint32 => if Archi.ptr64 then list_repeat 4%nat Undef else inj_value Q32 v
+  | Vptr b ofs, Mint32 => if Archi.ptr64 then List.repeat Undef 4%nat else inj_value Q32 v
   | Vlong n, Mint64 => inj_bytes (encode_int 8%nat (Int64.unsigned n))
-  | Vptr b ofs, Mint64 => if Archi.ptr64 then inj_value Q64 v else list_repeat 8%nat Undef
+  | Vptr b ofs, Mint64 => if Archi.ptr64 then inj_value Q64 v else List.repeat Undef 8%nat
   | Vsingle n, Mfloat32 => inj_bytes (encode_int 4%nat (Int.unsigned (Float32.to_bits n)))
   | Vfloat n, Mfloat64 => inj_bytes (encode_int 8%nat (Int64.unsigned (Float.to_bits n)))
   | _, Many32 => inj_value Q32 v
   | _, Many64 => inj_value Q64 v
-  | _, _ => list_repeat (size_chunk_nat chunk) Undef
+  | _, _ => List.repeat Undef (size_chunk_nat chunk)
   end.
 
 Definition decode_val (chunk: memory_chunk) (vl: list memval) : val :=
@@ -524,9 +526,9 @@ Ltac solve_decode_encode_val_general :=
   | |- context [ Int.repr(decode_int (encode_int 2 (Int.unsigned _))) ] => rewrite decode_encode_int_2
   | |- context [ Int.repr(decode_int (encode_int 4 (Int.unsigned _))) ] => rewrite decode_encode_int_4
   | |- context [ Int64.repr(decode_int (encode_int 8 (Int64.unsigned _))) ] => rewrite decode_encode_int_8
-  | |- Vint (Int.sign_ext _ (Int.sign_ext _ _)) = Vint _ => f_equal; apply Int.sign_ext_idem; omega
-  | |- Vint (Int.zero_ext _ (Int.zero_ext _ _)) = Vint _ => f_equal; apply Int.zero_ext_idem; omega
-  | |- Vint (Int.sign_ext _ (Int.zero_ext _ _)) = Vint _ => f_equal; apply Int.sign_ext_zero_ext; omega
+  | |- Vint (Int.sign_ext _ (Int.sign_ext _ _)) = Vint _ => f_equal; apply Int.sign_ext_idem; lia
+  | |- Vint (Int.zero_ext _ (Int.zero_ext _ _)) = Vint _ => f_equal; apply Int.zero_ext_idem; lia
+  | |- Vint (Int.sign_ext _ (Int.zero_ext _ _)) = Vint _ => f_equal; apply Int.sign_ext_zero_ext; lia
   end.
 
 Lemma decode_encode_val_general:
@@ -550,7 +552,7 @@ Lemma decode_encode_val_similar:
   v2 = Val.load_result chunk2 v1.
 Proof.
   intros until v2; intros TY SZ DE.
-  destruct chunk1; destruct chunk2; simpl in TY; try discriminate; simpl in SZ; try omegaContradiction;
+  destruct chunk1; destruct chunk2; simpl in TY; try discriminate; simpl in SZ; try extlia;
   destruct v1; auto.
 Qed.
 
@@ -560,7 +562,7 @@ Lemma decode_val_rettype:
 Proof.
   intros. unfold decode_val.
   destruct (proj_bytes cl).
-- destruct chunk; simpl; rewrite ? Int.sign_ext_idem, ? Int.zero_ext_idem by omega; auto.
+- destruct chunk; simpl; rewrite ? Int.sign_ext_idem, ? Int.zero_ext_idem by lia; auto.
 - Local Opaque Val.load_result.
   destruct chunk; simpl;
   (exact I || apply Val.load_result_type || destruct Archi.ptr64; (exact I || apply Val.load_result_type)).
@@ -660,7 +662,7 @@ Proof.
              exists j, mv = Fragment v q j /\ S j <> size_quantity_nat q).
   {
     induction n; simpl; intros. contradiction. destruct H0.
-    exists n; split; auto. omega. apply IHn; auto. omega.
+    exists n; split; auto. lia. apply IHn; auto. lia.
   }
   assert (B: forall q,
              q = quantity_chunk chunk ->
@@ -670,7 +672,7 @@ Proof.
 Local Transparent inj_value.
     intros. unfold inj_value. destruct (size_quantity_nat_pos q) as [sz' EQ'].
     rewrite EQ'. simpl. constructor; auto.
-    intros; eapply A; eauto. omega.
+    intros; eapply A; eauto. lia.
   }
   assert (C: forall bl,
              match v with Vint _ => True | Vlong _ => True | Vfloat _ => True | Vsingle _ => True | _ => False end ->
@@ -681,10 +683,10 @@ Local Transparent inj_value.
     constructor; auto. unfold inj_bytes; intros. exploit list_in_map_inv; eauto.
     intros (b & P & Q); exists b; auto.
   }
-  assert (D: shape_encoding chunk v (list_repeat (size_chunk_nat chunk) Undef)).
+  assert (D: shape_encoding chunk v (List.repeat Undef (size_chunk_nat chunk))).
   {
     intros. rewrite EQ; simpl; constructor; auto.
-    intros. eapply in_list_repeat; eauto.
+    intros. eapply repeat_spec; eauto.
   }
   generalize (encode_val_length chunk v). intros LEN.
   unfold encode_val; unfold encode_val in LEN;
@@ -726,8 +728,8 @@ Proof.
     induction n; destruct mvs; simpl; intros; try discriminate.
     contradiction.
     destruct m; try discriminate. InvBooleans. apply beq_nat_true in H4. subst.
-    destruct H0. subst mv. exists n0; split; auto. omega.
-    eapply IHn; eauto. omega.
+    destruct H0. subst mv. exists n0; split; auto. lia.
+    eapply IHn; eauto. lia.
   }
   assert (U: forall mvs, shape_decoding chunk mvs (Val.load_result chunk Vundef)).
   {
@@ -747,7 +749,7 @@ Proof.
     simpl. apply beq_nat_true in EQN. subst n q0. constructor. auto.
     destruct H0 as [E|[E|[E|E]]]; subst chunk; destruct q; auto || discriminate.
     congruence.
-    intros. eapply B; eauto. omega.
+    intros. eapply B; eauto. lia.
   }
   unfold decode_val.
   destruct (proj_bytes (mv1 :: mvl)) as [bl|] eqn:PB.
@@ -889,21 +891,21 @@ Qed.
 
 Lemma repeat_Undef_inject_any:
   forall f vl,
-  list_forall2 (memval_inject f) (list_repeat (length vl) Undef) vl.
+  list_forall2 (memval_inject f) (List.repeat Undef (length vl)) vl.
 Proof.
   induction vl; simpl; constructor; auto. constructor.
 Qed.
 
 Lemma repeat_Undef_inject_encode_val:
   forall f chunk v,
-  list_forall2 (memval_inject f) (list_repeat (size_chunk_nat chunk) Undef) (encode_val chunk v).
+  list_forall2 (memval_inject f) (List.repeat Undef (size_chunk_nat chunk)) (encode_val chunk v).
 Proof.
   intros. rewrite <- (encode_val_length chunk v). apply repeat_Undef_inject_any.
 Qed.
 
 Lemma repeat_Undef_inject_self:
   forall f n,
-  list_forall2 (memval_inject f) (list_repeat n Undef) (list_repeat n Undef).
+  list_forall2 (memval_inject f) (List.repeat Undef n) (List.repeat Undef n).
 Proof.
   induction n; simpl; constructor; auto. constructor.
 Qed.
@@ -922,7 +924,7 @@ Theorem encode_val_inject:
   Val.inject f v1 v2 ->
   list_forall2 (memval_inject f) (encode_val chunk v1) (encode_val chunk v2).
 Proof.
-Local Opaque list_repeat.
+Local Opaque List.repeat.
   intros. inversion H; subst; simpl; destruct chunk;
   auto using inj_bytes_inject, inj_value_inject, repeat_Undef_inject_self, repeat_Undef_inject_encode_val.
 - destruct Archi.ptr64; auto using inj_value_inject, repeat_Undef_inject_self.
@@ -962,22 +964,22 @@ Proof.
   induction l1; simpl int_of_bytes; intros.
   simpl. ring.
   simpl length. rewrite Nat2Z.inj_succ.
-  replace (Z.succ (Z.of_nat (length l1)) * 8) with (Z.of_nat (length l1) * 8 + 8) by omega.
+  replace (Z.succ (Z.of_nat (length l1)) * 8) with (Z.of_nat (length l1) * 8 + 8) by lia.
   rewrite two_p_is_exp. change (two_p 8) with 256. rewrite IHl1. ring.
-  omega. omega.
+  lia. lia.
 Qed.
 
 Lemma int_of_bytes_range:
   forall l, 0 <= int_of_bytes l < two_p (Z.of_nat (length l) * 8).
 Proof.
   induction l; intros.
-  simpl. omega.
+  simpl. lia.
   simpl length. rewrite Nat2Z.inj_succ.
-  replace (Z.succ (Z.of_nat (length l)) * 8) with (Z.of_nat (length l) * 8 + 8) by omega.
+  replace (Z.succ (Z.of_nat (length l)) * 8) with (Z.of_nat (length l) * 8 + 8) by lia.
   rewrite two_p_is_exp. change (two_p 8) with 256.
   simpl int_of_bytes. generalize (Byte.unsigned_range a).
-  change Byte.modulus with 256. omega.
-  omega. omega.
+  change Byte.modulus with 256. lia.
+  lia. lia.
 Qed.
 
 Lemma length_proj_bytes:
@@ -1021,7 +1023,7 @@ Proof.
     intros. apply Int.unsigned_repr.
     generalize (int_of_bytes_range l). rewrite H2.
     change (two_p (Z.of_nat 4 * 8)) with (Int.max_unsigned + 1).
-    omega.
+    lia.
   apply Val.lessdef_same.
   unfold decode_int, rev_if_be. destruct Archi.big_endian; rewrite B1; rewrite B2.
   + rewrite <- (rev_length b1) in L1.
@@ -1043,18 +1045,18 @@ Lemma bytes_of_int_append:
   bytes_of_int n1 x1 ++ bytes_of_int n2 x2.
 Proof.
   induction n1; intros.
-- simpl in *. f_equal. omega.
+- simpl in *. f_equal. lia.
 - assert (E: two_p (Z.of_nat (S n1) * 8) = two_p (Z.of_nat n1 * 8) * 256).
   {
     rewrite Nat2Z.inj_succ. change 256 with (two_p 8). rewrite <- two_p_is_exp.
-    f_equal. omega. omega. omega.
+    f_equal. lia. lia. lia.
   }
   rewrite E in *. simpl. f_equal.
   apply Byte.eqm_samerepr. exists (x2 * two_p (Z.of_nat n1 * 8)).
   change Byte.modulus with 256. ring.
   rewrite Z.mul_assoc. rewrite Z_div_plus. apply IHn1.
-  apply Zdiv_interval_1. omega. apply two_p_gt_ZERO; omega. omega.
-  assumption. omega.
+  apply Zdiv_interval_1. lia. apply two_p_gt_ZERO; lia. lia.
+  assumption. lia.
 Qed.
 
 Lemma bytes_of_int64:
diff --git a/common/Memory.v b/common/Memory.v
index 65f36966..bf8ca083 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -9,10 +9,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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
@@ -212,11 +213,11 @@ Proof.
   induction lo using (well_founded_induction_type (Zwf_up_well_founded hi)).
   destruct (zlt lo hi).
   destruct (perm_dec m b lo k p).
-  destruct (H (lo + 1)). red. omega.
-  left; red; intros. destruct (zeq lo ofs). congruence. apply r. omega.
-  right; red; intros. elim n. red; intros; apply H0; omega.
-  right; red; intros. elim n. apply H0. omega.
-  left; red; intros. omegaContradiction.
+  destruct (H (lo + 1)). red. lia.
+  left; red; intros. destruct (zeq lo ofs). congruence. apply r. lia.
+  right; red; intros. elim n. red; intros; apply H0; lia.
+  right; red; intros. elim n. apply H0. lia.
+  left; red; intros. extlia.
 Defined.
 
 (** [valid_access m chunk b ofs p] holds if a memory access
@@ -257,7 +258,7 @@ Theorem valid_access_valid_block:
 Proof.
   intros. destruct H.
   assert (perm m b ofs Cur Nonempty).
-    apply H. generalize (size_chunk_pos chunk). omega.
+    apply H. generalize (size_chunk_pos chunk). lia.
   eauto with mem.
 Qed.
 
@@ -268,7 +269,7 @@ Lemma valid_access_perm:
   valid_access m chunk b ofs p ->
   perm m b ofs k p.
 Proof.
-  intros. destruct H. apply perm_cur. apply H. generalize (size_chunk_pos chunk). omega.
+  intros. destruct H. apply perm_cur. apply H. generalize (size_chunk_pos chunk). lia.
 Qed.
 
 Lemma valid_access_compat:
@@ -314,9 +315,9 @@ Theorem valid_pointer_valid_access:
 Proof.
   intros. rewrite valid_pointer_nonempty_perm.
   split; intros.
-  split. simpl; red; intros. replace ofs0 with ofs by omega. auto.
+  split. simpl; red; intros. replace ofs0 with ofs by lia. auto.
   simpl. apply Z.divide_1_l.
-  destruct H. apply H. simpl. omega.
+  destruct H. apply H. simpl. lia.
 Qed.
 
 (** C allows pointers one past the last element of an array.  These are not
@@ -486,8 +487,8 @@ Proof.
   auto.
   simpl length in H. rewrite Nat2Z.inj_succ in H.
   transitivity (ZMap.get q (ZMap.set p a c)).
-  apply IHvl. intros. apply H. omega.
-  apply ZMap.gso. apply not_eq_sym. apply H. omega.
+  apply IHvl. intros. apply H. lia.
+  apply ZMap.gso. apply not_eq_sym. apply H. lia.
 Qed.
 
 Remark setN_outside:
@@ -496,7 +497,7 @@ Remark setN_outside:
   ZMap.get q (setN vl p c) = ZMap.get q c.
 Proof.
   intros. apply setN_other.
-  intros. omega.
+  intros. lia.
 Qed.
 
 Remark getN_setN_same:
@@ -506,7 +507,7 @@ Proof.
   induction vl; intros; simpl.
   auto.
   decEq.
-  rewrite setN_outside. apply ZMap.gss. omega.
+  rewrite setN_outside. apply ZMap.gss. lia.
   apply IHvl.
 Qed.
 
@@ -516,7 +517,7 @@ Remark getN_exten:
   getN n p c1 = getN n p c2.
 Proof.
   induction n; intros. auto. rewrite Nat2Z.inj_succ in H. simpl. decEq.
-  apply H. omega. apply IHn. intros. apply H. omega.
+  apply H. lia. apply IHn. intros. apply H. lia.
 Qed.
 
 Remark getN_setN_disjoint:
@@ -682,7 +683,7 @@ Qed.
 Theorem valid_access_empty: forall chunk b ofs p, ~valid_access empty chunk b ofs p.
 Proof.
   intros. red; intros. elim (perm_empty b ofs Cur p). apply H.
-  generalize (size_chunk_pos chunk); omega.
+  generalize (size_chunk_pos chunk); lia.
 Qed.
 
 (** ** Properties related to [load] *)
@@ -847,7 +848,7 @@ Theorem loadbytes_empty:
   n <= 0 -> loadbytes m b ofs n = Some nil.
 Proof.
   intros. unfold loadbytes. rewrite pred_dec_true. rewrite Z_to_nat_neg; auto.
-  red; intros. omegaContradiction.
+  red; intros. extlia.
 Qed.
 
 Lemma getN_concat:
@@ -855,9 +856,9 @@ Lemma getN_concat:
   getN (n1 + n2)%nat p c = getN n1 p c ++ getN n2 (p + Z.of_nat n1) c.
 Proof.
   induction n1; intros.
-  simpl. decEq. omega.
+  simpl. decEq. lia.
   rewrite Nat2Z.inj_succ. simpl. decEq.
-  replace (p + Z.succ (Z.of_nat n1)) with ((p + 1) + Z.of_nat n1) by omega.
+  replace (p + Z.succ (Z.of_nat n1)) with ((p + 1) + Z.of_nat n1) by lia.
   auto.
 Qed.
 
@@ -871,12 +872,12 @@ Proof.
   unfold loadbytes; intros.
   destruct (range_perm_dec m b ofs (ofs + n1) Cur Readable); try congruence.
   destruct (range_perm_dec m b (ofs + n1) (ofs + n1 + n2) Cur Readable); try congruence.
-  rewrite pred_dec_true. rewrite Z2Nat.inj_add by omega.
-  rewrite getN_concat. rewrite Z2Nat.id by omega.
+  rewrite pred_dec_true. rewrite Z2Nat.inj_add by lia.
+  rewrite getN_concat. rewrite Z2Nat.id by lia.
   congruence.
   red; intros.
-  assert (ofs0 < ofs + n1 \/ ofs0 >= ofs + n1) by omega.
-  destruct H4. apply r; omega. apply r0; omega.
+  assert (ofs0 < ofs + n1 \/ ofs0 >= ofs + n1) by lia.
+  destruct H4. apply r; lia. apply r0; lia.
 Qed.
 
 Theorem loadbytes_split:
@@ -891,13 +892,13 @@ Proof.
   unfold loadbytes; intros.
   destruct (range_perm_dec m b ofs (ofs + (n1 + n2)) Cur Readable);
   try congruence.
-  rewrite Z2Nat.inj_add in H by omega. rewrite getN_concat in H.
-  rewrite Z2Nat.id in H by omega.
+  rewrite Z2Nat.inj_add in H by lia. rewrite getN_concat in H.
+  rewrite Z2Nat.id in H by lia.
   repeat rewrite pred_dec_true.
   econstructor; econstructor.
   split. reflexivity. split. reflexivity. congruence.
-  red; intros; apply r; omega.
-  red; intros; apply r; omega.
+  red; intros; apply r; lia.
+  red; intros; apply r; lia.
 Qed.
 
 Theorem load_rep:
@@ -917,13 +918,13 @@ Proof.
   revert ofs H; induction n; intros; simpl; auto.
   f_equal.
   rewrite Nat2Z.inj_succ in H.
-  replace ofs with (ofs+0) by omega.
-  apply H; omega.
+  replace ofs with (ofs+0) by lia.
+  apply H; lia.
   apply IHn.
   intros.
   rewrite <- Z.add_assoc.
   apply H.
-  rewrite Nat2Z.inj_succ. omega.
+  rewrite Nat2Z.inj_succ. lia.
 Qed.
 
 Theorem load_int64_split:
@@ -938,7 +939,7 @@ Proof.
   exploit load_valid_access; eauto. intros [A B]. simpl in *.
   exploit load_loadbytes. eexact H. simpl. intros [bytes [LB EQ]].
   change 8 with (4 + 4) in LB.
-  exploit loadbytes_split. eexact LB. omega. omega.
+  exploit loadbytes_split. eexact LB. lia. lia.
   intros (bytes1 & bytes2 & LB1 & LB2 & APP).
   change 4 with (size_chunk Mint32) in LB1.
   exploit loadbytes_load. eexact LB1.
@@ -970,11 +971,11 @@ Proof.
   change (Int.unsigned (Int.repr 4)) with 4.
   apply Ptrofs.unsigned_repr.
   exploit (Zdivide_interval (Ptrofs.unsigned i) Ptrofs.modulus 8).
-  omega. apply Ptrofs.unsigned_range. auto.
+  lia. apply Ptrofs.unsigned_range. auto.
   exists (two_p (Ptrofs.zwordsize - 3)).
   unfold Ptrofs.modulus, Ptrofs.zwordsize, Ptrofs.wordsize.
   unfold Wordsize_Ptrofs.wordsize. destruct Archi.ptr64; reflexivity.
-  unfold Ptrofs.max_unsigned. omega.
+  unfold Ptrofs.max_unsigned. lia.
 Qed.
 
 Theorem loadv_int64_split:
@@ -1131,7 +1132,7 @@ Qed.
 Theorem load_store_same:
   load chunk m2 b ofs = Some (Val.load_result chunk v).
 Proof.
-  apply load_store_similar_2; auto. omega.
+  apply load_store_similar_2; auto. lia.
 Qed.
 
 Theorem load_store_other:
@@ -1183,9 +1184,9 @@ Proof.
   destruct H. congruence.
   destruct (zle n 0) as [z | n0].
   rewrite (Z_to_nat_neg _ z). auto.
-  destruct H. omegaContradiction.
+  destruct H. extlia.
   apply getN_setN_outside. rewrite encode_val_length. rewrite <- size_chunk_conv.
-  rewrite Z2Nat.id. auto. omega.
+  rewrite Z2Nat.id. auto. lia.
   auto.
   red; intros. eauto with mem.
   rewrite pred_dec_false. auto.
@@ -1198,11 +1199,11 @@ Lemma setN_in:
   In (ZMap.get q (setN vl p c)) vl.
 Proof.
   induction vl; intros.
-  simpl in H. omegaContradiction.
+  simpl in H. extlia.
   simpl length in H. rewrite Nat2Z.inj_succ in H. simpl.
   destruct (zeq p q). subst q. rewrite setN_outside. rewrite ZMap.gss.
-  auto with coqlib. omega.
-  right. apply IHvl. omega.
+  auto with coqlib. lia.
+  right. apply IHvl. lia.
 Qed.
 
 Lemma getN_in:
@@ -1211,10 +1212,10 @@ Lemma getN_in:
   In (ZMap.get q c) (getN n p c).
 Proof.
   induction n; intros.
-  simpl in H; omegaContradiction.
+  simpl in H; extlia.
   rewrite Nat2Z.inj_succ in H. simpl. destruct (zeq p q).
   subst q. auto.
-  right. apply IHn. omega.
+  right. apply IHn. lia.
 Qed.
 
 End STORE.
@@ -1363,28 +1364,28 @@ Proof.
   split. rewrite V', SIZE'. apply decode_val_shape.
   destruct (zeq ofs' ofs).
 - subst ofs'. left; split. auto. unfold c'. simpl.
-  rewrite setN_outside by omega. apply ZMap.gss.
+  rewrite setN_outside by lia. apply ZMap.gss.
 - right. destruct (zlt ofs ofs').
 (* If ofs < ofs':  the load reads (at ofs') a continuation byte from the write.
        ofs   ofs'   ofs+|chunk|
         [-------------------]       write
              [-------------------]  read
 *)
-+ left; split. omega. unfold c'. simpl. apply setN_in.
++ left; split. lia. unfold c'. simpl. apply setN_in.
   assert (Z.of_nat (length (mv1 :: mvl)) = size_chunk chunk).
   { rewrite <- ENC; rewrite encode_val_length. rewrite size_chunk_conv; auto. }
-  simpl length in H3. rewrite Nat2Z.inj_succ in H3. omega.
+  simpl length in H3. rewrite Nat2Z.inj_succ in H3. lia.
 (* If ofs > ofs':  the load reads (at ofs) the first byte from the write.
        ofs'   ofs   ofs'+|chunk'|
                [-------------------]  write
          [----------------]           read
 *)
-+ right; split. omega. replace mv1 with (ZMap.get ofs c').
++ right; split. lia. replace mv1 with (ZMap.get ofs c').
   apply getN_in.
   assert (size_chunk chunk' = Z.succ (Z.of_nat sz')).
   { rewrite size_chunk_conv. rewrite SIZE'. rewrite Nat2Z.inj_succ; auto. }
-  omega.
-  unfold c'. simpl. rewrite setN_outside by omega. apply ZMap.gss.
+  lia.
+  unfold c'. simpl. rewrite setN_outside by lia. apply ZMap.gss.
 Qed.
 
 Definition compat_pointer_chunks (chunk1 chunk2: memory_chunk) : Prop :=
@@ -1471,10 +1472,10 @@ Theorem load_store_pointer_mismatch:
 Proof.
   intros.
   exploit load_store_overlap; eauto.
-  generalize (size_chunk_pos chunk'); omega.
-  generalize (size_chunk_pos chunk); omega.
+  generalize (size_chunk_pos chunk'); lia.
+  generalize (size_chunk_pos chunk); lia.
   intros (mv1 & mvl & mv1' & mvl' & ENC & DEC & CASES).
-  destruct CASES as [(A & B) | [(A & B) | (A & B)]]; try omegaContradiction.
+  destruct CASES as [(A & B) | [(A & B) | (A & B)]]; try extlia.
   inv ENC; inv DEC; auto.
 - elim H1. apply compat_pointer_chunks_true; auto.
 - contradiction.
@@ -1496,8 +1497,8 @@ Proof.
   destruct (valid_access_dec m chunk1 b ofs Writable);
   destruct (valid_access_dec m chunk2 b ofs Writable); auto.
   f_equal. apply mkmem_ext; auto. congruence.
-  elim n. apply valid_access_compat with chunk1; auto. omega.
-  elim n. apply valid_access_compat with chunk2; auto. omega.
+  elim n. apply valid_access_compat with chunk1; auto. lia.
+  elim n. apply valid_access_compat with chunk2; auto. lia.
 Qed.
 
 Theorem store_signed_unsigned_8:
@@ -1543,7 +1544,7 @@ Proof.
   destruct (valid_access_dec m Mfloat64 b ofs Writable); try discriminate.
   destruct (valid_access_dec m Mfloat64al32 b ofs Writable).
   rewrite <- H. f_equal. apply mkmem_ext; auto.
-  elim n. apply valid_access_compat with Mfloat64; auto. simpl; omega.
+  elim n. apply valid_access_compat with Mfloat64; auto. simpl; lia.
 Qed.
 
 Theorem storev_float64al32:
@@ -1706,7 +1707,7 @@ Proof.
   rewrite pred_dec_true.
   rewrite storebytes_mem_contents. decEq.
   rewrite PMap.gsspec. destruct (peq b' b). subst b'.
-  apply getN_setN_disjoint. rewrite Z2Nat.id by omega. intuition congruence.
+  apply getN_setN_disjoint. rewrite Z2Nat.id by lia. intuition congruence.
   auto.
   red; auto with mem.
   apply pred_dec_false.
@@ -1751,8 +1752,8 @@ Lemma setN_concat:
   setN (bytes1 ++ bytes2) ofs c = setN bytes2 (ofs + Z.of_nat (length bytes1)) (setN bytes1 ofs c).
 Proof.
   induction bytes1; intros.
-  simpl. decEq. omega.
-  simpl length. rewrite Nat2Z.inj_succ. simpl. rewrite IHbytes1. decEq. omega.
+  simpl. decEq. lia.
+  simpl length. rewrite Nat2Z.inj_succ. simpl. rewrite IHbytes1. decEq. lia.
 Qed.
 
 Theorem storebytes_concat:
@@ -1771,8 +1772,8 @@ Proof.
   elim n.
   rewrite app_length. rewrite Nat2Z.inj_add. red; intros.
   destruct (zlt ofs0 (ofs + Z.of_nat(length bytes1))).
-  apply r. omega.
-  eapply perm_storebytes_2; eauto. apply r0. omega.
+  apply r. lia.
+  eapply perm_storebytes_2; eauto. apply r0. lia.
 Qed.
 
 Theorem storebytes_split:
@@ -1785,10 +1786,10 @@ Proof.
   intros.
   destruct (range_perm_storebytes m b ofs bytes1) as [m1 ST1].
   red; intros. exploit storebytes_range_perm; eauto. rewrite app_length.
-  rewrite Nat2Z.inj_add. omega.
+  rewrite Nat2Z.inj_add. lia.
   destruct (range_perm_storebytes m1 b (ofs + Z.of_nat (length bytes1)) bytes2) as [m2' ST2].
   red; intros. eapply perm_storebytes_1; eauto. exploit storebytes_range_perm.
-  eexact H. instantiate (1 := ofs0). rewrite app_length. rewrite Nat2Z.inj_add. omega.
+  eexact H. instantiate (1 := ofs0). rewrite app_length. rewrite Nat2Z.inj_add. lia.
   auto.
   assert (Some m2 = Some m2').
   rewrite <- H. eapply storebytes_concat; eauto.
@@ -1896,7 +1897,7 @@ Theorem perm_alloc_2:
 Proof.
   unfold perm; intros. injection ALLOC; intros. rewrite <- H1; simpl.
   subst b. rewrite PMap.gss. unfold proj_sumbool. rewrite zle_true.
-  rewrite zlt_true. simpl. auto with mem. omega. omega.
+  rewrite zlt_true. simpl. auto with mem. lia. lia.
 Qed.
 
 Theorem perm_alloc_inv:
@@ -1940,7 +1941,7 @@ Theorem valid_access_alloc_same:
   valid_access m2 chunk b ofs Freeable.
 Proof.
   intros. constructor; auto with mem.
-  red; intros. apply perm_alloc_2. omega.
+  red; intros. apply perm_alloc_2. lia.
 Qed.
 
 Local Hint Resolve valid_access_alloc_other valid_access_alloc_same: mem.
@@ -1955,11 +1956,11 @@ Proof.
   intros. inv H.
   generalize (size_chunk_pos chunk); intro.
   destruct (eq_block b' b). subst b'.
-  assert (perm m2 b ofs Cur p). apply H0. omega.
-  assert (perm m2 b (ofs + size_chunk chunk - 1) Cur p). apply H0. omega.
+  assert (perm m2 b ofs Cur p). apply H0. lia.
+  assert (perm m2 b (ofs + size_chunk chunk - 1) Cur p). apply H0. lia.
   exploit perm_alloc_inv. eexact H2. rewrite dec_eq_true. intro.
   exploit perm_alloc_inv. eexact H3. rewrite dec_eq_true. intro.
-  intuition omega.
+  intuition lia.
   split; auto. red; intros.
   exploit perm_alloc_inv. apply H0. eauto. rewrite dec_eq_false; auto.
 Qed.
@@ -2006,7 +2007,7 @@ Theorem load_alloc_same':
 Proof.
   intros. assert (exists v, load chunk m2 b ofs = Some v).
     apply valid_access_load. constructor; auto.
-    red; intros. eapply perm_implies. apply perm_alloc_2. omega. auto with mem.
+    red; intros. eapply perm_implies. apply perm_alloc_2. lia. auto with mem.
   destruct H2 as [v LOAD]. rewrite LOAD. decEq.
   eapply load_alloc_same; eauto.
 Qed.
@@ -2116,7 +2117,7 @@ Theorem perm_free_2:
 Proof.
   intros. rewrite free_result. unfold perm, unchecked_free; simpl.
   rewrite PMap.gss. unfold proj_sumbool. rewrite zle_true. rewrite zlt_true.
-  simpl. tauto. omega. omega.
+  simpl. tauto. lia. lia.
 Qed.
 
 Theorem perm_free_3:
@@ -2149,7 +2150,7 @@ Theorem valid_access_free_1:
 Proof.
   intros. inv H. constructor; auto with mem.
   red; intros. eapply perm_free_1; eauto.
-  destruct (zlt lo hi). intuition. right. omega.
+  destruct (zlt lo hi). intuition. right. lia.
 Qed.
 
 Theorem valid_access_free_2:
@@ -2161,9 +2162,9 @@ Proof.
   generalize (size_chunk_pos chunk); intros.
   destruct (zlt ofs lo).
   elim (perm_free_2 lo Cur p).
-  omega. apply H3. omega.
+  lia. apply H3. lia.
   elim (perm_free_2 ofs Cur p).
-  omega. apply H3. omega.
+  lia. apply H3. lia.
 Qed.
 
 Theorem valid_access_free_inv_1:
@@ -2189,7 +2190,7 @@ Proof.
   destruct (zlt lo hi); auto.
   destruct (zle (ofs + size_chunk chunk) lo); auto.
   destruct (zle hi ofs); auto.
-  elim (valid_access_free_2 chunk ofs p); auto. omega.
+  elim (valid_access_free_2 chunk ofs p); auto. lia.
 Qed.
 
 Theorem load_free:
@@ -2227,7 +2228,7 @@ Proof.
   red; intros. eapply perm_free_3; eauto.
   rewrite pred_dec_false; auto.
   red; intros. elim n0; red; intros.
-  eapply perm_free_1; eauto. destruct H; auto. right; omega.
+  eapply perm_free_1; eauto. destruct H; auto. right; lia.
 Qed.
 
 Theorem loadbytes_free_2:
@@ -2297,7 +2298,7 @@ Proof.
   unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP.
   unfold perm. simpl. rewrite PMap.gss. unfold proj_sumbool.
   rewrite zle_true. rewrite zlt_true. simpl. constructor.
-  omega. omega.
+  lia. lia.
 Qed.
 
 Theorem perm_drop_2:
@@ -2307,7 +2308,7 @@ Proof.
   unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP.
   revert H0. unfold perm; simpl. rewrite PMap.gss. unfold proj_sumbool.
   rewrite zle_true. rewrite zlt_true. simpl. auto.
-  omega. omega.
+  lia. lia.
 Qed.
 
 Theorem perm_drop_3:
@@ -2317,7 +2318,7 @@ Proof.
   unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP.
   unfold perm; simpl. rewrite PMap.gsspec. destruct (peq b' b). subst b'.
   unfold proj_sumbool. destruct (zle lo ofs). destruct (zlt ofs hi).
-  byContradiction. intuition omega.
+  byContradiction. intuition lia.
   auto. auto. auto.
 Qed.
 
@@ -2343,7 +2344,7 @@ Proof.
   destruct (eq_block b' b). subst b'.
   destruct (zlt ofs0 lo). eapply perm_drop_3; eauto.
   destruct (zle hi ofs0). eapply perm_drop_3; eauto.
-  apply perm_implies with p. eapply perm_drop_1; eauto. omega.
+  apply perm_implies with p. eapply perm_drop_1; eauto. lia.
   generalize (size_chunk_pos chunk); intros. intuition.
   eapply perm_drop_3; eauto.
 Qed.
@@ -2385,7 +2386,7 @@ Proof.
   destruct (eq_block b' b). subst b'.
   destruct (zlt ofs0 lo). eapply perm_drop_3; eauto.
   destruct (zle hi ofs0). eapply perm_drop_3; eauto.
-  apply perm_implies with p. eapply perm_drop_1; eauto. omega. intuition.
+  apply perm_implies with p. eapply perm_drop_1; eauto. lia. intuition.
   eapply perm_drop_3; eauto.
   rewrite pred_dec_false; eauto.
   red; intros; elim n0; red; intros.
@@ -2443,8 +2444,8 @@ Lemma range_perm_inj:
   range_perm m2 b2 (lo + delta) (hi + delta) k p.
 Proof.
   intros; red; intros.
-  replace ofs with ((ofs - delta) + delta) by omega.
-  eapply perm_inj; eauto. apply H0. omega.
+  replace ofs with ((ofs - delta) + delta) by lia.
+  eapply perm_inj; eauto. apply H0. lia.
 Qed.
 
 Lemma valid_access_inj:
@@ -2456,7 +2457,7 @@ Lemma valid_access_inj:
 Proof.
   intros. destruct H1 as [A B]. constructor.
   replace (ofs + delta + size_chunk chunk)
-     with ((ofs + size_chunk chunk) + delta) by omega.
+     with ((ofs + size_chunk chunk) + delta) by lia.
   eapply range_perm_inj; eauto.
   apply Z.divide_add_r; auto. eapply mi_align; eauto with mem.
 Qed.
@@ -2478,9 +2479,9 @@ Proof.
   rewrite Nat2Z.inj_succ in H1.
   constructor.
   eapply mi_memval; eauto.
-  apply H1. omega.
-  replace (ofs + delta + 1) with ((ofs + 1) + delta) by omega.
-  apply IHn. red; intros; apply H1; omega.
+  apply H1. lia.
+  replace (ofs + delta + 1) with ((ofs + 1) + delta) by lia.
+  apply IHn. red; intros; apply H1; lia.
 Qed.
 
 Lemma load_inj:
@@ -2511,11 +2512,11 @@ Proof.
   destruct (range_perm_dec m1 b1 ofs (ofs + len) Cur Readable); inv H0.
   exists (getN (Z.to_nat len) (ofs + delta) (m2.(mem_contents)#b2)).
   split. apply pred_dec_true.
-  replace (ofs + delta + len) with ((ofs + len) + delta) by omega.
+  replace (ofs + delta + len) with ((ofs + len) + delta) by lia.
   eapply range_perm_inj; eauto with mem.
   apply getN_inj; auto.
-  destruct (zle 0 len). rewrite Z2Nat.id by omega. auto.
-  rewrite Z_to_nat_neg by omega. simpl. red; intros; omegaContradiction.
+  destruct (zle 0 len). rewrite Z2Nat.id by lia. auto.
+  rewrite Z_to_nat_neg by lia. simpl. red; intros; extlia.
 Qed.
 
 (** Preservation of stores. *)
@@ -2530,11 +2531,11 @@ Lemma setN_inj:
 Proof.
   induction 1; intros; simpl.
   auto.
-  replace (p + delta + 1) with ((p + 1) + delta) by omega.
+  replace (p + delta + 1) with ((p + 1) + delta) by lia.
   apply IHlist_forall2; auto.
   intros. rewrite ZMap.gsspec at 1. destruct (ZIndexed.eq q0 p). subst q0.
   rewrite ZMap.gss. auto.
-  rewrite ZMap.gso. auto. unfold ZIndexed.t in *. omega.
+  rewrite ZMap.gso. auto. unfold ZIndexed.t in *. lia.
 Qed.
 
 Definition meminj_no_overlap (f: meminj) (m: mem) : Prop :=
@@ -2589,8 +2590,8 @@ Proof.
   assert (b2 <> b2 \/ ofs0 + delta0 <> (r - delta) + delta).
     eapply H1; eauto. eauto 6 with mem.
     exploit store_valid_access_3. eexact H0. intros [A B].
-    eapply perm_implies. apply perm_cur_max. apply A. omega. auto with mem.
-  destruct H8. congruence. omega.
+    eapply perm_implies. apply perm_cur_max. apply A. lia. auto with mem.
+  destruct H8. congruence. lia.
   (* block <> b1, block <> b2 *)
   eapply mi_memval; eauto. eauto with mem.
 Qed.
@@ -2637,8 +2638,8 @@ Proof.
   rewrite setN_outside. auto.
   rewrite encode_val_length. rewrite <- size_chunk_conv.
   destruct (zlt (ofs0 + delta) ofs); auto.
-  destruct (zle (ofs + size_chunk chunk) (ofs0 + delta)). omega.
-  byContradiction. eapply H0; eauto. omega.
+  destruct (zle (ofs + size_chunk chunk) (ofs0 + delta)). lia.
+  byContradiction. eapply H0; eauto. lia.
   eauto with mem.
 Qed.
 
@@ -2659,7 +2660,7 @@ Proof.
        with ((ofs + Z.of_nat (length bytes1)) + delta).
     eapply range_perm_inj; eauto with mem.
     eapply storebytes_range_perm; eauto.
-    rewrite (list_forall2_length H3). omega.
+    rewrite (list_forall2_length H3). lia.
   destruct (range_perm_storebytes _ _ _ _ H4) as [n2 STORE].
   exists n2; split. eauto.
   constructor.
@@ -2690,9 +2691,9 @@ Proof.
     eapply H1; eauto 6 with mem.
     exploit storebytes_range_perm. eexact H0.
     instantiate (1 := r - delta).
-    rewrite (list_forall2_length H3). omega.
+    rewrite (list_forall2_length H3). lia.
     eauto 6 with mem.
-  destruct H9. congruence. omega.
+  destruct H9. congruence. lia.
   (* block <> b1, block <> b2 *)
   eauto.
 Qed.
@@ -2739,8 +2740,8 @@ Proof.
   rewrite PMap.gsspec. destruct (peq b2 b). subst b2.
   rewrite setN_outside. auto.
   destruct (zlt (ofs0 + delta) ofs); auto.
-  destruct (zle (ofs + Z.of_nat (length bytes2)) (ofs0 + delta)). omega.
-  byContradiction. eapply H0; eauto. omega.
+  destruct (zle (ofs + Z.of_nat (length bytes2)) (ofs0 + delta)). lia.
+  byContradiction. eapply H0; eauto. lia.
   eauto with mem.
 Qed.
 
@@ -2837,10 +2838,10 @@ Proof.
   intros. destruct (eq_block b0 b1).
   subst b0. assert (delta0 = delta) by congruence. subst delta0.
   assert (lo <= ofs < hi).
-  { eapply perm_alloc_3; eauto. apply H6. generalize (size_chunk_pos chunk); omega. }
+  { eapply perm_alloc_3; eauto. apply H6. generalize (size_chunk_pos chunk); lia. }
   assert (lo <= ofs + size_chunk chunk - 1 < hi).
-  { eapply perm_alloc_3; eauto. apply H6. generalize (size_chunk_pos chunk); omega. }
-  apply H2. omega.
+  { eapply perm_alloc_3; eauto. apply H6. generalize (size_chunk_pos chunk); lia. }
+  apply H2. lia.
   eapply mi_align0 with (ofs := ofs) (p := p); eauto.
   red; intros. eapply perm_alloc_4; eauto.
 (* mem_contents *)
@@ -2885,7 +2886,7 @@ Proof.
   intros. eapply perm_free_1; eauto.
   destruct (eq_block b2 b); auto. subst b. right.
   assert (~ (lo <= ofs + delta < hi)). red; intros; eapply H1; eauto.
-  omega.
+  lia.
   constructor.
 (* perm *)
   auto.
@@ -2930,8 +2931,8 @@ Proof.
   intros.
   assert ({ m2' | drop_perm m2 b2 (lo + delta) (hi + delta) p = Some m2' }).
   apply range_perm_drop_2. red; intros.
-  replace ofs with ((ofs - delta) + delta) by omega.
-  eapply perm_inj; eauto. eapply range_perm_drop_1; eauto. omega.
+  replace ofs with ((ofs - delta) + delta) by lia.
+  eapply perm_inj; eauto. eapply range_perm_drop_1; eauto. lia.
   destruct X as [m2' DROP]. exists m2'; split; auto.
   inv H.
   constructor.
@@ -2945,9 +2946,9 @@ Proof.
   destruct (zlt (ofs + delta0) (lo + delta0)). eapply perm_drop_3; eauto.
   destruct (zle (hi + delta0) (ofs + delta0)). eapply perm_drop_3; eauto.
   assert (perm_order p p0).
-    eapply perm_drop_2.  eexact H0. instantiate (1 := ofs). omega. eauto.
+    eapply perm_drop_2.  eexact H0. instantiate (1 := ofs). lia. eauto.
   apply perm_implies with p; auto.
-  eapply perm_drop_1. eauto. omega.
+  eapply perm_drop_1. eauto. lia.
   (* b1 <> b0 *)
   eapply perm_drop_3; eauto.
   destruct (eq_block b3 b2); auto.
@@ -2956,7 +2957,7 @@ Proof.
   exploit H1; eauto.
   instantiate (1 := ofs + delta0 - delta).
   apply perm_cur_max. apply perm_implies with Freeable.
-  eapply range_perm_drop_1; eauto. omega. auto with mem.
+  eapply range_perm_drop_1; eauto. lia. auto with mem.
   eapply perm_drop_4; eauto. eapply perm_max. apply perm_implies with p0. eauto.
   eauto with mem.
   intuition.
@@ -2987,7 +2988,7 @@ Proof.
   destruct (eq_block b2 b); auto. subst b2. right.
   destruct (zlt (ofs + delta) lo); auto.
   destruct (zle hi (ofs + delta)); auto.
-  byContradiction. exploit H1; eauto. omega.
+  byContradiction. exploit H1; eauto. lia.
   (* align *)
   eapply mi_align0; eauto.
   (* contents *)
@@ -3020,9 +3021,9 @@ Theorem extends_refl:
   forall m, extends m m.
 Proof.
   intros. constructor. auto. constructor.
-  intros. unfold inject_id in H; inv H. replace (ofs + 0) with ofs by omega. auto.
+  intros. unfold inject_id in H; inv H. replace (ofs + 0) with ofs by lia. auto.
   intros. unfold inject_id in H; inv H. apply Z.divide_0_r.
-  intros. unfold inject_id in H; inv H. replace (ofs + 0) with ofs by omega.
+  intros. unfold inject_id in H; inv H. replace (ofs + 0) with ofs by lia.
   apply memval_lessdef_refl.
   tauto.
 Qed.
@@ -3035,7 +3036,7 @@ Theorem load_extends:
 Proof.
   intros. inv H. exploit load_inj; eauto. unfold inject_id; reflexivity.
   intros [v2 [A B]]. exists v2; split.
-  replace (ofs + 0) with ofs in A by omega. auto.
+  replace (ofs + 0) with ofs in A by lia. auto.
   rewrite val_inject_id in B. auto.
 Qed.
 
@@ -3059,7 +3060,7 @@ Theorem loadbytes_extends:
               /\ list_forall2 memval_lessdef bytes1 bytes2.
 Proof.
   intros. inv H.
-  replace ofs with (ofs + 0) by omega. eapply loadbytes_inj; eauto.
+  replace ofs with (ofs + 0) by lia. eapply loadbytes_inj; eauto.
 Qed.
 
 Theorem store_within_extends:
@@ -3078,7 +3079,7 @@ Proof.
     rewrite val_inject_id. eauto.
   intros [m2' [A B]].
   exists m2'; split.
-  replace (ofs + 0) with ofs in A by omega. auto.
+  replace (ofs + 0) with ofs in A by lia. auto.
   constructor; auto.
   rewrite (nextblock_store _ _ _ _ _ _ H0).
   rewrite (nextblock_store _ _ _ _ _ _ A).
@@ -3096,7 +3097,7 @@ Proof.
   intros. inversion H. constructor.
   rewrite (nextblock_store _ _ _ _ _ _ H0). auto.
   eapply store_outside_inj; eauto.
-  unfold inject_id; intros. inv H2. eapply H1; eauto. omega.
+  unfold inject_id; intros. inv H2. eapply H1; eauto. lia.
   intros. eauto using perm_store_2.
 Qed.
 
@@ -3130,7 +3131,7 @@ Proof.
     unfold inject_id; reflexivity.
   intros [m2' [A B]].
   exists m2'; split.
-  replace (ofs + 0) with ofs in A by omega. auto.
+  replace (ofs + 0) with ofs in A by lia. auto.
   constructor; auto.
   rewrite (nextblock_storebytes _ _ _ _ _ H0).
   rewrite (nextblock_storebytes _ _ _ _ _ A).
@@ -3148,7 +3149,7 @@ Proof.
   intros. inversion H. constructor.
   rewrite (nextblock_storebytes _ _ _ _ _ H0). auto.
   eapply storebytes_outside_inj; eauto.
-  unfold inject_id; intros. inv H2. eapply H1; eauto. omega.
+  unfold inject_id; intros. inv H2. eapply H1; eauto. lia.
   intros. eauto using perm_storebytes_2.
 Qed.
 
@@ -3180,12 +3181,12 @@ Proof.
   intros.
   eapply perm_implies with Freeable; auto with mem.
   eapply perm_alloc_2; eauto.
-  omega.
+  lia.
   intros. eapply perm_alloc_inv in H; eauto.
   generalize (perm_alloc_inv _ _ _ _ _ H0 b0 ofs Max Nonempty); intros PERM.
   destruct (eq_block b0 b).
   subst b0.
-  assert (EITHER: lo1 <= ofs < hi1 \/ ~(lo1 <= ofs < hi1)) by omega.
+  assert (EITHER: lo1 <= ofs < hi1 \/ ~(lo1 <= ofs < hi1)) by lia.
   destruct EITHER.
   left. apply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto.
   right; tauto.
@@ -3217,7 +3218,7 @@ Proof.
   intros. inv H. constructor.
   rewrite (nextblock_free _ _ _ _ _ H0). auto.
   eapply free_right_inj; eauto.
-  unfold inject_id; intros. inv H. eapply H1; eauto. omega.
+  unfold inject_id; intros. inv H. eapply H1; eauto. lia.
   intros. eauto using perm_free_3.
 Qed.
 
@@ -3232,7 +3233,7 @@ Proof.
   intros. inversion H.
   assert ({ m2': mem | free m2 b lo hi = Some m2' }).
     apply range_perm_free. red; intros.
-    replace ofs with (ofs + 0) by omega.
+    replace ofs with (ofs + 0) by lia.
     eapply perm_inj with (b1 := b); eauto.
     eapply free_range_perm; eauto.
   destruct X as [m2' FREE]. exists m2'; split; auto.
@@ -3242,7 +3243,7 @@ Proof.
   eapply free_right_inj with (m1 := m1'); eauto.
   eapply free_left_inj; eauto.
   unfold inject_id; intros. inv H1.
-  eapply perm_free_2. eexact H0. instantiate (1 := ofs); omega. eauto.
+  eapply perm_free_2. eexact H0. instantiate (1 := ofs); lia. eauto.
   intros. exploit mext_perm_inv0; eauto using perm_free_3. intros [A|A].
   eapply perm_free_inv in A; eauto. destruct A as [[A B]|A]; auto.
   subst b0. right; eapply perm_free_2; eauto.
@@ -3261,7 +3262,7 @@ Theorem perm_extends:
   forall m1 m2 b ofs k p,
   extends m1 m2 -> perm m1 b ofs k p -> perm m2 b ofs k p.
 Proof.
-  intros. inv H. replace ofs with (ofs + 0) by omega.
+  intros. inv H. replace ofs with (ofs + 0) by lia.
   eapply perm_inj; eauto.
 Qed.
 
@@ -3276,7 +3277,7 @@ Theorem valid_access_extends:
   forall m1 m2 chunk b ofs p,
   extends m1 m2 -> valid_access m1 chunk b ofs p -> valid_access m2 chunk b ofs p.
 Proof.
-  intros. inv H. replace ofs with (ofs + 0) by omega.
+  intros. inv H. replace ofs with (ofs + 0) by lia.
   eapply valid_access_inj; eauto. auto.
 Qed.
 
@@ -3421,7 +3422,7 @@ Theorem weak_valid_pointer_inject:
   weak_valid_pointer m2 b2 (ofs + delta) = true.
 Proof.
   intros until 2. unfold weak_valid_pointer. rewrite !orb_true_iff.
-  replace (ofs + delta - 1) with ((ofs - 1) + delta) by omega.
+  replace (ofs + delta - 1) with ((ofs - 1) + delta) by lia.
   intros []; eauto using valid_pointer_inject.
 Qed.
 
@@ -3439,8 +3440,8 @@ Proof.
   assert (perm m1 b1 (Ptrofs.unsigned ofs1) Max Nonempty) by eauto with mem.
   exploit mi_representable; eauto. intros [A B].
   assert (0 <= delta <= Ptrofs.max_unsigned).
-    generalize (Ptrofs.unsigned_range ofs1). omega.
-  unfold Ptrofs.add. repeat rewrite Ptrofs.unsigned_repr; omega.
+    generalize (Ptrofs.unsigned_range ofs1). lia.
+  unfold Ptrofs.add. repeat rewrite Ptrofs.unsigned_repr; lia.
 Qed.
 
 Lemma address_inject':
@@ -3451,7 +3452,7 @@ Lemma address_inject':
   Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)) = Ptrofs.unsigned ofs1 + delta.
 Proof.
   intros. destruct H0. eapply address_inject; eauto.
-  apply H0. generalize (size_chunk_pos chunk). omega.
+  apply H0. generalize (size_chunk_pos chunk). lia.
 Qed.
 
 Theorem weak_valid_pointer_inject_no_overflow:
@@ -3466,7 +3467,7 @@ Proof.
   exploit mi_representable; eauto. destruct H0; eauto with mem.
   intros [A B].
   pose proof (Ptrofs.unsigned_range ofs).
-  rewrite Ptrofs.unsigned_repr; omega.
+  rewrite Ptrofs.unsigned_repr; lia.
 Qed.
 
 Theorem valid_pointer_inject_no_overflow:
@@ -3506,7 +3507,7 @@ Proof.
   exploit mi_representable; eauto. destruct H0; eauto with mem.
   intros [A B].
   pose proof (Ptrofs.unsigned_range ofs).
-  unfold Ptrofs.add. repeat rewrite Ptrofs.unsigned_repr; auto; omega.
+  unfold Ptrofs.add. repeat rewrite Ptrofs.unsigned_repr; auto; lia.
 Qed.
 
 Theorem inject_no_overlap:
@@ -3541,8 +3542,8 @@ Proof.
   rewrite (address_inject' _ _ _ _ _ _ _ _ H H2 H4).
   inv H1. simpl in H5. inv H2. simpl in H1.
   eapply mi_no_overlap; eauto.
-  apply perm_cur_max. apply (H5 (Ptrofs.unsigned ofs1)). omega.
-  apply perm_cur_max. apply (H1 (Ptrofs.unsigned ofs2)). omega.
+  apply perm_cur_max. apply (H5 (Ptrofs.unsigned ofs1)). lia.
+  apply perm_cur_max. apply (H1 (Ptrofs.unsigned ofs2)). lia.
 Qed.
 
 Theorem disjoint_or_equal_inject:
@@ -3561,16 +3562,16 @@ Proof.
   intros.
   destruct (eq_block b1 b2).
   assert (b1' = b2') by congruence. assert (delta1 = delta2) by congruence. subst.
-  destruct H5. congruence. right. destruct H5. left; congruence. right. omega.
+  destruct H5. congruence. right. destruct H5. left; congruence. right. lia.
   destruct (eq_block b1' b2'); auto. subst. right. right.
   set (i1 := (ofs1 + delta1, ofs1 + delta1 + sz)).
   set (i2 := (ofs2 + delta2, ofs2 + delta2 + sz)).
   change (snd i1 <= fst i2 \/ snd i2 <= fst i1).
-  apply Intv.range_disjoint'; simpl; try omega.
+  apply Intv.range_disjoint'; simpl; try lia.
   unfold Intv.disjoint, Intv.In; simpl; intros. red; intros.
   exploit mi_no_overlap; eauto.
-  instantiate (1 := x - delta1). apply H2. omega.
-  instantiate (1 := x - delta2). apply H3. omega.
+  instantiate (1 := x - delta1). apply H2. lia.
+  instantiate (1 := x - delta2). apply H3. lia.
   intuition.
 Qed.
 
@@ -3585,9 +3586,9 @@ Theorem aligned_area_inject:
   (al | ofs + delta).
 Proof.
   intros.
-  assert (P: al > 0) by omega.
-  assert (Q: Z.abs al <= Z.abs sz). apply Zdivide_bounds; auto. omega.
-  rewrite Z.abs_eq in Q; try omega. rewrite Z.abs_eq in Q; try omega.
+  assert (P: al > 0) by lia.
+  assert (Q: Z.abs al <= Z.abs sz). apply Zdivide_bounds; auto. lia.
+  rewrite Z.abs_eq in Q; try lia. rewrite Z.abs_eq in Q; try lia.
   assert (R: exists chunk, al = align_chunk chunk /\ al = size_chunk chunk).
     destruct H0. subst; exists Mint8unsigned; auto.
     destruct H0. subst; exists Mint16unsigned; auto.
@@ -3595,7 +3596,7 @@ Proof.
     subst; exists Mint64; auto.
   destruct R as [chunk [A B]].
   assert (valid_access m chunk b ofs Nonempty).
-    split. red; intros; apply H3. omega. congruence.
+    split. red; intros; apply H3. lia. congruence.
   exploit valid_access_inject; eauto. intros [C D].
   congruence.
 Qed.
@@ -3952,7 +3953,7 @@ Proof.
     unfold f'; intros. destruct (eq_block b0 b1).
       inversion H8. subst b0 b3 delta0.
       elim (fresh_block_alloc _ _ _ _ _ H0).
-      eapply perm_valid_block with (ofs := ofs). apply H9. generalize (size_chunk_pos chunk); omega.
+      eapply perm_valid_block with (ofs := ofs). apply H9. generalize (size_chunk_pos chunk); lia.
       eauto.
     unfold f'; intros. destruct (eq_block b0 b1).
       inversion H8. subst b0 b3 delta0.
@@ -3975,10 +3976,10 @@ Proof.
   congruence.
   inversion H10; subst b0 b1' delta1.
     destruct (eq_block b2 b2'); auto. subst b2'. right; red; intros.
-    eapply H6; eauto. omega.
+    eapply H6; eauto. lia.
   inversion H11; subst b3 b2' delta2.
     destruct (eq_block b1' b2); auto. subst b1'. right; red; intros.
-    eapply H6; eauto. omega.
+    eapply H6; eauto. lia.
   eauto.
 (* representable *)
   unfold f'; intros.
@@ -3986,16 +3987,16 @@ Proof.
    subst. injection H9; intros; subst b' delta0. destruct H10.
     exploit perm_alloc_inv; eauto; rewrite dec_eq_true; intro.
     exploit H3. apply H4 with (k := Max) (p := Nonempty); eauto.
-    generalize (Ptrofs.unsigned_range_2 ofs). omega.
+    generalize (Ptrofs.unsigned_range_2 ofs). lia.
    exploit perm_alloc_inv; eauto; rewrite dec_eq_true; intro.
    exploit H3. apply H4 with (k := Max) (p := Nonempty); eauto.
-   generalize (Ptrofs.unsigned_range_2 ofs). omega.
+   generalize (Ptrofs.unsigned_range_2 ofs). lia.
   eapply mi_representable0; try eassumption.
   destruct H10; eauto using perm_alloc_4.
 (* perm inv *)
   intros. unfold f' in H9; destruct (eq_block b0 b1).
   inversion H9; clear H9; subst b0 b3 delta0.
-  assert (EITHER: lo <= ofs < hi \/ ~(lo <= ofs < hi)) by omega.
+  assert (EITHER: lo <= ofs < hi \/ ~(lo <= ofs < hi)) by lia.
   destruct EITHER.
   left. apply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto.
   right; intros A. eapply perm_alloc_inv in A; eauto. rewrite dec_eq_true in A. tauto.
@@ -4026,10 +4027,10 @@ Proof.
   eapply alloc_right_inject; eauto.
   eauto.
   instantiate (1 := b2). eauto with mem.
-  instantiate (1 := 0). unfold Ptrofs.max_unsigned. generalize Ptrofs.modulus_pos; omega.
+  instantiate (1 := 0). unfold Ptrofs.max_unsigned. generalize Ptrofs.modulus_pos; lia.
   auto.
   intros. apply perm_implies with Freeable; auto with mem.
-  eapply perm_alloc_2; eauto. omega.
+  eapply perm_alloc_2; eauto. lia.
   red; intros. apply Z.divide_0_r.
   intros. apply (valid_not_valid_diff m2 b2 b2); eauto with mem.
   intros [f' [A [B [C D]]]].
@@ -4152,13 +4153,13 @@ Proof.
   simpl; rewrite H0; auto.
   intros. destruct (eq_block b1 b).
   subst b1. rewrite H1 in H2; inv H2.
-  exists lo, hi; split; auto with coqlib. omega.
+  exists lo, hi; split; auto with coqlib. lia.
   exploit mi_no_overlap. eexact H. eexact n. eauto. eauto.
   eapply perm_max. eapply perm_implies. eauto. auto with mem.
   instantiate (1 := ofs + delta0 - delta).
   apply perm_cur_max. apply perm_implies with Freeable; auto with mem.
-  eapply free_range_perm; eauto. omega.
-  intros [A|A]. congruence. omega.
+  eapply free_range_perm; eauto. lia.
+  intros [A|A]. congruence. lia.
 Qed.
 
 Lemma drop_outside_inject: forall f m1 m2 b lo hi p m2',
@@ -4185,7 +4186,7 @@ Proof.
   (* perm *)
   destruct (f b1) as [[b' delta'] |] eqn:?; try discriminate.
   destruct (f' b') as [[b'' delta''] |] eqn:?; inv H.
-  replace (ofs + (delta' + delta'')) with ((ofs + delta') + delta'') by omega.
+  replace (ofs + (delta' + delta'')) with ((ofs + delta') + delta'') by lia.
   eauto.
   (* align *)
   destruct (f b1) as [[b' delta'] |] eqn:?; try discriminate.
@@ -4193,12 +4194,12 @@ Proof.
   apply Z.divide_add_r.
   eapply mi_align0; eauto.
   eapply mi_align1 with (ofs := ofs + delta') (p := p); eauto.
-  red; intros. replace ofs0 with ((ofs0 - delta') + delta') by omega.
-  eapply mi_perm0; eauto. apply H0. omega.
+  red; intros. replace ofs0 with ((ofs0 - delta') + delta') by lia.
+  eapply mi_perm0; eauto. apply H0. lia.
   (* memval *)
   destruct (f b1) as [[b' delta'] |] eqn:?; try discriminate.
   destruct (f' b') as [[b'' delta''] |] eqn:?; inv H.
-  replace (ofs + (delta' + delta'')) with ((ofs + delta') + delta'') by omega.
+  replace (ofs + (delta' + delta'')) with ((ofs + delta') + delta'') by lia.
   eapply memval_inject_compose; eauto.
 Qed.
 
@@ -4227,11 +4228,11 @@ Proof.
   exploit mi_no_overlap0; eauto. intros A.
   destruct (eq_block b1x b2x).
   subst b1x. destruct A. congruence.
-  assert (delta1y = delta2y) by congruence. right; omega.
+  assert (delta1y = delta2y) by congruence. right; lia.
   exploit mi_no_overlap1. eauto. eauto. eauto.
     eapply perm_inj. eauto. eexact H2. eauto.
     eapply perm_inj. eauto. eexact H3. eauto.
-  intuition omega.
+  intuition lia.
 (* representable *)
   intros.
   destruct (f b) as [[b1 delta1] |] eqn:?; try discriminate.
@@ -4243,15 +4244,15 @@ Proof.
   exploit mi_representable1. eauto. instantiate (1 := ofs').
   rewrite H.
   replace (Ptrofs.unsigned ofs + delta1 - 1) with
-    ((Ptrofs.unsigned ofs - 1) + delta1) by omega.
+    ((Ptrofs.unsigned ofs - 1) + delta1) by lia.
   destruct H0; eauto using perm_inj.
-  rewrite H. omega.
+  rewrite H. lia.
 (* perm inv *)
   intros.
   destruct (f b1) as [[b' delta'] |] eqn:?; try discriminate.
   destruct (f' b') as [[b'' delta''] |] eqn:?; try discriminate.
   inversion H; clear H; subst b'' delta.
-  replace (ofs + (delta' + delta'')) with ((ofs + delta') + delta'') in H0 by omega.
+  replace (ofs + (delta' + delta'')) with ((ofs + delta') + delta'') in H0 by lia.
   exploit mi_perm_inv1; eauto. intros [A|A].
   eapply mi_perm_inv0; eauto.
   right; red; intros. elim A. eapply perm_inj; eauto.
@@ -4303,7 +4304,7 @@ Proof.
 (* inj *)
   replace f with (compose_meminj f inject_id). eapply mem_inj_compose; eauto.
   apply extensionality; intros. unfold compose_meminj, inject_id.
-  destruct (f x) as [[y delta] | ]; auto. decEq. decEq. omega.
+  destruct (f x) as [[y delta] | ]; auto. decEq. decEq. lia.
 (* unmapped *)
   eauto.
 (* mapped *)
@@ -4368,7 +4369,7 @@ Proof.
   apply flat_inj_no_overlap.
 (* range *)
   unfold flat_inj; intros.
-  destruct (plt b (nextblock m)); inv H0. generalize (Ptrofs.unsigned_range_2 ofs); omega.
+  destruct (plt b (nextblock m)); inv H0. generalize (Ptrofs.unsigned_range_2 ofs); lia.
 (* perm inv *)
   unfold flat_inj; intros.
   destruct (plt b1 (nextblock m)); inv H0.
@@ -4381,7 +4382,7 @@ Proof.
   intros; red; constructor.
 (* perm *)
   unfold flat_inj; intros. destruct (plt b1 thr); inv H.
-  replace (ofs + 0) with ofs by omega; auto.
+  replace (ofs + 0) with ofs by lia; auto.
 (* align *)
   unfold flat_inj; intros. destruct (plt b1 thr); inv H. apply Z.divide_0_r.
 (* mem_contents *)
@@ -4401,7 +4402,7 @@ Proof.
   red. intros. apply Z.divide_0_r.
   intros.
   apply perm_implies with Freeable; auto with mem.
-  eapply perm_alloc_2; eauto. omega.
+  eapply perm_alloc_2; eauto. lia.
   unfold flat_inj. apply pred_dec_true.
   rewrite (alloc_result _ _ _ _ _ H). auto.
 Qed.
@@ -4417,7 +4418,7 @@ Proof.
   intros; red.
   exploit store_mapped_inj. eauto. eauto. apply flat_inj_no_overlap.
   unfold flat_inj. apply pred_dec_true; auto. eauto.
-  replace (ofs + 0) with ofs by omega.
+  replace (ofs + 0) with ofs by lia.
   intros [m'' [A B]]. congruence.
 Qed.
 
@@ -4464,7 +4465,7 @@ Lemma valid_block_unchanged_on:
   forall m m' b,
   unchanged_on m m' -> valid_block m b -> valid_block m' b.
 Proof.
-  unfold valid_block; intros. apply unchanged_on_nextblock in H. xomega.
+  unfold valid_block; intros. apply unchanged_on_nextblock in H. extlia.
 Qed.
 
 Lemma perm_unchanged_on:
@@ -4507,7 +4508,7 @@ Proof.
 + unfold loadbytes. destruct H.
   destruct (range_perm_dec m b ofs (ofs + n) Cur Readable).
   rewrite pred_dec_true. f_equal.
-  apply getN_exten. intros. rewrite Z2Nat.id in H by omega.
+  apply getN_exten. intros. rewrite Z2Nat.id in H by lia.
   apply unchanged_on_contents0; auto.
   red; intros. apply unchanged_on_perm0; auto.
   rewrite pred_dec_false. auto.
@@ -4525,7 +4526,7 @@ Proof.
   destruct (zle n 0).
 + erewrite loadbytes_empty in * by assumption. auto.
 + rewrite <- H1. apply loadbytes_unchanged_on_1; auto.
-  exploit loadbytes_range_perm; eauto. instantiate (1 := ofs). omega.
+  exploit loadbytes_range_perm; eauto. instantiate (1 := ofs). lia.
   intros. eauto with mem.
 Qed.
 
@@ -4568,7 +4569,7 @@ Proof.
   rewrite encode_val_length. rewrite <- size_chunk_conv.
   destruct (zlt ofs0 ofs); auto.
   destruct (zlt ofs0 (ofs + size_chunk chunk)); auto.
-  elim (H0 ofs0). omega. auto.
+  elim (H0 ofs0). lia. auto.
 Qed.
 
 Lemma storebytes_unchanged_on:
@@ -4584,7 +4585,7 @@ Proof.
   destruct (peq b0 b); auto. subst b0. apply setN_outside.
   destruct (zlt ofs0 ofs); auto.
   destruct (zlt ofs0 (ofs + Z.of_nat (length bytes))); auto.
-  elim (H0 ofs0). omega. auto.
+  elim (H0 ofs0). lia. auto.
 Qed.
 
 Lemma alloc_unchanged_on:
@@ -4613,7 +4614,7 @@ Proof.
 - split; intros.
   eapply perm_free_1; eauto.
   destruct (eq_block b0 b); auto. destruct (zlt ofs lo); auto. destruct (zle hi ofs); auto.
-  subst b0. elim (H0 ofs). omega. auto.
+  subst b0. elim (H0 ofs). lia. auto.
   eapply perm_free_3; eauto.
 - unfold free in H. destruct (range_perm_dec m b lo hi Cur Freeable); inv H.
   simpl. auto.
@@ -4631,7 +4632,7 @@ Proof.
   destruct (eq_block b0 b); auto.
   subst b0.
   assert (~ (lo <= ofs < hi)). { red; intros; eelim H0; eauto. }
-  right; omega.
+  right; lia.
   eapply perm_drop_4; eauto.
 - unfold drop_perm in H.
   destruct (range_perm_dec m b lo hi Cur Freeable); inv H; simpl. auto.
@@ -4658,7 +4659,7 @@ Notation mem := Mem.mem.
 
 Global Opaque Mem.alloc Mem.free Mem.store Mem.load Mem.storebytes Mem.loadbytes.
 
-Hint Resolve
+Global Hint Resolve
   Mem.valid_not_valid_diff
   Mem.perm_implies
   Mem.perm_cur
diff --git a/common/Memtype.v b/common/Memtype.v
index ca9c6f1f..b8ad1a6b 100644
--- a/common/Memtype.v
+++ b/common/Memtype.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
@@ -60,7 +61,7 @@ Inductive perm_order: permission -> permission -> Prop :=
   | perm_W_R:   perm_order Writable Readable
   | perm_any_N: forall p, perm_order p Nonempty.
 
-Hint Constructors perm_order: mem.
+Global Hint Constructors perm_order: mem.
 
 Lemma perm_order_trans:
   forall p1 p2 p3, perm_order p1 p2 -> perm_order p2 p3 -> perm_order p1 p3.
diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index 38bbfa47..c33cb2dc 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.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/common/Sections.ml b/common/Sections.ml
index ea0b6dbc..c256628e 100644
--- a/common/Sections.ml
+++ b/common/Sections.ml
@@ -6,22 +6,27 @@
 (*                                                                     *)
 (*  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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
 (* Handling of linker sections *)
 
+type initialized =
+  | Uninit       (* uninitialized data area *)
+  | Init         (* initialized with fixed, non-relocatable data *)
+  | Init_reloc   (* initialized with relocatable data (symbol addresses) *)
+
 type section_name =
   | Section_text
-  | Section_data of bool (* true = init data, false = uninit data *)
-                  * bool (* thread local? *)
-  | Section_small_data of bool
-  | Section_const of bool
-  | Section_small_const of bool
+  | Section_data of initialized * bool (* true = thread local ? *)
+  | Section_small_data of initialized
+  | Section_const of initialized
+  | Section_small_const of initialized
   | Section_string
   | Section_literal
   | Section_jumptable
@@ -41,6 +46,7 @@ type access_mode =
 
 type section_info = {
   sec_name_init: section_name;
+  sec_name_init_reloc: section_name;
   sec_name_uninit: section_name;
   sec_writable: bool;
   sec_executable: bool;
@@ -48,8 +54,9 @@ type section_info = {
 }
 
 let default_section_info = {
-  sec_name_init = Section_data (true, false);
-  sec_name_uninit = Section_data (false, false);
+  sec_name_init = Section_data (Init, false);
+  sec_name_init_reloc = Section_data (Init_reloc, false);
+  sec_name_uninit = Section_data (Uninit, false);
   sec_writable = true;
   sec_executable = false;
   sec_access = Access_default
@@ -60,46 +67,55 @@ let default_section_info = {
 let builtin_sections = [
   "CODE",
      {sec_name_init = Section_text;
+      sec_name_init_reloc = Section_text;
       sec_name_uninit = Section_text;
       sec_writable = false; sec_executable = true;
       sec_access = Access_default};
   "DATA",
-     {sec_name_init = Section_data (true, false);
-      sec_name_uninit = Section_data (false, false);
+     {sec_name_init = Section_data (Init, false);
+      sec_name_init_reloc = Section_data (Init_reloc, false);
+      sec_name_uninit = Section_data (Uninit, false);
       sec_writable = true; sec_executable = false;
       sec_access = Access_default};
   "TDATA",
-     {sec_name_init = Section_data (true, true);
-      sec_name_uninit = Section_data (false, true);
+     {sec_name_init = Section_data (Init, true);
+      sec_name_init_reloc = Section_data (Init_reloc, true);
+      sec_name_uninit = Section_data (Uninit, true);
       sec_writable = true; sec_executable = false;
       sec_access = Access_default};
   "SDATA",
-     {sec_name_init = Section_small_data true;
-      sec_name_uninit = Section_small_data false;
+     {sec_name_init = Section_small_data Init;
+      sec_name_init_reloc = Section_small_data Init_reloc;
+      sec_name_uninit = Section_small_data Uninit;
       sec_writable = true; sec_executable = false;
       sec_access = Access_near};
   "CONST",
-     {sec_name_init = Section_const true;
-      sec_name_uninit = Section_const false;
+     {sec_name_init = Section_const Init;
+      sec_name_init_reloc = Section_const Init_reloc;
+      sec_name_uninit = Section_const Uninit;
       sec_writable = false; sec_executable = false;
       sec_access = Access_default};
   "SCONST",
-     {sec_name_init = Section_small_const true;
-      sec_name_uninit = Section_small_const false;
+     {sec_name_init = Section_small_const Init;
+      sec_name_init_reloc = Section_small_const Init_reloc;
+      sec_name_uninit = Section_small_const Uninit;
       sec_writable = false; sec_executable = false;
       sec_access = Access_near};
   "STRING",
      {sec_name_init = Section_string;
+      sec_name_init_reloc = Section_string;
       sec_name_uninit = Section_string;
       sec_writable = false; sec_executable = false;
       sec_access = Access_default};
   "LITERAL",
      {sec_name_init = Section_literal;
+      sec_name_init_reloc = Section_literal;
       sec_name_uninit = Section_literal;
       sec_writable = false; sec_executable = false;
       sec_access = Access_default};
   "JUMPTABLE",
      {sec_name_init = Section_jumptable;
+      sec_name_init_reloc = Section_jumptable;
       sec_name_uninit = Section_jumptable;
       sec_writable = false; sec_executable = false;
       sec_access = Access_default}
@@ -134,15 +150,19 @@ let define_section name ?iname ?uname ?writable ?executable ?access () =
     match executable with Some b -> b | None -> si.sec_executable
   and access =
     match access with Some b -> b | None -> si.sec_access in
-  let iname =
+  let i =
     match iname with Some s -> Section_user(s, writable, executable)
                    | None -> si.sec_name_init in
-  let uname =
+  let ir =
+    match iname with Some s -> Section_user(s, writable, executable)
+                   | None -> si.sec_name_init_reloc in
+  let u =
     match uname with Some s -> Section_user(s, writable, executable)
                    | None -> si.sec_name_uninit in
   let new_si =
-    { sec_name_init = iname;
-      sec_name_uninit = uname;
+    { sec_name_init = i;
+      sec_name_init_reloc = ir;
+      sec_name_uninit = u;
       sec_writable = writable;
       sec_executable = executable;
       sec_access = access } in
@@ -162,7 +182,7 @@ let use_section_for id name =
 
 let gcc_section name readonly exec =
   let sn = Section_user(name, not readonly, exec) in
-  { sec_name_init = sn; sec_name_uninit = sn;
+  { sec_name_init = sn; sec_name_init_reloc = sn; sec_name_uninit = sn;
     sec_writable = not readonly; sec_executable = exec;
     sec_access = Access_default }
 
@@ -206,7 +226,12 @@ let for_variable env loc id ty init thrl =
           Hashtbl.find current_section_table name
         with Not_found ->
           assert false in
-  ((if init then si.sec_name_init else si.sec_name_uninit), si.sec_access)
+  let secname =
+    match init with
+    | Uninit -> si.sec_name_uninit
+    | Init -> si.sec_name_init
+    | Init_reloc -> si.sec_name_init_reloc in
+  (secname, si.sec_access)
 
 (* Determine sections for a function definition *)
 
diff --git a/common/Sections.mli b/common/Sections.mli
index 00c06c20..6d1d9c69 100644
--- a/common/Sections.mli
+++ b/common/Sections.mli
@@ -6,23 +6,28 @@
 (*                                                                     *)
 (*  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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
 
 (* Handling of linker sections *)
 
+type initialized =
+  | Uninit       (* uninitialized data area *)
+  | Init         (* initialized with fixed, non-relocatable data *)
+  | Init_reloc   (* initialized with relocatable data (symbol addresses) *)
+
 type section_name =
   | Section_text
-  | Section_data of bool (* true = init data, false = uninit data *)
-                  * bool (* thread local? *)
-  | Section_small_data of bool
-  | Section_const of bool
-  | Section_small_const of bool
+  | Section_data of initialized * bool (* true = thread local? *)
+  | Section_small_data of initialized
+  | Section_const of initialized
+  | Section_small_const of initialized
   | Section_string
   | Section_literal
   | Section_jumptable
@@ -47,7 +52,7 @@ val define_section:
          -> ?writable:bool -> ?executable:bool -> ?access:access_mode -> unit -> unit
 val use_section_for: AST.ident -> string -> bool
 
-val for_variable: Env.t -> C.location -> AST.ident -> C.typ -> bool -> bool ->
+val for_variable: Env.t -> C.location -> AST.ident -> C.typ -> initialized -> bool ->
                                           section_name * access_mode
 val for_function: Env.t -> C.location -> AST.ident -> C.attributes -> section_name list
 val for_stringlit: unit -> section_name
diff --git a/common/Separation.v b/common/Separation.v
index 27065d1f..f41d94c3 100644
--- a/common/Separation.v
+++ b/common/Separation.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
@@ -113,7 +114,7 @@ Proof.
   intros P Q [[A B] [C D]]. split; auto.
 Qed.
 
-Hint Resolve massert_imp_refl massert_eqv_refl : core.
+Global Hint Resolve massert_imp_refl massert_eqv_refl : core.
 
 (** * Separating conjunction *)
 
@@ -355,12 +356,12 @@ Proof.
   intros. rewrite <- sep_assoc. eapply sep_imp; eauto.
   split; simpl; intros.
 - intuition auto.
-+ omega.
-+ apply H5; omega.
-+ omega.
-+ apply H5; omega.
-+ red; simpl; intros; omega.
-- intuition omega.
++ lia.
++ apply H5; lia.
++ lia.
++ apply H5; lia.
++ red; simpl; intros; lia.
+- intuition lia.
 Qed.
 
 Lemma range_drop_left:
@@ -392,12 +393,12 @@ Proof.
   assert (mid <= align mid al) by (apply align_le; auto).
   split; simpl; intros.
 - intuition auto.
-+ omega.
-+ apply H7; omega.
-+ omega.
-+ apply H7; omega.
-+ red; simpl; intros; omega.
-- intuition omega.
++ lia.
++ apply H7; lia.
++ lia.
++ apply H7; lia.
++ red; simpl; intros; lia.
+- intuition lia.
 Qed.
 
 Lemma range_preserved:
@@ -493,7 +494,7 @@ Proof.
   split; [|split].
 - assert (Mem.valid_access m chunk b ofs Freeable).
   { split; auto. red; auto. }
-  split. generalize (size_chunk_pos chunk). unfold Ptrofs.max_unsigned. omega.
+  split. generalize (size_chunk_pos chunk). unfold Ptrofs.max_unsigned. lia.
   split. auto.
 + destruct (Mem.valid_access_load m chunk b ofs) as [v LOAD].
   eauto with mem.
@@ -616,7 +617,7 @@ Next Obligation.
   assert (IMG: forall b1 b2 delta ofs k p,
            j b1 = Some (b2, delta) -> Mem.perm m0 b1 ofs k p -> img b2 (ofs + delta)).
   { intros. red. exists b1, delta; split; auto.
-    replace (ofs + delta - delta) with ofs by omega.
+    replace (ofs + delta - delta) with ofs by lia.
     eauto with mem. }
   destruct H. constructor.
 - destruct mi_inj. constructor; intros.
@@ -668,7 +669,7 @@ Proof.
   intros; red; intros. eelim C; eauto. simpl.
   exists b1, delta; split; auto. destruct VALID as [V1 V2].
   apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem.
-  apply V1. omega.
+  apply V1. lia.
 - red; simpl; intros. destruct H1 as (b0 & delta0 & U & V).
   eelim C; eauto. simpl. exists b0, delta0; eauto with mem.
 Qed.
@@ -690,7 +691,7 @@ Lemma alloc_parallel_rule:
   /\ (forall b, b <> b1 -> j' b = j b).
 Proof.
   intros until delta; intros SEP ALLOC1 ALLOC2 ALIGN LO HI RANGE1 RANGE2 RANGE3.
-  assert (RANGE4: lo <= hi) by xomega.
+  assert (RANGE4: lo <= hi) by extlia.
   assert (FRESH1: ~Mem.valid_block m1 b1) by (eapply Mem.fresh_block_alloc; eauto).
   assert (FRESH2: ~Mem.valid_block m2 b2) by (eapply Mem.fresh_block_alloc; eauto).
   destruct SEP as (INJ & SP & DISJ). simpl in INJ.
@@ -698,10 +699,10 @@ Proof.
 - eapply Mem.alloc_right_inject; eauto.
 - eexact ALLOC1.
 - instantiate (1 := b2). eauto with mem.
-- instantiate (1 := delta). xomega.
-- intros. assert (0 <= ofs < sz2) by (eapply Mem.perm_alloc_3; eauto). omega.
+- instantiate (1 := delta). extlia.
+- intros. assert (0 <= ofs < sz2) by (eapply Mem.perm_alloc_3; eauto). lia.
 - intros. apply Mem.perm_implies with Freeable; auto with mem.
-  eapply Mem.perm_alloc_2; eauto. xomega.
+  eapply Mem.perm_alloc_2; eauto. extlia.
 - red; intros. apply Z.divide_trans with 8; auto.
   exists (8 / align_chunk chunk). destruct chunk; reflexivity.
 - intros. elim FRESH2. eapply Mem.valid_block_inject_2; eauto.
@@ -709,19 +710,19 @@ Proof.
   exists j'; split; auto.
   rewrite <- ! sep_assoc.
   split; [|split].
-+ simpl. intuition auto; try (unfold Ptrofs.max_unsigned in *; omega).
++ simpl. intuition auto; try (unfold Ptrofs.max_unsigned in *; lia).
 * apply Mem.perm_implies with Freeable; auto with mem.
-  eapply Mem.perm_alloc_2; eauto. omega.
+  eapply Mem.perm_alloc_2; eauto. lia.
 * apply Mem.perm_implies with Freeable; auto with mem.
-  eapply Mem.perm_alloc_2; eauto. omega.
-* red; simpl; intros. destruct H1, H2. omega.
+  eapply Mem.perm_alloc_2; eauto. lia.
+* red; simpl; intros. destruct H1, H2. lia.
 * red; simpl; intros.
   assert (b = b2) by tauto. subst b.
   assert (0 <= ofs < lo \/ hi <= ofs < sz2) by tauto. clear H1.
   destruct H2 as (b0 & delta0 & D & E).
   eapply Mem.perm_alloc_inv in E; eauto.
   destruct (eq_block b0 b1).
-  subst b0. rewrite J2 in D. inversion D; clear D; subst delta0. xomega.
+  subst b0. rewrite J2 in D. inversion D; clear D; subst delta0. extlia.
   rewrite J3 in D by auto. elim FRESH2. eapply Mem.valid_block_inject_2; eauto.
 + apply (m_invar P) with m2; auto. eapply Mem.alloc_unchanged_on; eauto.
 + red; simpl; intros.
@@ -753,11 +754,11 @@ Proof.
   simpl in E.
   assert (PERM: Mem.range_perm m2 b2 0 sz2 Cur Freeable).
   { red; intros.
-    destruct (zlt ofs lo). apply J; omega.
-    destruct (zle hi ofs). apply K; omega.
-    replace ofs with ((ofs - delta) + delta) by omega.
+    destruct (zlt ofs lo). apply J; lia.
+    destruct (zle hi ofs). apply K; lia.
+    replace ofs with ((ofs - delta) + delta) by lia.
     eapply Mem.perm_inject; eauto.
-    eapply Mem.free_range_perm; eauto. xomega.
+    eapply Mem.free_range_perm; eauto. extlia.
   }
   destruct (Mem.range_perm_free _ _ _ _ PERM) as [m2' FREE].
   exists m2'; split; auto. split; [|split].
@@ -768,16 +769,16 @@ Proof.
   destruct (zle hi (ofs + delta0)). intuition auto.
   destruct (eq_block b0 b1).
 * subst b0. rewrite H1 in H; inversion H; clear H; subst delta0.
-  eelim (Mem.perm_free_2 m1); eauto. xomega.
+  eelim (Mem.perm_free_2 m1); eauto. extlia.
 * exploit Mem.mi_no_overlap; eauto.
   apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem.
   eapply Mem.perm_free_3; eauto.
   apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
   eapply (Mem.free_range_perm m1); eauto.
-  instantiate (1 := ofs + delta0 - delta). xomega.
-  intros [X|X]. congruence. omega.
+  instantiate (1 := ofs + delta0 - delta). extlia.
+  intros [X|X]. congruence. lia.
 + simpl. exists b0, delta0; split; auto.
-  replace (ofs + delta0 - delta0) with ofs by omega.
+  replace (ofs + delta0 - delta0) with ofs by lia.
   apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem.
   eapply Mem.perm_free_3; eauto.
 - apply (m_invar P) with m2; auto.
@@ -787,7 +788,7 @@ Proof.
   destruct (zle hi i). intuition auto.
   right; exists b1, delta; split; auto.
   apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
-  eapply Mem.free_range_perm; eauto. xomega.
+  eapply Mem.free_range_perm; eauto. extlia.
 - red; simpl; intros. eelim C; eauto.
   simpl. right. destruct H as (b0 & delta0 & U & V).
   exists b0, delta0; split; auto.
@@ -870,7 +871,7 @@ Proof.
   exists j', vres2, m2'; intuition auto.
   split; [|split].
 - exact INJ'.
-- apply m_invar with (m0 := m2).
+- apply (m_invar _ m2).
 + apply globalenv_inject_incr with j m1; auto.
 + eapply Mem.unchanged_on_implies; eauto.
   intros; red; intros; red; intros.
diff --git a/common/Smallstep.v b/common/Smallstep.v
index 27ad0a2d..f337ba3c 100644
--- a/common/Smallstep.v
+++ b/common/Smallstep.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
@@ -893,8 +894,8 @@ Proof.
   exploit (sd_traces DET). eexact H3. intros L2.
   assert (t1 = t0 /\ t2 = t3).
     destruct t1. inv MT. auto.
-    destruct t1; simpl in L1; try omegaContradiction.
-    destruct t0. inv MT. destruct t0; simpl in L2; try omegaContradiction.
+    destruct t1; simpl in L1; try extlia.
+    destruct t0. inv MT. destruct t0; simpl in L2; try extlia.
     simpl in H5. split. congruence. congruence.
   destruct H1; subst.
   assert (s2 = s4) by (eapply sd_determ_2; eauto). subst s4.
@@ -974,7 +975,7 @@ Proof.
     destruct C as [P | [P Q]]; auto using lex_ord_left.
   + exploit sd_determ_3. eauto. eexact A. eauto. intros [P Q]; subst t s1'0.
     exists (i, n), s2; split; auto.
-    right; split. apply star_refl. apply lex_ord_right. omega.
+    right; split. apply star_refl. apply lex_ord_right. lia.
 - exact public_preserved.
 Qed.
 
@@ -1256,7 +1257,7 @@ Proof.
   subst t.
   assert (EITHER: t1 = E0 \/ t2 = E0).
     unfold Eapp in H2; rewrite app_length in H2.
-    destruct t1; auto. destruct t2; auto. simpl in H2; omegaContradiction.
+    destruct t1; auto. destruct t2; auto. simpl in H2; extlia.
   destruct EITHER; subst.
   exploit IHstar; eauto. intros [s2x [s2y [A [B C]]]].
   exists s2x; exists s2y; intuition. eapply star_left; eauto.
@@ -1305,7 +1306,7 @@ Proof.
 - (* 1 L2 makes one or several transitions *)
   assert (EITHER: t = E0 \/ (length t = 1)%nat).
   { exploit L3_single_events; eauto.
-    destruct t; auto. destruct t; auto. simpl. intros. omegaContradiction. }
+    destruct t; auto. destruct t; auto. simpl. intros. extlia. }
   destruct EITHER.
 + (* 1.1 these are silent transitions *)
   subst t. exploit (bsim_E0_plus S12); eauto.
@@ -1473,7 +1474,7 @@ Remark not_silent_length:
   forall t1 t2, (length (t1 ** t2) <= 1)%nat -> t1 = E0 \/ t2 = E0.
 Proof.
   unfold Eapp, E0; intros. rewrite app_length in H.
-  destruct t1; destruct t2; auto. simpl in H. omegaContradiction.
+  destruct t1; destruct t2; auto. simpl in H. extlia.
 Qed.
 
 Lemma f2b_determinacy_inv:
@@ -1622,7 +1623,7 @@ Proof.
   intros [[EQ1 [EQ2 EQ3]] | [NOT1 [NOT2 MT]]].
 + (* 2.1 L2 makes a silent transition: remain in "before" state *)
   subst. simpl in *. exists (F2BI_before n0); exists s1; split.
-  right; split. apply star_refl. constructor. omega.
+  right; split. apply star_refl. constructor. lia.
   econstructor; eauto. eapply star_right; eauto.
 + (* 2.2 L2 make a non-silent transition *)
   exploit not_silent_length. eapply (sr_traces L1_receptive); eauto. intros [EQ | EQ].
@@ -1650,7 +1651,7 @@ Proof.
   exploit f2b_determinacy_inv. eexact H2. eexact STEP2.
   intros [[EQ1 [EQ2 EQ3]] | [NOT1 [NOT2 MT]]].
   subst. exists (F2BI_after n); exists s1; split.
-  right; split. apply star_refl. constructor; omega.
+  right; split. apply star_refl. constructor; lia.
   eapply f2b_match_after'; eauto.
   congruence.
 Qed.
@@ -1763,7 +1764,7 @@ Proof.
   destruct IHstar as [s2x [A B]]. exists s2x; split; auto.
   eapply plus_left. eauto. apply plus_star; eauto. auto.
   destruct t1. simpl in *. subst t. exists s2; split; auto. apply plus_one; auto.
-  simpl in LEN. omegaContradiction.
+  simpl in LEN. extlia.
 Qed.
 
 Lemma ffs_simulation:
@@ -1955,7 +1956,7 @@ Proof.
   assert (t2 = ev :: nil). inv H1; simpl in H0; tauto.
   subst t2. exists (t, s0). constructor; auto. simpl; auto.
 (* single-event *)
-  red. intros. inv H0; simpl; omega.
+  red. intros. inv H0; simpl; lia.
 Qed.
 
 (** * Connections with big-step semantics *)
diff --git a/common/Subtyping.v b/common/Subtyping.v
index 26b282e0..8e5d9361 100644
--- a/common/Subtyping.v
+++ b/common/Subtyping.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
@@ -222,7 +223,7 @@ Definition weight_bounds (ob: option bounds) : nat :=
 Lemma weight_bounds_1:
   forall lo hi s, weight_bounds (Some (B lo hi s)) < weight_bounds None.
 Proof.
-  intros; simpl. generalize (T.weight_range hi); omega.
+  intros; simpl. generalize (T.weight_range hi); lia.
 Qed.
 
 Lemma weight_bounds_2:
@@ -233,8 +234,8 @@ Proof.
   intros; simpl.
   generalize (T.weight_sub _ _ s1) (T.weight_sub _ _ s2) (T.weight_sub _ _ H) (T.weight_sub _ _ H0); intros.
   destruct H1.
-  assert (T.weight lo2 < T.weight lo1) by (apply T.weight_sub_strict; auto). omega.
-  assert (T.weight hi1 < T.weight hi2) by (apply T.weight_sub_strict; auto). omega.
+  assert (T.weight lo2 < T.weight lo1) by (apply T.weight_sub_strict; auto). lia.
+  assert (T.weight hi1 < T.weight hi2) by (apply T.weight_sub_strict; auto). lia.
 Qed.
 
 Hint Resolve T.sub_refl: ty.
@@ -250,11 +251,11 @@ Lemma weight_type_move:
 Proof.
   unfold type_move; intros.
   destruct (peq r1 r2).
-  inv H. split; auto. split; intros. omega. discriminate.
+  inv H. split; auto. split; intros. lia. discriminate.
   destruct (te_typ e)!r1 as [[lo1 hi1 s1]|] eqn:E1;
   destruct (te_typ e)!r2 as [[lo2 hi2 s2]|] eqn:E2.
 - destruct (T.sub_dec hi1 lo2).
-  inv H. split; auto. split; intros. omega. discriminate.
+  inv H. split; auto. split; intros. lia. discriminate.
   destruct (T.sub_dec lo1 hi2); try discriminate.
   set (lo2' := T.lub lo1 lo2) in *.
   set (hi1' := T.glb hi1 hi2) in *.
@@ -264,45 +265,45 @@ Proof.
   set (b2 := B lo2' hi2 (T.lub_min lo1 lo2 hi2 s s2)) in *.
 Local Opaque weight_bounds.
   destruct (T.eq lo2 lo2'); destruct (T.eq hi1 hi1'); inversion H; clear H; subst changed e'; simpl.
-+ split; auto. split; intros. omega. discriminate.
++ split; auto. split; intros. lia. discriminate.
 + assert (weight_bounds (Some b1) < weight_bounds (Some (B lo1 hi1 s1)))
   by (apply weight_bounds_2; auto with ty).
   split; auto. split; intros.
-  rewrite PTree.gsspec. destruct (peq r r1). subst r. rewrite E1. omega. omega.
-  rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E2. omega.
+  rewrite PTree.gsspec. destruct (peq r r1). subst r. rewrite E1. lia. lia.
+  rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E2. lia.
 + assert (weight_bounds (Some b2) < weight_bounds (Some (B lo2 hi2 s2)))
   by (apply weight_bounds_2; auto with ty).
   split; auto. split; intros.
-  rewrite PTree.gsspec. destruct (peq r r2). subst r. rewrite E2. omega. omega.
-  rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E1. omega.
+  rewrite PTree.gsspec. destruct (peq r r2). subst r. rewrite E2. lia. lia.
+  rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E1. lia.
 + assert (weight_bounds (Some b1) < weight_bounds (Some (B lo1 hi1 s1)))
   by (apply weight_bounds_2; auto with ty).
   assert (weight_bounds (Some b2) < weight_bounds (Some (B lo2 hi2 s2)))
   by (apply weight_bounds_2; auto with ty).
   split; auto. split; intros.
   rewrite ! PTree.gsspec.
-  destruct (peq r r2). subst r. rewrite E2. omega.
-  destruct (peq r r1). subst r. rewrite E1. omega.
-  omega.
-  rewrite PTree.gss. rewrite PTree.gso by auto. rewrite PTree.gss. omega.
+  destruct (peq r r2). subst r. rewrite E2. lia.
+  destruct (peq r r1). subst r. rewrite E1. lia.
+  lia.
+  rewrite PTree.gss. rewrite PTree.gso by auto. rewrite PTree.gss. lia.
 
 - set (b2 := B lo1 (T.high_bound lo1) (T.high_bound_sub lo1)) in *.
   assert (weight_bounds (Some b2) < weight_bounds None) by (apply weight_bounds_1).
   inv H; simpl.
   split. destruct (T.sub_dec hi1 lo1); auto.
   split; intros.
-  rewrite PTree.gsspec. destruct (peq r r2). subst r; rewrite E2; omega. omega.
-  rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E1. omega.
+  rewrite PTree.gsspec. destruct (peq r r2). subst r; rewrite E2; lia. lia.
+  rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E1. lia.
 
 - set (b1 := B (T.low_bound hi2) hi2 (T.low_bound_sub hi2)) in *.
   assert (weight_bounds (Some b1) < weight_bounds None) by (apply weight_bounds_1).
   inv H; simpl.
   split. destruct (T.sub_dec hi2 lo2); auto.
   split; intros.
-  rewrite PTree.gsspec. destruct (peq r r1). subst r; rewrite E1; omega. omega.
-  rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E2. omega.
+  rewrite PTree.gsspec. destruct (peq r r1). subst r; rewrite E1; lia. lia.
+  rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E2. lia.
 
-- inv H. split; auto. simpl; split; intros. omega. congruence.
+- inv H. split; auto. simpl; split; intros. lia. congruence.
 Qed.
 
 Definition weight_constraints (b: PTree.t bounds) (cstr: list constraint) : nat :=
@@ -312,7 +313,7 @@ Remark weight_constraints_tighter:
   forall b1 b2, (forall r, weight_bounds b1!r <= weight_bounds b2!r) ->
   forall q, weight_constraints b1 q <= weight_constraints b2 q.
 Proof.
-  induction q; simpl. omega. generalize (H (fst a)) (H (snd a)); omega.
+  induction q; simpl. lia. generalize (H (fst a)) (H (snd a)); lia.
 Qed.
 
 Lemma weight_solve_rec:
@@ -323,8 +324,8 @@ Lemma weight_solve_rec:
      <= weight_constraints e.(te_typ) e.(te_sub) + weight_constraints e.(te_typ) q.
 Proof.
   induction q; simpl; intros.
-- inv H. split. intros; omega. replace (changed' && negb changed') with false.
-  omega. destruct changed'; auto.
+- inv H. split. intros; lia. replace (changed' && negb changed') with false.
+  lia. destruct changed'; auto.
 - destruct a as [r1 r2]; monadInv H; simpl.
   rename x into changed1. rename x0 into e1.
   exploit weight_type_move; eauto. intros [A [B C]].
@@ -336,7 +337,7 @@ Proof.
   assert (Q: weight_constraints (te_typ e1) (te_sub e1) <=
              weight_constraints (te_typ e1) (te_sub e) +
              weight_bounds (te_typ e1)!r1 + weight_bounds (te_typ e1)!r2).
-  { destruct A as [Q|Q]; rewrite Q. omega. simpl. omega. }
+  { destruct A as [Q|Q]; rewrite Q. lia. simpl. lia. }
   assert (R: weight_constraints (te_typ e1) q <= weight_constraints (te_typ e) q)
   by (apply weight_constraints_tighter; auto).
   set (ch1 := if changed' && negb (changed || changed1) then 1 else 0) in *.
@@ -344,11 +345,11 @@ Proof.
   destruct changed1.
   assert (ch2 <= ch1 + 1).
   { unfold ch2, ch1. rewrite orb_true_r. simpl. rewrite andb_false_r.
-    destruct (changed' && negb changed); omega. }
-  exploit C; eauto. omega.
+    destruct (changed' && negb changed); lia. }
+  exploit C; eauto. lia.
   assert (ch2 <= ch1).
-  { unfold ch2, ch1. rewrite orb_false_r. omega. }
-  generalize (B r1) (B r2); omega.
+  { unfold ch2, ch1. rewrite orb_false_r. lia. }
+  generalize (B r1) (B r2); lia.
 Qed.
 
 Definition weight_typenv (e: typenv) : nat :=
@@ -364,7 +365,7 @@ Function solve_constraints (e: typenv) {measure weight_typenv e}: res typenv :=
   end.
 Proof.
   intros. exploit weight_solve_rec; eauto. simpl. intros [A B].
-  unfold weight_typenv. omega.
+  unfold weight_typenv. lia.
 Qed.
 
 Definition typassign := positive -> T.t.
diff --git a/common/Switch.v b/common/Switch.v
index 5a6d4c63..b9aeed96 100644
--- a/common/Switch.v
+++ b/common/Switch.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
@@ -235,8 +236,8 @@ Proof.
   destruct (split_lt n cases) as [lc rc] eqn:SEQ.
   rewrite (IHcases lc rc) by auto.
   destruct (zlt key n); intros EQ; inv EQ; simpl.
-+ destruct (zeq v key). rewrite zlt_true by omega. auto. auto.
-+ destruct (zeq v key). rewrite zlt_false by omega. auto. auto.
++ destruct (zeq v key). rewrite zlt_true by lia. auto. auto.
++ destruct (zeq v key). rewrite zlt_false by lia. auto. auto.
 Qed.
 
 Lemma split_between_prop:
@@ -269,12 +270,12 @@ Lemma validate_jumptable_correct_rec:
   list_nth_z tbl v = Some(ZMap.get (base + v) cases).
 Proof.
   induction tbl; simpl; intros.
-- unfold list_length_z in H0. simpl in H0. omegaContradiction.
+- unfold list_length_z in H0. simpl in H0. extlia.
 - InvBooleans. rewrite list_length_z_cons in H0. apply beq_nat_true in H1.
   destruct (zeq v 0).
-  + replace (base + v) with base by omega. congruence.
-  + replace (base + v) with (Z.succ base + Z.pred v) by omega.
-    apply IHtbl. auto. omega.
+  + replace (base + v) with base by lia. congruence.
+  + replace (base + v) with (Z.succ base + Z.pred v) by lia.
+    apply IHtbl. auto. lia.
 Qed.
 
 Lemma validate_jumptable_correct:
@@ -288,12 +289,12 @@ Lemma validate_jumptable_correct:
 Proof.
   intros.
   rewrite (validate_jumptable_correct_rec cases tbl ofs); auto.
-- f_equal. f_equal. rewrite Z.mod_small. omega.
-  destruct (zle ofs v). omega.
+- f_equal. f_equal. rewrite Z.mod_small. lia.
+  destruct (zle ofs v). lia.
   assert (M: ((v - ofs) + 1 * modulus) mod modulus = (v - ofs) + modulus).
-  { rewrite Z.mod_small. omega. omega. }
-  rewrite Z_mod_plus in M by auto. rewrite M in H0. omega.
-- generalize (Z_mod_lt (v - ofs) modulus modulus_pos). omega.
+  { rewrite Z.mod_small. lia. lia. }
+  rewrite Z_mod_plus in M by auto. rewrite M in H0. lia.
+- generalize (Z_mod_lt (v - ofs) modulus modulus_pos). lia.
 Qed.
 
 Lemma validate_correct_rec:
@@ -309,7 +310,7 @@ Proof.
   destruct cases as [ | [key1 act1] cases1]; intros.
 + apply beq_nat_true in H. subst act. reflexivity.
 + InvBooleans. apply beq_nat_true in H2. subst. simpl.
-  destruct (zeq v hi). auto. omegaContradiction.
+  destruct (zeq v hi). auto. extlia.
 - (* eq node *)
   destruct (split_eq key cases) as [optact others] eqn:EQ. intros.
   destruct optact as [act1|]; InvBooleans; try discriminate.
@@ -319,19 +320,19 @@ Proof.
   + congruence.
   + eapply IHt; eauto.
     unfold refine_low_bound, refine_high_bound. split.
-    destruct (zeq key lo); omega.
-    destruct (zeq key hi); omega.
+    destruct (zeq key lo); lia.
+    destruct (zeq key hi); lia.
 - (* lt node *)
   destruct (split_lt key cases) as [lcases rcases] eqn:EQ; intros; InvBooleans.
   rewrite (split_lt_prop v default _ _ _ _ EQ). destruct (zlt v key).
-  eapply IHt1. eauto. omega.
-  eapply IHt2. eauto. omega.
+  eapply IHt1. eauto. lia.
+  eapply IHt2. eauto. lia.
 - (* jumptable node *)
   destruct (split_between default ofs sz cases) as [ins outs] eqn:EQ; intros; InvBooleans.
   rewrite (split_between_prop v _ _ _ _ _ _ EQ).
-  assert (0 <= (v - ofs) mod modulus < modulus) by (apply Z_mod_lt; omega).
+  assert (0 <= (v - ofs) mod modulus < modulus) by (apply Z_mod_lt; lia).
   destruct (zlt ((v - ofs) mod modulus) sz).
-  rewrite Z.mod_small by omega. eapply validate_jumptable_correct; eauto.
+  rewrite Z.mod_small by lia. eapply validate_jumptable_correct; eauto.
   eapply IHt; eauto.
 Qed.
 
@@ -346,7 +347,7 @@ Theorem validate_switch_correct:
 Proof.
   unfold validate_switch, table_tree_agree; split.
   eapply validate_wf; eauto.
-  intros; eapply validate_correct_rec; eauto. omega.
+  intros; eapply validate_correct_rec; eauto. lia.
 Qed.
 
 End COMPTREE.
diff --git a/common/Switchaux.ml b/common/Switchaux.ml
index 1744a932..eb1ab8bc 100644
--- a/common/Switchaux.ml
+++ b/common/Switchaux.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/common/Unityping.v b/common/Unityping.v
index 28bcfb5c..1089b359 100644
--- a/common/Unityping.v
+++ b/common/Unityping.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
@@ -126,12 +127,12 @@ Lemma length_move:
   length e'.(te_equ) + (if changed then 1 else 0) <= S(length e.(te_equ)).
 Proof.
   unfold move; intros.
-  destruct (peq r1 r2). inv H. omega.
+  destruct (peq r1 r2). inv H. lia.
   destruct e.(te_typ)!r1 as [ty1|]; destruct e.(te_typ)!r2 as [ty2|]; inv H; simpl.
-  destruct (T.eq ty1 ty2); inv H1. omega.
-  omega.
-  omega.
-  omega.
+  destruct (T.eq ty1 ty2); inv H1. lia.
+  lia.
+  lia.
+  lia.
 Qed.
 
 Lemma length_solve_rec:
@@ -140,14 +141,14 @@ Lemma length_solve_rec:
   length e'.(te_equ) + (if ch' && negb ch then 1 else 0) <= length e.(te_equ) + length q.
 Proof.
   induction q; simpl; intros.
-- inv H. replace (ch' && negb ch') with false. omega. destruct ch'; auto.
+- inv H. replace (ch' && negb ch') with false. lia. destruct ch'; auto.
 - destruct a as [r1 r2]; monadInv H. rename x0 into e0. rename x into ch0.
   exploit IHq; eauto. intros A.
   exploit length_move; eauto. intros B.
   set (X := (if ch' && negb (ch || ch0) then 1 else 0)) in *.
   set (Y := (if ch0 then 1 else 0)) in *.
   set (Z := (if ch' && negb ch then 1 else 0)) in *.
-  cut (Z <= X + Y). intros. omega.
+  cut (Z <= X + Y). intros. lia.
   unfold X, Y, Z. destruct ch'; destruct ch; destruct ch0; simpl; auto.
 Qed.
 
@@ -164,7 +165,7 @@ Function solve_constraints (e: typenv) {measure weight_typenv e}: res typenv :=
   end.
 Proof.
   intros. exploit length_solve_rec; eauto. simpl. intros.
-  unfold weight_typenv. omega.
+  unfold weight_typenv. lia.
 Qed.
 
 Definition typassign := positive -> T.t.
@@ -199,7 +200,7 @@ Proof.
   apply A. rewrite PTree.gso by congruence. auto.
 Qed.
 
-Hint Resolve set_incr: ty.
+Global Hint Resolve set_incr: ty.
 
 Lemma set_sound:
   forall te x ty e e', set e x ty = OK e' -> satisf te e' -> te x = ty.
@@ -216,7 +217,7 @@ Proof.
   induction xl; destruct tyl; simpl; intros; monadInv H; eauto with ty.
 Qed.
 
-Hint Resolve set_list_incr: ty.
+Global Hint Resolve set_list_incr: ty.
 
 Lemma set_list_sound:
   forall te xl tyl e e', set_list e xl tyl = OK e' -> satisf te e' -> map te xl = tyl.
@@ -242,7 +243,7 @@ Proof.
 - inv H; simpl in *; split; auto.
 Qed.
 
-Hint Resolve move_incr: ty.
+Global Hint Resolve move_incr: ty.
 
 Lemma move_sound:
   forall te e r1 r2 e' changed,
diff --git a/common/Values.v b/common/Values.v
index 5d32e54e..9353366d 100644
--- a/common/Values.v
+++ b/common/Values.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
@@ -20,6 +21,7 @@ Require Import Coqlib.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
+Require Import Lia.
 
 Definition block : Type := positive.
 Definition eq_block := peq.
@@ -1045,10 +1047,10 @@ Lemma load_result_rettype:
   forall chunk v, has_rettype (load_result chunk v) (rettype_of_chunk chunk).
 Proof.
   intros. unfold has_rettype; destruct chunk; destruct v; simpl; auto.
-- rewrite Int.sign_ext_idem by omega; auto.
-- rewrite Int.zero_ext_idem by omega; auto.
-- rewrite Int.sign_ext_idem by omega; auto.
-- rewrite Int.zero_ext_idem by omega; auto.
+- rewrite Int.sign_ext_idem by lia; auto.
+- rewrite Int.zero_ext_idem by lia; auto.
+- rewrite Int.sign_ext_idem by lia; auto.
+- rewrite Int.zero_ext_idem by lia; auto.
 - destruct Archi.ptr64 eqn:SF; simpl; auto.
 - destruct Archi.ptr64 eqn:SF; simpl; auto.
 - destruct Archi.ptr64 eqn:SF; simpl; auto.
@@ -1074,14 +1076,14 @@ Theorem cast8unsigned_and:
   forall x, zero_ext 8 x = and x (Vint(Int.repr 255)).
 Proof.
   destruct x; simpl; auto. decEq.
-  change 255 with (two_p 8 - 1). apply Int.zero_ext_and. omega.
+  change 255 with (two_p 8 - 1). apply Int.zero_ext_and. lia.
 Qed.
 
 Theorem cast16unsigned_and:
   forall x, zero_ext 16 x = and x (Vint(Int.repr 65535)).
 Proof.
   destruct x; simpl; auto. decEq.
-  change 65535 with (two_p 16 - 1). apply Int.zero_ext_and. omega.
+  change 65535 with (two_p 16 - 1). apply Int.zero_ext_and. lia.
 Qed.
 
 Theorem bool_of_val_of_bool:
@@ -1318,7 +1320,7 @@ Proof.
    unfold divs. rewrite Int.eq_false; try discriminate.
    simpl. rewrite (Int.eq_false Int.one Int.mone); try discriminate.
    rewrite andb_false_intro2; auto. f_equal. f_equal.
-   rewrite Int.divs_one; auto. replace Int.zwordsize with 32; auto. omega.
+   rewrite Int.divs_one; auto. replace Int.zwordsize with 32; auto. lia.
 Qed.
 
 Theorem divu_pow2:
@@ -1445,7 +1447,7 @@ Proof.
   destruct (Int.ltu i0 (Int.repr 31)) eqn:?; inv H1.
   exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 31)) with 31. intros.
   assert (Int.ltu i0 Int.iwordsize = true).
-    unfold Int.ltu. apply zlt_true. change (Int.unsigned Int.iwordsize) with 32. omega.
+    unfold Int.ltu. apply zlt_true. change (Int.unsigned Int.iwordsize) with 32. lia.
   simpl. rewrite H0. simpl. decEq. rewrite Int.shrx_carry; auto.
 Qed.
 
@@ -1460,7 +1462,7 @@ Proof.
   destruct (Int.ltu i0 (Int.repr 31)) eqn:?; inv H1.
   exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 31)) with 31. intros.
   assert (Int.ltu i0 Int.iwordsize = true).
-    unfold Int.ltu. apply zlt_true. change (Int.unsigned Int.iwordsize) with 32. omega.
+    unfold Int.ltu. apply zlt_true. change (Int.unsigned Int.iwordsize) with 32. lia.
   exists i; exists i0; intuition.
   rewrite Int.shrx_shr; auto. destruct (Int.lt i Int.zero); simpl; rewrite H0; auto.
 Qed.
@@ -1483,12 +1485,12 @@ Proof.
   replace (Int.ltu (Int.sub (Int.repr 32) n) Int.iwordsize) with true. simpl.
   replace (Int.ltu n Int.iwordsize) with true.
   f_equal; apply Int.shrx_shr_2; assumption.
-  symmetry; apply zlt_true. change (Int.unsigned n < 32); omega.
+  symmetry; apply zlt_true. change (Int.unsigned n < 32); lia.
   symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 32)) with 32.
   assert (Int.unsigned n <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned n), H0. auto. }
   rewrite Int.unsigned_repr.
-  change (Int.unsigned Int.iwordsize) with 32; omega.
-  assert (32 < Int.max_unsigned) by reflexivity. omega.
+  change (Int.unsigned Int.iwordsize) with 32; lia.
+  assert (32 < Int.max_unsigned) by reflexivity. lia.
 Qed.
 
 Theorem shrx1_shr:
@@ -1535,14 +1537,14 @@ Proof.
     replace (Int.ltu (Int.sub (Int.repr 32) n) Int.iwordsize) with true. simpl.
     replace (Int.ltu n Int.iwordsize) with true.
     f_equal; apply Int.shrx_shr_2; assumption.
-    symmetry; apply zlt_true. change (Int.unsigned n < 32); omega.
+    symmetry; apply zlt_true. change (Int.unsigned n < 32); lia.
     symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 32)) with 32.
     assert (Int.unsigned n <> 0).
     { red; intros; elim H.
       rewrite <- (Int.repr_unsigned n), H0. auto. }
     rewrite Int.unsigned_repr.
-    change (Int.unsigned Int.iwordsize) with 32; omega.
-    assert (32 < Int.max_unsigned) by reflexivity. omega.
+    change (Int.unsigned Int.iwordsize) with 32; lia.
+    assert (32 < Int.max_unsigned) by reflexivity. lia.
 Qed.
 
 Theorem or_rolm:
@@ -1732,7 +1734,7 @@ Proof.
   rewrite (Int64.eq_false Int64.one Int64.mone); try discriminate.
   rewrite andb_false_intro2; auto.
   simpl. f_equal. f_equal. apply Int64.divs_one.
-  replace Int64.zwordsize with 64; auto. omega.
+  replace Int64.zwordsize with 64; auto. lia.
 Qed.
 
 Theorem divlu_pow2:
@@ -1775,7 +1777,7 @@ Proof.
   destruct (Int.ltu i0 (Int.repr 63)) eqn:?; inv H1.
   exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 63)) with 63. intros.
   assert (Int.ltu i0 Int64.iwordsize' = true).
-    unfold Int.ltu. apply zlt_true. change (Int.unsigned Int64.iwordsize') with 64. omega.
+    unfold Int.ltu. apply zlt_true. change (Int.unsigned Int64.iwordsize') with 64. lia.
   simpl. rewrite H0. simpl. decEq. rewrite Int64.shrx'_carry; auto.
 Qed.
 
@@ -1796,12 +1798,12 @@ Proof.
   replace (Int.ltu (Int.sub (Int.repr 64) n) Int64.iwordsize') with true. simpl.
   replace (Int.ltu n Int64.iwordsize') with true.
   f_equal; apply Int64.shrx'_shr_2; assumption.
-  symmetry; apply zlt_true. change (Int.unsigned n < 64); omega.
+  symmetry; apply zlt_true. change (Int.unsigned n < 64); lia.
   symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 64)) with 64.
   assert (Int.unsigned n <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned n), H0. auto. }
   rewrite Int.unsigned_repr.
-  change (Int.unsigned Int64.iwordsize') with 64; omega.
-  assert (64 < Int.max_unsigned) by reflexivity. omega.
+  change (Int.unsigned Int64.iwordsize') with 64; lia.
+  assert (64 < Int.max_unsigned) by reflexivity. lia.
 Qed.
 
 Theorem shrxl1_shrl:
@@ -1848,12 +1850,12 @@ simpl. change (Int.ltu (Int.repr 63) Int64.iwordsize') with true. simpl.
   replace (Int.ltu (Int.sub (Int.repr 64) n) Int64.iwordsize') with true. simpl.
   replace (Int.ltu n Int64.iwordsize') with true.
   f_equal; apply Int64.shrx'_shr_2; assumption.
-  symmetry; apply zlt_true. change (Int.unsigned n < 64); omega.
+  symmetry; apply zlt_true. change (Int.unsigned n < 64); lia.
   symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 64)) with 64.
   assert (Int.unsigned n <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned n), H0. auto. }
   rewrite Int.unsigned_repr.
-  change (Int.unsigned Int64.iwordsize') with 64; omega.
-  assert (64 < Int.max_unsigned) by reflexivity. omega.
+  change (Int.unsigned Int64.iwordsize') with 64; lia.
+  assert (64 < Int.max_unsigned) by reflexivity. lia.
 Qed.
 
 Theorem negate_cmp_bool:
@@ -2127,7 +2129,7 @@ Inductive lessdef_list: list val -> list val -> Prop :=
       lessdef v1 v2 -> lessdef_list vl1 vl2 ->
       lessdef_list (v1 :: vl1) (v2 :: vl2).
 
-Hint Resolve lessdef_refl lessdef_undef lessdef_list_nil lessdef_list_cons : core.
+Global Hint Resolve lessdef_refl lessdef_undef lessdef_list_nil lessdef_list_cons : core.
 
 Lemma lessdef_list_inv:
   forall vl1 vl2, lessdef_list vl1 vl2 -> vl1 = vl2 \/ In Vundef vl1.
@@ -2352,7 +2354,7 @@ Inductive inject (mi: meminj): val -> val -> Prop :=
   | val_inject_undef: forall v,
       inject mi Vundef v.
 
-Hint Constructors inject : core.
+Global Hint Constructors inject : core.
 
 Inductive inject_list (mi: meminj): list val -> list val-> Prop:=
   | inject_list_nil :
@@ -2361,7 +2363,7 @@ Inductive inject_list (mi: meminj): list val -> list val-> Prop:=
       inject mi v v' -> inject_list mi vl vl'->
       inject_list mi (v :: vl) (v' :: vl').
 
-Hint Resolve inject_list_nil inject_list_cons : core.
+Global Hint Resolve inject_list_nil inject_list_cons : core.
 
 Lemma inject_ptrofs:
   forall mi i, inject mi (Vptrofs i) (Vptrofs i).
@@ -2369,7 +2371,7 @@ Proof.
   unfold Vptrofs; intros. destruct Archi.ptr64; auto.
 Qed.
 
-Hint Resolve inject_ptrofs : core.
+Global Hint Resolve inject_ptrofs : core.
 
 Section VAL_INJ_OPS.
 
@@ -2721,7 +2723,7 @@ Proof.
   constructor. eapply val_inject_incr; eauto. auto.
 Qed.
 
-Hint Resolve inject_incr_refl val_inject_incr val_inject_list_incr : core.
+Global Hint Resolve inject_incr_refl val_inject_incr val_inject_list_incr : core.
 
 Lemma val_inject_lessdef:
   forall v1 v2, Val.lessdef v1 v2 <-> Val.inject (fun b => Some(b, 0)) v1 v2.