diff --git a/CHANGELOG.md b/CHANGELOG.md
index 701298e33495bbe82fa46cc1481d479da4c2e750..c15d3c9c279f97b8f2966c3182b6e81550c48158 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,20 +7,28 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 
 **Changes in the theory of Iris itself:**
 
-* [#] Redefine invariants as "semantic invariants" so that they support
+* [#] Redefined invariants as "semantic invariants" so that they support
   splitting and other forms of weakening.
 * Updated the strong variant of the opening lemma for cancellable invariants
   to match that of regular invariants, where you can pick the mask at a later time.
 
 **Changes in program logic:**
 
-* In the axiomatization of ectx languages we replace the axiom of positivity of
+* In the axiomatization of ectx languages we replaced the axiom of positivity of
   context composition with an axiom that says if `fill K e` takes a head step,
   then either `K` is the empty evaluation context or `e` is a value.
 * Added a library for "invariant locations": heap locations that will not be
   deallocated (i.e., they are GC-managed) and satisfy some pure, Coq-level
   invariant.  See `iris.base_logic.lib.gen_inv_heap` for details.
 
+**Changes in heap_lang:**
+
+* Added a fraction to the heap_lang `array` assertion.
+* Added array_copy library for copying and cloning arrays.
+* Added the ghost state for "invariant locations" to `heapG`.  This affects the
+  statement of `heap_adequacy`, which is now responsible for initializing the
+  "invariant locations" invariant.
+
 **Changes in Coq:**
 
 * Added support for Coq 8.10 and Coq 8.11; dropped support for Coq 8.7 and Coq 8.8.
@@ -180,11 +188,6 @@ s/\bauth_both_frac_op\b/auth_both_op/g
 ' $(find theories -name "*.v")
 ```
 
-**Changes in heap_lang:**
-
-* Added a fraction to the heap_lang `array` assertion.
-* Added array_copy library for copying and cloning arrays.
-
 ## Iris 3.2.0 (released 2019-08-29)
 
 The highlight of this release is the completely re-engineered interactive proof
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index c1a914da86c7c63c9b3c4fe0b9f0af9d575937cc..6b88e361c6150d1fec7b32d21c915a084d817de0 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -221,7 +221,7 @@ Section tests.
 End tests.
 
 Section notation_tests.
-  Context `{!heapG Σ, inv_heapG loc val Σ}.
+  Context `{!heapG Σ}.
 
   (* Make sure these parse and type-check. *)
   Lemma inv_mapsto_own_test (l : loc) : ⊢ l ↦_(λ _, True) #5. Abort.
@@ -291,4 +291,4 @@ Section error_tests.
 End error_tests.
 
 Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (λ v _, v = #2).
-Proof. eapply (heap_adequacy heapΣ)=> ?. by apply heap_e_spec. Qed.
+Proof. eapply (heap_adequacy heapΣ)=> ?. iIntros "_". by iApply heap_e_spec. Qed.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 756b8f40687887bc5b754e01486f85a5d3bec350..349deb199ebb5dd04879fc9bc5c3037af2b60d82 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -124,7 +124,7 @@ Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ].
 (** This lemma implicitly shows that these functors are enough to meet
 all library assumptions. *)
 Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
-Proof. apply (heap_adequacy clientΣ)=> ?. apply client_safe. Qed.
+Proof. apply (heap_adequacy clientΣ)=> ?. iIntros "_". iApply client_safe. Qed.
 
 (* Since we check the output of the test files, this means
 our test suite will fail if we ever accidentally add an axiom
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index f11b9390339d66515f9a4ad5ab4167f5fc2c1630..b7cfef5df12188ce4d23761514ad5de5c6155a07 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -142,4 +142,4 @@ Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ].
 (** This lemma implicitly shows that these functors are enough to meet
 all library assumptions. *)
 Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
-Proof. apply (heap_adequacy clientΣ)=> ?. apply client_safe. Qed.
+Proof. apply (heap_adequacy clientΣ)=> ?. iIntros "_". iApply client_safe. Qed.
diff --git a/theories/base_logic/lib/gen_inv_heap.v b/theories/base_logic/lib/gen_inv_heap.v
index a6fd87779a71487bf25ace21e3ef80687d0a2b80..20311ce9739af67bdf5f4bc4fb3b31a11c914809 100644
--- a/theories/base_logic/lib/gen_inv_heap.v
+++ b/theories/base_logic/lib/gen_inv_heap.v
@@ -113,7 +113,7 @@ Section to_inv_heap.
   Qed.
 End to_inv_heap.
 
-Lemma inv_heap_init {L V : Type} `{Countable L, !invG Σ, !gen_heapG L V Σ, !inv_heapPreG L V Σ} E:
+Lemma inv_heap_init (L V : Type) `{Countable L, !invG Σ, !gen_heapG L V Σ, !inv_heapPreG L V Σ} E :
   ⊢ |==> ∃ _ : inv_heapG L V Σ, |={E}=> inv_heap_inv L V.
 Proof.
   iMod (own_alloc (● (to_inv_heap ∅))) as (γ) "H●".
diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index d3fc86c702def562ee4696483a84942af198f2ac..2b6366bb2ab2e2e66b6d56402474eb130768903d 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -7,23 +7,25 @@ Set Default Proof Using "Type".
 Class heapPreG Σ := HeapPreG {
   heap_preG_iris :> invPreG Σ;
   heap_preG_heap :> gen_heapPreG loc val Σ;
+  heap_preG_inv_heap :> inv_heapPreG loc val Σ;
   heap_preG_proph :> proph_mapPreG proph_id (val * val) Σ;
 }.
 
 Definition heapΣ : gFunctors :=
-  #[invΣ; gen_heapΣ loc val; proph_mapΣ proph_id (val * val)].
+  #[invΣ; gen_heapΣ loc val; inv_heapΣ loc val; proph_mapΣ proph_id (val * val)].
 Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
 Proof. solve_inG. Qed.
 
 Definition heap_adequacy Σ `{!heapPreG Σ} s e σ φ :
-  (∀ `{!heapG Σ}, ⊢ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
+  (∀ `{!heapG Σ}, ⊢ inv_heap_inv -∗ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
   adequate s e σ (λ v _, φ v).
 Proof.
   intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "".
   iMod (gen_heap_init σ.(heap)) as (?) "Hh".
+  iMod (inv_heap_init loc val) as (?) ">Hi".
   iMod (proph_map_init κs σ.(used_proph_id)) as (?) "Hp".
   iModIntro. iExists
     (λ σ κs, (gen_heap_ctx σ.(heap) ∗ proph_map_ctx κs σ.(used_proph_id))%I),
     (λ _, True%I).
-  iFrame. iApply (Hwp (HeapG _ _ _ _)).
+  iFrame. iApply (Hwp (HeapG _ _ _ _ _)). done.
 Qed.
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 814e86d99634ffa1b1c067162d916b9f5684d3c1..584d4a340de71e560c1d41e298352475380c52eb 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -1,8 +1,7 @@
 From stdpp Require Import fin_maps.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth gmap.
-From iris.base_logic.lib Require Export gen_heap proph_map.
-From iris.base_logic.lib Require Import gen_inv_heap.
+From iris.base_logic.lib Require Export gen_heap proph_map gen_inv_heap.
 From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
 From iris.heap_lang Require Export lang.
@@ -12,6 +11,7 @@ Set Default Proof Using "Type".
 Class heapG Σ := HeapG {
   heapG_invG : invG Σ;
   heapG_gen_heapG :> gen_heapG loc val Σ;
+  heapG_inv_heapG :> inv_heapG loc val Σ;
   heapG_proph_mapG :> proph_mapG proph_id (val * val) Σ;
 }.
 
@@ -35,6 +35,7 @@ Notation "l ↦□ I" := (inv_mapsto (L:=loc) (V:=val) l I%stdpp%type)
   (at level 20, format "l  ↦□  I") : bi_scope.
 Notation "l ↦_ I v" := (inv_mapsto_own (L:=loc) (V:=val) l v I%stdpp%type)
   (at level 20, I at level 9, format "l  ↦_ I   v") : bi_scope.
+Notation inv_heap_inv := (inv_heap_inv loc val).
 
 (** The tactic [inv_head_step] performs inversion on hypotheses of the shape
 [head_step]. The tactic will discharge head-reductions starting from values, and
diff --git a/theories/heap_lang/total_adequacy.v b/theories/heap_lang/total_adequacy.v
index 2194d6df05dfc79d204bbcb1a92a5518d87664b2..346b024d2abdd439457b38ac2ca2ff42ba5b6e48 100644
--- a/theories/heap_lang/total_adequacy.v
+++ b/theories/heap_lang/total_adequacy.v
@@ -5,15 +5,16 @@ From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
 Definition heap_total Σ `{!heapPreG Σ} s e σ φ :
-  (∀ `{!heapG Σ}, ⊢ WP e @ s; ⊤ [{ v, ⌜φ v⌝ }]) →
+  (∀ `{!heapG Σ}, ⊢ inv_heap_inv -∗ WP e @ s; ⊤ [{ v, ⌜φ v⌝ }]) →
   sn erased_step ([e], σ).
 Proof.
   intros Hwp; eapply (twp_total _ _); iIntros (?) "".
   iMod (gen_heap_init σ.(heap)) as (?) "Hh".
+  iMod (inv_heap_init loc val) as (?) ">Hi".
   iMod (proph_map_init [] σ.(used_proph_id)) as (?) "Hp".
   iModIntro.
   iExists
     (λ σ κs _, (gen_heap_ctx σ.(heap) ∗ proph_map_ctx κs σ.(used_proph_id))%I),
     (λ _, True%I); iFrame.
-  iApply (Hwp (HeapG _ _ _ _)).
+  iApply (Hwp (HeapG _ _ _ _ _)). done.
 Qed.