diff --git a/theories/base_logic/lib/gen_inv_heap.v b/theories/base_logic/lib/gen_inv_heap.v
index cfb216e1b16be7e9d57ef6871bf012bbb00abe80..230ce99431a926d5e84ff2d78df2d298696b4c58 100644
--- a/theories/base_logic/lib/gen_inv_heap.v
+++ b/theories/base_logic/lib/gen_inv_heap.v
@@ -16,8 +16,8 @@ may just be [True].
 Since invariant locations cannot be deallocated, they only make sense when
 modeling 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.  *)
+using a separate assertion [inv_mapsto_own] for "invariant" locations, 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.