diff options
| author | chaomaer <1506174913@qq.com> | 2019-03-25 17:47:17 +0800 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-03-25 10:47:17 +0100 |
| commit | 02015cafba394b4e18c6231204c5838724b31297 (patch) | |
| tree | df6c0c260cfb38176389138043bd7909d43e8882 /common | |
| parent | 624553ae0b0be62a16ff4bcc9df358f71b759815 (diff) | |
| download | compcert-02015cafba394b4e18c6231204c5838724b31297.tar.gz compcert-02015cafba394b4e18c6231204c5838724b31297.zip | |
Update the comment of the free operation (#277)
The comment says "writable" but it should be "freeable".
Diffstat (limited to 'common')
| -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 |