From 7cc2810b4b1ea92a8f8a8739f69a94d5578e7b9d Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 29 Mar 2021 11:12:07 +0200 Subject: replacing omega with lia in some file --- aarch64/Asmblock.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'aarch64/Asmblock.v') 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. -- cgit