diff options
Diffstat (limited to 'kvx/Asmblockgenproof1.v')
-rw-r--r-- | kvx/Asmblockgenproof1.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/kvx/Asmblockgenproof1.v b/kvx/Asmblockgenproof1.v index c6ad70ab..a65bd5bc 100644 --- a/kvx/Asmblockgenproof1.v +++ b/kvx/Asmblockgenproof1.v @@ -20,6 +20,7 @@ Require Import AST Integers Floats Values Memory Globalenvs. Require Import Op Locations Machblock Conventions. Require Import Asmblock Asmblockgen Asmblockgenproof0 Asmblockprops. Require Import Chunks. +Require Import Lia. Import PArithCoercions. @@ -1466,7 +1467,7 @@ Proof. change (Int.unsigned Int.zero) with 0. pose proof (Int.unsigned_range x) as RANGE. unfold zlt, zeq. - destruct (Z_lt_dec _ _); destruct (Z.eq_dec _ _); trivial; omega. + destruct (Z_lt_dec _ _); destruct (Z.eq_dec _ _); trivial; lia. Qed. Lemma int64_ltu_to_neq: @@ -1478,7 +1479,7 @@ Proof. change (Int64.unsigned Int64.zero) with 0. pose proof (Int64.unsigned_range x) as RANGE. unfold zlt, zeq. - destruct (Z_lt_dec _ _); destruct (Z.eq_dec _ _); trivial; omega. + destruct (Z_lt_dec _ _); destruct (Z.eq_dec _ _); trivial; lia. Qed. Ltac splitall := repeat match goal with |- _ /\ _ => split end. |