From 57a3c4ffe6988fc2e57ffa6183f696a95da53e98 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 9 Nov 2020 15:51:47 +0100
Subject: [PATCH] wp_pures: also handle [WP v]

---
 tests/heap_lang.v              | 4 ++++
 theories/heap_lang/proofmode.v | 6 ++++--
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 421093021..42940fee7 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -142,6 +142,10 @@ Section tests.
     P -∗ (∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}.
   Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
 
+  Lemma wp_pures_val (b : bool) :
+    ⊢ WP #b {{ _, True }}.
+  Proof. wp_pures. done. Qed.
+
   Lemma wp_cmpxchg l v :
     val_is_unboxed v →
     l ↦ v -∗ WP CmpXchg #l v v {{ _, True }}.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index d24214eb7..b5a5f78cc 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -107,8 +107,10 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
 (* TODO: do this in one go, without [repeat]. *)
 Ltac wp_pures :=
   iStartProof;
-  repeat (wp_pure _; []). (* The `;[]` makes sure that no side-condition
-                             magically spawns. *)
+  first [ (* The `;[]` makes sure that no side-condition magically spawns. *)
+          progress repeat (wp_pure _; [])
+        | wp_finish (* In case wp_pure never ran, make sure we do the usual cleanup. *)
+        ].
 
 (** Unlike [wp_pures], the tactics [wp_rec] and [wp_lam] should also reduce
 lambdas/recs that are hidden behind a definition, i.e. they should use
-- 
GitLab