diff --git a/CHANGELOG.md b/CHANGELOG.md
index c15d3c9c279f97b8f2966c3182b6e81550c48158..eadb540381b9e33152fe178ff209119c6a9edd5e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -23,8 +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 a fraction to the heap_lang `array` assertion.
-* Added array_copy library for copying and cloning arrays.
+* Added array_tools library 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/theories/base_logic/lib/gen_inv_heap.v b/theories/base_logic/lib/gen_inv_heap.v
index 20311ce9739af67bdf5f4bc4fb3b31a11c914809..2f2de4cadb2c85217f588bbceaad4b1ec477b441 100644
--- a/theories/base_logic/lib/gen_inv_heap.v
+++ b/theories/base_logic/lib/gen_inv_heap.v
@@ -14,11 +14,10 @@ it is that they are reading in that case. In that extreme case, the invariant
 may just be [True].
 
 Since invariant locations cannot be deallocated, they only make sense when
-modelling languages with garbage collection.  Note that heap_lang does not
-actually have explicit dealloaction. However, the proof rules we provide for
-heap operations currently are conservative in the sense that they do not expose
-this fact.  By making "invariant" locations a separate assertion, we can keep
-all the other proofs that do not need it conservative.  *)
+modelling languages with garbage collection.  HeapLang can be used to model
+either language by choosing whether or not to use the [Free] operation.  By
+making "invariant" locations a separate assertion, we can keep all the other
+proofs that do not need it conservative.  *)
 
 Definition inv_heapN: namespace := nroot .@ "inv_heap".
 Local Notation "l ↦ v" := (mapsto l 1 v) (at level 20) : bi_scope.