From 3a7c26b0d541bb274f5e6bab0d27675e851a1ffa Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 7 Jan 2021 18:34:15 +0100
Subject: [PATCH] explain what gen_heap_init_names is for

---
 iris/base_logic/lib/gen_heap.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index 774cdea70..51ecbe6ee 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -305,6 +305,10 @@ Section gen_heap.
   Qed.
 End gen_heap.
 
+(** This variant of [gen_heap_init] should only be used when absolutely needed.
+The key difference to [gen_heap_init] is that the [inG] instances in the new
+[gen_heapG] instance are related to the original [gen_heapPreG] instance,
+whereas [gen_heap_init] forgets about that relation. *)
 Lemma gen_heap_init_names `{Countable L, !gen_heapPreG L V Σ} σ :
   ⊢ |==> ∃ γh γm : gname,
     let hG := GenHeapG L V Σ γh γm in
-- 
GitLab