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/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 '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. |