diff options
Diffstat (limited to 'common/Memtype.v')
| -rw-r--r-- | common/Memtype.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/common/Memtype.v b/common/Memtype.v index 03dc1499..53775d8b 100644 --- a/common/Memtype.v +++ b/common/Memtype.v @@ -358,7 +358,7 @@ Axiom load_loadbytes: Axiom loadbytes_length: forall m b ofs n bytes, loadbytes m b ofs n = Some bytes -> - length bytes = nat_of_Z n. + length bytes = Z.to_nat n. Axiom loadbytes_empty: forall m b ofs n, |