From 0fe52ef4160f6b4497b075df345b85920f31c961 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Tue, 25 Aug 2020 17:07:06 +0200
Subject: [PATCH] Nits

---
 theories/examples/basics.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/examples/basics.v b/theories/examples/basics.v
index 041548b..7b5c15e 100644
--- a/theories/examples/basics.v
+++ b/theories/examples/basics.v
@@ -375,10 +375,10 @@ Proof.
   iIntros (Î¦) "_ HÎ¦". wp_lam.
   wp_apply (start_chan_spec prot_ref_loop); iIntros (c) "Hc".
   - do 4 wp_pure _. iLÃ¶b as "IH". wp_lam.
-    wp_recv (l x) as "Hl". wp_load. wp_store. wp_send with "[Hl//]".
+    wp_recv (l x) as "Hl". wp_load. wp_store. wp_send with "[$Hl]".
     do 2 wp_pure _. by iApply "IH".
   - wp_alloc l1 as "Hl1". wp_alloc l2 as "Hl2".
-    wp_send with "[Hl1//]". wp_send with "[Hl2//]".
+    wp_send with "[$Hl1]". wp_send with "[$Hl2]".
     wp_recv as "Hl1". wp_recv as "Hl2".
     wp_load. wp_load. wp_pures. by iApply "HÎ¦".
 Qed.
-- 
GitLab