diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index e77f27827510e4a3d1658791f5cfe3c814d24890..de766bd774ba3c5d6e51a1b4d483401152ef05f3 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -370,7 +370,7 @@ Section heap.
   Proof.
     intros ??; iDestruct 1 as (hF) "(Hvalσ & HhF & %)".
     assert (Z.to_nat n ≠ O). { rewrite -(Nat2Z.id 0)=>/Z2Nat.inj. lia. }
-    iMod (heap_alloc_vs _ _ (Z.to_nat n) with "[$Hvalσ]") as "[Hvalσ Hmapsto]"; first done.
+    iMod (heap_alloc_vs _ _ (Z.to_nat n) with "[$Hvalσ]") as "[Hvalσ ?]"; first done.
     iMod (own_update _ (● hF) with "HhF") as "[HhF Hfreeable]".
     { apply auth_update_alloc,
         (alloc_singleton_local_update _ (l.1) (1%Qp, inter (l.2) (Z.to_nat n))).