Commit 48892aba authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Change bound variable so that we do not have `Ψ v ∨ ...` but `Ψ w ∨ ...`.

parent e88994af
......@@ -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.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment