From 218d8b335645225689407de2eca5dc42c1ea43dd Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 22 May 2020 16:43:16 +0200
Subject: [PATCH] clarify comment

---
 theories/base_logic/lib/gen_inv_heap.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/base_logic/lib/gen_inv_heap.v b/theories/base_logic/lib/gen_inv_heap.v
index cfb216e1b..230ce9943 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.
-- 
GitLab