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/PostpassScheduling.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/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: |