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 /scheduling/postpass_lib/Machblock.v | |
| parent | 9a0bf569fab7398abd46bd07d2ee777fe745f591 (diff) | |
| download | compcert-kvx-7cc2810b4b1ea92a8f8a8739f69a94d5578e7b9d.tar.gz compcert-kvx-7cc2810b4b1ea92a8f8a8739f69a94d5578e7b9d.zip | |
replacing omega with lia in some file
Diffstat (limited to 'scheduling/postpass_lib/Machblock.v')
| -rw-r--r-- | scheduling/postpass_lib/Machblock.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/scheduling/postpass_lib/Machblock.v b/scheduling/postpass_lib/Machblock.v index 404c2a96..c8eadbd7 100644 --- a/scheduling/postpass_lib/Machblock.v +++ b/scheduling/postpass_lib/Machblock.v @@ -29,6 +29,7 @@ Require Import Conventions. Require Stacklayout. Require Import Mach. Require Import Linking. +Require Import Lia. (** * Abstract Syntax *) @@ -87,9 +88,9 @@ Lemma size_null b: Proof. destruct b as [h b e]. cbn. unfold size. cbn. intros H. - assert (length h = 0%nat) as Hh; [ omega |]. - assert (length b = 0%nat) as Hb; [ omega |]. - assert (length_opt e = 0%nat) as He; [ omega|]. + assert (length h = 0%nat) as Hh; [ lia |]. + assert (length b = 0%nat) as Hb; [ lia |]. + assert (length_opt e = 0%nat) as He; [ lia|]. repeat split. destruct h; try (cbn in Hh; discriminate); auto. destruct b; try (cbn in Hb; discriminate); auto. |