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 /aarch64/Asmblock.v | |
| parent | 9a0bf569fab7398abd46bd07d2ee777fe745f591 (diff) | |
| download | compcert-kvx-7cc2810b4b1ea92a8f8a8739f69a94d5578e7b9d.tar.gz compcert-kvx-7cc2810b4b1ea92a8f8a8739f69a94d5578e7b9d.zip | |
replacing omega with lia in some file
Diffstat (limited to 'aarch64/Asmblock.v')
| -rw-r--r-- | aarch64/Asmblock.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index c606002a..073f1f4c 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -37,6 +37,7 @@ Require Import Values Memory Events Globalenvs Smallstep. Require Import Locations Conventions. Require Stacklayout. Require Import OptionMonad Asm. +Require Import Lia. Require Export Asm. Local Open Scope option_monad_scope. @@ -437,7 +438,7 @@ Qed. Lemma size_positive (b:bblock): size b > 0. Proof. unfold size. destruct b as [hd bdy ex cor]. cbn. - destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; cbn; omega); + destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; cbn; lia); unfold non_empty_bblockb in cor; simpl in cor. inversion cor. Qed. |