diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 7ab1f4c18447b4164959a282d8c0f5c82a65f7fd..4371dc2376a72e4d96c9d61074697781eaeefe3c 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -685,7 +685,7 @@ Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
 Proof. revert Ki1. induction Ki2, Ki1; naive_solver eauto with f_equal. Qed.
 
 Lemma alloc_fresh v n σ :
-  let l := fresh_locs (dom (gset loc) σ.(heap)) n in
+  let l := fresh_locs (dom (gset loc) σ.(heap)) in
   0 < n →
   head_step (AllocN ((Val $ LitV $ LitInt $ n)) (Val v)) σ []
             (Val $ LitV $ LitLoc l) (state_init_heap l n v σ) [].
diff --git a/theories/heap_lang/locations.v b/theories/heap_lang/locations.v
index b751bc1ebb33b9e71bf797eba2b77a5dd74de1f2..7484c98ab8e5870ca92fe0992009c0586d9fdd7c 100644
--- a/theories/heap_lang/locations.v
+++ b/theories/heap_lang/locations.v
@@ -30,13 +30,13 @@ Proof. destruct l; rewrite /loc_add /=; f_equal; lia. Qed.
 Instance loc_add_inj l : Inj eq eq (loc_add l).
 Proof. destruct l; rewrite /Inj /loc_add /=; intros; simplify_eq; lia. Qed.
 
-Definition fresh_locs (ls : gset loc) (n : Z) : loc :=
+Definition fresh_locs (ls : gset loc) : loc :=
   {| loc_car := set_fold (λ k r, (1 + loc_car k) `max` r)%Z 1%Z ls |}.
 
-Lemma fresh_locs_fresh ls n i :
-  (0 ≤ i)%Z → (i < n)%Z → fresh_locs ls n +ₗ i ∉ ls.
+Lemma fresh_locs_fresh ls i :
+  (0 ≤ i)%Z → fresh_locs ls +ₗ i ∉ ls.
 Proof.
-  intros Hi _. cut (∀ l, l ∈ ls → loc_car l < loc_car (fresh_locs ls n) + i)%Z.
+  intros Hi. cut (∀ l, l ∈ ls → loc_car l < loc_car (fresh_locs ls) + i)%Z.
   { intros help Hf%help. simpl in *. lia. }
   apply (set_fold_ind_L (λ r ls, ∀ l, l ∈ ls → (loc_car l < r + i)%Z));
     set_solver by eauto with lia.