diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-29 11:12:07 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-29 11:12:07 +0200 |
| commit | 7cc2810b4b1ea92a8f8a8739f69a94d5578e7b9d (patch) | |
| tree | c59a30ef47d86bcc3be8ae186b4305b09fb411fe /kvx/Asmblockgenproof1.v | |
| parent | 9a0bf569fab7398abd46bd07d2ee777fe745f591 (diff) | |
| download | compcert-kvx-7cc2810b4b1ea92a8f8a8739f69a94d5578e7b9d.tar.gz compcert-kvx-7cc2810b4b1ea92a8f8a8739f69a94d5578e7b9d.zip | |
replacing omega with lia in some file
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. |