diff options
Diffstat (limited to 'kvx/Asmblock.v')
-rw-r--r-- | kvx/Asmblock.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/kvx/Asmblock.v b/kvx/Asmblock.v index 64b2c535..17ebac32 100644 --- a/kvx/Asmblock.v +++ b/kvx/Asmblock.v @@ -29,6 +29,7 @@ Require Stacklayout. Require Import Conventions. Require Import Errors. Require Export Asmvliw. +Require Import Lia. (* Notations necessary to hook Asmvliw definitions *) Notation undef_caller_save_regs := Asmvliw.undef_caller_save_regs. @@ -212,7 +213,7 @@ Qed. Lemma length_nonil {A: Type} : forall l:(list A), l <> nil -> (length l > 0)%nat. Proof. intros. destruct l; try (contradict H; auto; fail). - cbn. omega. + cbn. lia. Qed. Lemma to_nat_pos : forall z:Z, (Z.to_nat z > 0)%nat -> z > 0. @@ -226,7 +227,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). inversion cor; contradict H; cbn; auto. Qed. |