diff options
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. |