diff options
Diffstat (limited to 'kvx/PostpassScheduling.v')
| -rw-r--r-- | kvx/PostpassScheduling.v | 7 |
1 files changed, 4 insertions, 3 deletions
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: |