From 234a9cadc8da94b331fc3ead341380142749e8c7 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Fri, 2 Jun 2023 17:52:09 +0200 Subject: [PATCH] gen_heap: fix a comment --- iris/base_logic/lib/gen_heap.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v index a7ca238c1..41f23cb4e 100644 --- a/iris/base_logic/lib/gen_heap.v +++ b/iris/base_logic/lib/gen_heap.v @@ -49,10 +49,10 @@ building abstractions, then one can gradually assign more ghost information to a location instead of having to do all of this at once. We use namespaces so that these can be matched up with the invariant namespaces. *) -(** To implement this mechanism, we use three resource algebras: +(** To implement this mechanism, we use three pieces of ghost state: -- A [gmap_view L V], which keeps track of the values of locations. -- A [gmap_view L gname], which keeps track of the meta information of +- A [ghost_map L V], which keeps track of the values of locations. +- A [ghost_map L gname], which keeps track of the meta information of locations. More specifically, this RA introduces an indirection: it keeps track of a ghost name for each location. - The ghost names in the aforementioned authoritative RA refer to namespace maps -- GitLab