diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 494844854ce1013d5d263b2b3b922a7b2d723df0..8268ee417cd7168e1c54ccfc1669ef1f35b833c7 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -81,7 +81,7 @@ Proof.
 Qed.
 
 Section gen_heap.
-  Context `{Countable L, !gen_heapG L V Σ}.
+  Context {L V} `{Countable L, !gen_heapG L V Σ}.
   Implicit Types P Q : iProp Σ.
   Implicit Types Φ : V → iProp Σ.
   Implicit Types σ : gmap L V.