diff options
Diffstat (limited to 'common/Memdata.v')
| -rw-r--r-- | common/Memdata.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/common/Memdata.v b/common/Memdata.v index a9ed48b4..307a02db 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -50,7 +50,7 @@ Proof. Qed. Definition size_chunk_nat (chunk: memory_chunk) : nat := - nat_of_Z(size_chunk chunk). + Z.to_nat(size_chunk chunk). Lemma size_chunk_conv: forall chunk, size_chunk chunk = Z.of_nat (size_chunk_nat chunk). |