From 7fef7ccb1d344874373167f85ae517d8d264f274 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 26 Jan 2021 13:40:15 +0100
Subject: [PATCH] Make better use of `wp_smart_apply`.

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

diff --git a/theories/examples/basics.v b/theories/examples/basics.v
index bee5f69..62a1972 100644
--- a/theories/examples/basics.v
+++ b/theories/examples/basics.v
@@ -284,7 +284,7 @@ Proof.
   wp_smart_apply (start_chan_spec prot_loop); iIntros (c) "Hc".
   - iLöb as "IH".
     wp_recv (x) as "_". wp_send with "[//]".
-    do 2 wp_pure _. by iApply "IH".
+    by wp_smart_apply "IH".
   - wp_send with "[//]". wp_recv as "_". wp_send with "[//]". wp_recv as "_".
     wp_pures. by iApply "HΦ".
 Qed.
@@ -355,7 +355,7 @@ Proof.
   wp_smart_apply (start_chan_spec prot_loop); iIntros (c) "Hc".
   - iLöb as "IH".
     wp_recv (x) as "_". wp_send with "[//]".
-    do 2 wp_pure _. by iApply "IH".
+    by wp_smart_apply "IH".
   - wp_send with "[//]". wp_send with "[//]". wp_recv as "_". wp_recv as "_".
     wp_pures. by iApply "HΦ".
 Qed.
@@ -369,7 +369,7 @@ Proof.
   wp_smart_apply (start_chan_spec prot_ref_loop); iIntros (c) "Hc".
   - iLöb as "IH". wp_lam.
     wp_recv (l x) as "Hl". wp_load. wp_store. wp_send with "[$Hl]".
-    do 2 wp_pure _. by iApply "IH".
+    by wp_smart_apply "IH".
   - wp_alloc l1 as "Hl1". wp_alloc l2 as "Hl2".
     wp_send with "[$Hl1]". wp_send with "[$Hl2]".
     wp_recv as "Hl1". wp_recv as "Hl2".
-- 
GitLab