replacing omega with lia in some file

1 files changed, 2 insertions, 2 deletions

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.
   }