diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-11 11:41:37 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-11 11:41:37 +0200 |
| commit | af16cdae6d58033cc8aa06bca330f98b96ba12f2 (patch) | |
| tree | 4985e9ae8fa0d580bbf95a198edeca4f0bd6ff46 /scheduling/postpass_lib/Machblock.v | |
| parent | 21c979fce33b068ce4b86e67d3d866b203411c6c (diff) | |
| parent | 02b169b444c435b8d1aacf54969dd7de57317a5c (diff) | |
| download | compcert-kvx-af16cdae6d58033cc8aa06bca330f98b96ba12f2.tar.gz compcert-kvx-af16cdae6d58033cc8aa06bca330f98b96ba12f2.zip | |
Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL
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. |