From 305121db6fc691a9a4dbf2ee0afe65cf6812e9f2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 8 May 2023 14:34:47 +0200
Subject: [PATCH] fix some outdated references to heapG

---
 docs/resource_algebras.md | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/docs/resource_algebras.md b/docs/resource_algebras.md
index 71d547b32..134e5f540 100644
--- a/docs/resource_algebras.md
+++ b/docs/resource_algebras.md
@@ -59,12 +59,12 @@ Now you can add `one_shotG` as an assumption to all your module definitions and
 proofs.  We typically use a section for this:
 ```coq
 Section proof.
-Context `{!heapG Σ, !one_shotG Σ}.
+Context `{!heapGS Σ, !one_shotG Σ}.
 ```
-Notice that besides our own assumptions `one_shotG`, we also assume `heapG`,
+Notice that besides our own assumptions `one_shotG`, we also assume `heapGS`,
 which are assumptions that every HeapLang proof makes (they are related to
 defining the `↦` connective as well as the basic Iris infrastructure for
-invariants and WP).  For this purpose, `heapG` contains not only assumptions
+invariants and WP).  For this purpose, `heapGS` contains not only assumptions
 about `Σ`, it also contains some ghost names to refer to particular ghost state
 (see "global ghost state instances" below).
 
@@ -102,7 +102,7 @@ see the next section), you have to call the respective initialization or
 adequacy lemma.  [For example](tests/one_shot.v):
 ```coq
 Section client.
-  Context `{!heapG Σ, !one_shotG Σ, !spawnG Σ}.
+  Context `{!heapGS Σ, !one_shotG Σ, !spawnG Σ}.
 
   Lemma client_safe : WP client {{ _, True }}%I.
   (* ... *)
-- 
GitLab