replacing omega with lia in some file

2 files changed, 9 insertions, 9 deletions

diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v
index 6a0297e9..2669d4bc 100644
--- a/riscV/RTLpathSE_simplify.v
+++ b/riscV/RTLpathSE_simplify.v
@@ -524,7 +524,7 @@ Remark ltu_12_wordsize:
 Proof.
   unfold Int.iwordsize, Int.zwordsize. simpl.
   unfold Int.ltu. apply zlt_true.
-  rewrite !Int.unsigned_repr; try cbn; try omega.
+  rewrite !Int.unsigned_repr; try cbn; try lia.
 Qed.
 
 (* Signed longs *)
@@ -575,14 +575,14 @@ Proof.
   intros v n EQMAX. unfold Val.cmp_bool; destruct v; simpl; auto.
   unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1).
   destruct (zlt (Int.signed n) (Int.signed i)).
-  rewrite zlt_false by omega. auto.
-  rewrite zlt_true by omega. auto.
+  rewrite zlt_false by lia. auto.
+  rewrite zlt_true by lia. auto.
   rewrite Int.add_signed. symmetry; apply Int.signed_repr. 
   specialize (Int.eq_spec n (Int.repr Int.max_signed)).
   rewrite EQMAX; simpl; intros.
   assert (Int.signed n <> Int.max_signed).
   { red; intros E. elim H. rewrite <- (Int.repr_signed n). rewrite E. auto. }
-  generalize (Int.signed_range n); omega.
+  generalize (Int.signed_range n); lia.
 Qed.
 
 Lemma cmpl_ltle_add_one: forall v n,
@@ -593,14 +593,14 @@ Proof.
   intros v n EQMAX. unfold Val.cmpl_bool; destruct v; simpl; auto.
   unfold Int64.lt. replace (Int64.signed (Int64.add n Int64.one)) with (Int64.signed n + 1).
   destruct (zlt (Int64.signed n) (Int64.signed i)).
-  rewrite zlt_false by omega. auto.
-  rewrite zlt_true by omega. auto.
+  rewrite zlt_false by lia. auto.
+  rewrite zlt_true by lia. auto.
   rewrite Int64.add_signed. symmetry; apply Int64.signed_repr. 
   specialize (Int64.eq_spec n (Int64.repr Int64.max_signed)).
   rewrite EQMAX; simpl; intros.
   assert (Int64.signed n <> Int64.max_signed).
   { red; intros E. elim H. rewrite <- (Int64.repr_signed n). rewrite E. auto. }
-  generalize (Int64.signed_range n); omega.
+  generalize (Int64.signed_range n); lia.
 Qed.
 
 Remark lt_maxsgn_false_int: forall i,
diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index 97f3ff61..ca0834db 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -13,7 +13,7 @@
 Require Import Coqlib Compopts.
 Require Import AST Integers Floats Values Memory Globalenvs.
 Require Import Op RTL ValueDomain.
-Require Import Zbits.
+Require Import Zbits Lia.
 
 (** Value analysis for RISC V operators *)
 
@@ -390,7 +390,7 @@ Proof.
   assert (DEFAULT: vmatch bc (Val.maketotal (option_map Val.of_bool ob)) (Uns Pbot 1)).
   {
     destruct ob; simpl; auto with va.
-    destruct b; constructor; try omega.
+    destruct b; constructor; try lia.
     change 1 with (usize Int.one). apply is_uns_usize.
     red; intros. apply Int.bits_zero.
   }