Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL

1 files changed, 2 insertions, 2 deletions

diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index d29180e4..e0314c6a 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 *)
 
@@ -405,7 +405,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.
   }