diff --git a/theories/heap_lang/primitive_laws.v b/theories/heap_lang/primitive_laws.v
index 5e1ccb1e6eb14f5ec155fed82809002243ac3ead..425121877339991ce7a8ae1cb6960eefd42d3ef9 100644
--- a/theories/heap_lang/primitive_laws.v
+++ b/theories/heap_lang/primitive_laws.v
@@ -394,7 +394,7 @@ Proof.
   iIntros (Hn Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
   iIntros (σ1 κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia.
   iIntros (κ v2 σ2 efs Hstep); inv_head_step.
-  iMod (gen_heap_alloc_gen _ (heap_array l (replicate (Z.to_nat n) v)) with "Hσ")
+  iMod (gen_heap_alloc_big _ (heap_array l (replicate (Z.to_nat n) v)) with "Hσ")
     as "(Hσ & Hl & Hm)".
   { apply heap_array_map_disjoint.
     rewrite replicate_length Z2Nat.id; auto with lia. }
diff --git a/theories/heap_lang/total_adequacy.v b/theories/heap_lang/total_adequacy.v
index 8fc7f84881a66771ae08b9dcca299859d31628b4..4d07855593ec88efbcc91a0046d2187b26852055 100644
--- a/theories/heap_lang/total_adequacy.v
+++ b/theories/heap_lang/total_adequacy.v
@@ -9,7 +9,7 @@ Definition heap_total Σ `{!heapPreG Σ} s e σ φ :
   sn erased_step ([e], σ).
 Proof.
   intros Hwp; eapply (twp_total _ _); iIntros (?) "".
-  iMod (gen_heap_init σ.(heap)) as (?) "Hh".
+  iMod (gen_heap_init σ.(heap)) as (?) "[Hh _]".
   iMod (inv_heap_init loc (option val)) as (?) ">Hi".
   iMod (proph_map_init [] σ.(used_proph_id)) as (?) "Hp".
   iModIntro.