diff options
Diffstat (limited to 'common/Memdata.v')
| -rw-r--r-- | common/Memdata.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/common/Memdata.v b/common/Memdata.v index 1d651db2..6f04db36 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -23,6 +23,7 @@ Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. +Require Import Lia. (** * Properties of memory chunks *) @@ -48,7 +49,7 @@ Definition largest_size_chunk := 8. Lemma max_size_chunk: forall chunk, size_chunk chunk <= 8. Proof. - destruct chunk; simpl; omega. + destruct chunk; simpl; lia. Qed. Lemma size_chunk_pos: |