diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index eca53a8ad9748efcdf3535efa00dc030edb8bd70..913a9d8c096430efd49d968647686ea1afcf172e 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -204,7 +204,7 @@ Section tests.
 End tests.
 
 Section notation_tests.
-  Context `{!heapG Σ, inv_heapG loc val Σ}.
+  Context `{!heapG Σ, !inv_heapG Σ}.
 
   (* Make sure these parse and type-check. *)
   Lemma inv_mapsto_own_test (l : loc) : ⊢ l ↦_(λ _, True) #5. Abort.
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 814e86d99634ffa1b1c067162d916b9f5684d3c1..3bbdc425a90ec9af05a5768708b6ebed3d62bcf2 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.
@@ -35,6 +34,8 @@ 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_heapG := (inv_heapG loc val).
+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