diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index 043afce2debdf80b51ce7f380e69af6a5be898bf..688af41d9176625189a88a55eb92029599258e69 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -57,7 +57,7 @@ Proof.
wp_seq. iApply wp_pvs. wp_alloc l as "Hl".
iPvs (own_alloc (Excl ())) as {γ} "Hγ"; first done.
iPvs (inv_alloc N _ (lock_inv γ l R) with "-[HΦ]") as "#?"; first done.
- { iNext. iExists false. by iFrame "Hl HR". }
+ { iIntros ">". iExists false. by iFrame "Hl HR". }
iPvsIntro. iApply "HΦ". iExists N, γ. by repeat iSplit.
Qed.
@@ -78,11 +78,9 @@ Qed.
Lemma release_spec R l (Φ : val → iProp) :
(locked l R ★ R ★ Φ #()) ⊢ WP release #l {{ Φ }}.
Proof.
- iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as {N γ} "(%&#?&#?&Hγ)".
+ iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as {N γ} "(% & #? & #? & Hγ)".
rewrite /release. wp_let.
- iInv N as "Hinv". iDestruct "Hinv" as {b} "[Hl Hγ']"; destruct b.
- - wp_store. iFrame "HΦ". iNext. iExists false. by iFrame "Hl HR Hγ".
- - wp_store. iDestruct "Hγ'" as "[Hγ' _]".
- iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as "%".
+ iInv N as "Hinv". iDestruct "Hinv" as {b} "[Hl _]".
+ wp_store. iFrame "HΦ". iNext. iExists false. by iFrame "Hl HR Hγ".
Qed.
End proof.