From 80623a8c7ebbd451bbfe3d8a395f5bb741667a81 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Tue, 9 Jul 2019 16:47:30 +0200
Subject: [PATCH] Get rid of a superflous argument to `fresh_locs`.

---
 theories/heap_lang/lang.v      | 2 +-
 theories/heap_lang/locations.v | 8 ++++----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 7ab1f4c18..4371dc237 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 b751bc1eb..7484c98ab 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.
-- 
GitLab