From ad163b18311c2b9e6ae4664f0e66e239df6daa76 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 18 Mar 2023 10:03:27 +0100
Subject: [PATCH] Remove useless scope.

---
 iris_heap_lang/locations.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/iris_heap_lang/locations.v b/iris_heap_lang/locations.v
index ac67d09f1..631e1be25 100644
--- a/iris_heap_lang/locations.v
+++ b/iris_heap_lang/locations.v
@@ -44,8 +44,7 @@ Module Loc.
   Definition fresh (ls : gset loc) : loc :=
     {| loc_car := set_fold (λ k r, (1 + loc_car k) `max` r) 1 ls |}.
 
-  Lemma fresh_fresh ls i :
-    (0 ≤ i)%Z → fresh ls +ₗ i ∉ ls.
+  Lemma fresh_fresh ls i : 0 ≤ i → fresh ls +ₗ i ∉ ls.
   Proof.
     intros Hi. cut (∀ l, l ∈ ls → loc_car l < loc_car (fresh ls) + i).
     { intros help Hf%help. simpl in *. lia. }
-- 
GitLab