diff --git a/CHANGELOG.md b/CHANGELOG.md
index eadb540381b9e33152fe178ff209119c6a9edd5e..58ed3cc85c8b8b2375d32877a1de88a0e5ff7eed 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -23,9 +23,9 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 
 **Changes in heap_lang:**
 
-* Added support for deallocation of locations.
+* Added support for deallocation of locations via the `Free` operation.
 * Added a fraction to the heap_lang `array` assertion.
-* Added array_tools library for deallocating, copying and cloning arrays.
+* Added `lib.array` module for deallocating, copying and cloning arrays.
 * Added the ghost state for "invariant locations" to `heapG`.  This affects the
   statement of `heap_adequacy`, which is now responsible for initializing the
   "invariant locations" invariant.
diff --git a/_CoqProject b/_CoqProject
index 1619de757060b8a50ccc77e5366844dfedfb60e9..156b00d69619b9b9866f6467e799fae1fb6436c5 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -124,7 +124,7 @@ theories/heap_lang/lib/atomic_heap.v
 theories/heap_lang/lib/increment.v
 theories/heap_lang/lib/diverge.v
 theories/heap_lang/lib/arith.v
-theories/heap_lang/lib/array_tools.v
+theories/heap_lang/lib/array.v
 theories/proofmode/base.v
 theories/proofmode/tokens.v
 theories/proofmode/coq_tactics.v
diff --git a/theories/heap_lang/lib/array_tools.v b/theories/heap_lang/lib/array.v
similarity index 100%
rename from theories/heap_lang/lib/array_tools.v
rename to theories/heap_lang/lib/array.v