diff options
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. |