From f94e312e5a902bd9be4b64b8ed258cd4be0f652c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 12 Oct 2020 20:03:18 +0200
Subject: [PATCH] clarify the intended use of gen_heap

---
 theories/base_logic/lib/gen_heap.v | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index d41b2f9d9..f698c5b00 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -9,8 +9,13 @@ Import uPred.
 (** This file provides a generic mechanism for a point-to connective [l ↦{q} v]
 with fractional permissions (where [l : L] and [v : V] over some abstract type
 [L] for locations and [V] for values). This mechanism can be plugged into a
-language by using the heap invariant [gen_heap_ctx σ] where [σ : gmap L V]. See
-heap-lang for an example.
+language and related to the physical heap by using [gen_heap_ctx σ] in the state
+interpretation of the weakest precondition, where [σ : gmap L V]. See heap-lang
+for an example.
+
+This library is not meant to be used for ghost state unrelated to the physical
+heap, and will not be very usable for that case. Use [algebra.lib.gmap_view]
+together with [own] instead.
 
 Next to the point-to connective [l ↦{q} v], which keeps track of the value [v]
 of a location [l], this mechanism allows one to attach "meta" or "ghost" data to
-- 
GitLab