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 --- kvx/NeedOp.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'kvx/NeedOp.v') diff --git a/kvx/NeedOp.v b/kvx/NeedOp.v index f636336d..4578b4e8 100644 --- a/kvx/NeedOp.v +++ b/kvx/NeedOp.v @@ -18,6 +18,7 @@ Require Import AST Integers Floats. Require Import Values Memory Globalenvs. Require Import Op RTL. Require Import NeedDomain. +Require Import Lia. (** Neededness analysis for RISC-V operators *) @@ -405,8 +406,8 @@ Lemma operation_is_redundant_sound: vagree v arg1' nv. Proof. intros. destruct op; cbn in *; try discriminate; inv H1; FuncInv; subst. -- apply sign_ext_redundant_sound; auto. omega. -- apply sign_ext_redundant_sound; auto. omega. +- apply sign_ext_redundant_sound; auto. lia. +- apply sign_ext_redundant_sound; auto. lia. - apply andimm_redundant_sound; auto. - apply orimm_redundant_sound; auto. Qed. -- cgit