From 48892abafd4655b470f29677c8722ef4fc1bf64c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 4 Dec 2017 11:29:16 +0100
Subject: [PATCH] =?UTF-8?q?Change=20bound=20variable=20so=20that=20we=20do?=
 =?UTF-8?q?=20not=20have=20`=CE=A8=20v=20=E2=88=A8=20...`=20but=20`=CE=A8?=
 =?UTF-8?q?=20w=20=E2=88=A8=20...`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/heap_lang/lib/spawn.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/heap_lang/lib/spawn.v b/theories/heap_lang/lib/spawn.v
index 5e5ad25ed..f9059566e 100644
--- a/theories/heap_lang/lib/spawn.v
+++ b/theories/heap_lang/lib/spawn.v
@@ -31,7 +31,7 @@ Context `{!heapG Σ, !spawnG Σ} (N : namespace).
 
 Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp Σ) : iProp Σ :=
   (∃ lv, l ↦ lv ∗ (⌜lv = NONEV⌝ ∨
-                   ∃ v, ⌜lv = SOMEV v⌝ ∗ (Ψ v ∨ own γ (Excl ()))))%I.
+                   ∃ w, ⌜lv = SOMEV w⌝ ∗ (Ψ w ∨ own γ (Excl ()))))%I.
 
 Definition join_handle (l : loc) (Ψ : val → iProp Σ) : iProp Σ :=
   (∃ γ, own γ (Excl ()) ∗ inv N (spawn_inv γ l Ψ))%I.
-- 
GitLab