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/PostpassScheduling.v | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'kvx/PostpassScheduling.v') diff --git a/kvx/PostpassScheduling.v b/kvx/PostpassScheduling.v index 1f1f238a..08e640c6 100644 --- a/kvx/PostpassScheduling.v +++ b/kvx/PostpassScheduling.v @@ -18,6 +18,7 @@ Require Import Coqlib Errors AST Integers. Require Import Asmblock Axioms Memory Globalenvs. Require Import Asmblockdeps Asmblockgenproof0 Asmblockprops. Require Peephole. +Require Import Lia. Local Open Scope error_monad_scope. @@ -87,8 +88,8 @@ Lemma concat2_zlt_size: Proof. intros. monadInv H. split. - - unfold check_size in EQ. destruct (zlt Ptrofs.max_unsigned (size a)); monadInv EQ. omega. - - unfold check_size in EQ1. destruct (zlt Ptrofs.max_unsigned (size b)); monadInv EQ1. omega. + - unfold check_size in EQ. destruct (zlt Ptrofs.max_unsigned (size a)); monadInv EQ. lia. + - unfold check_size in EQ1. destruct (zlt Ptrofs.max_unsigned (size b)); monadInv EQ1. lia. Qed. Lemma concat2_noexit: @@ -436,7 +437,7 @@ Lemma verified_schedule_size: Proof. intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i. all: try (apply verified_schedule_nob_size; auto; fail). - inv H. simpl. omega. + inv H. simpl. lia. Qed. Lemma verified_schedule_no_header_in_middle: -- cgit