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 ae4fa5fd..03dc1499 100644 --- a/common/Memtype.v +++ b/common/Memtype.v @@ -104,7 +104,7 @@ Parameter alloc: forall (m: mem) (lo hi: Z), mem * block. (** [free m b lo hi] frees (deallocates) the range of offsets from [lo] included to [hi] excluded in block [b]. Returns the updated memory - state, or [None] if the freed addresses are not writable. *) + state, or [None] if the freed addresses are not freeable. *) Parameter free: forall (m: mem) (b: block) (lo hi: Z), option mem. (** [load chunk m b ofs] reads a memory quantity [chunk] from |