From 86672bcaf85eca0e06e21d366fa1b2cb9dcb673d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 26 Aug 2016 13:06:12 +0200
Subject: [PATCH] More simpl to reduce %V scopes.

---
 heap_lang/lib/counter.v      | 4 ++--
 tests/joining_existentials.v | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/heap_lang/lib/counter.v b/heap_lang/lib/counter.v
index 804e47c4e..f318d1b6b 100644
--- a/heap_lang/lib/counter.v
+++ b/heap_lang/lib/counter.v
@@ -36,7 +36,7 @@ Lemma newcounter_spec (R : iProp Σ) Φ :
   heapN ⊥ N →
   heap_ctx ★ (∀ l, counter l 0 -★ Φ #l) ⊢ WP newcounter #() {{ Φ }}.
 Proof.
-  iIntros (?) "[#Hh HΦ]". rewrite /newcounter. wp_seq. wp_alloc l as "Hl".
+  iIntros (?) "[#Hh HΦ]". rewrite /newcounter /=. wp_seq. wp_alloc l as "Hl".
   iVs (auth_alloc (counter_inv l) N _ (O:mnat) with "[Hl]")
     as (γ) "[#? Hγ]"; try by auto.
   iVsIntro. iApply "HΦ". rewrite /counter; eauto 10.
@@ -74,7 +74,7 @@ Lemma read_spec l j (Φ : val → iProp Σ) :
   ⊢ WP read #l {{ Φ }}.
 Proof.
   iIntros "[Hc HΦ]". iDestruct "Hc" as (γ) "(% & #? & #Hγ & Hγf)".
-  rewrite /read. wp_let.
+  rewrite /read /=. wp_let.
   iVs (auth_open (counter_inv l) with "[Hγf]") as (j') "(% & Hl & Hclose)"; auto.
   wp_load.
   iVs ("Hclose" $! (j `max` j') with "[Hl]") as "Hγf".
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index b9a7a6ca2..e06e47214 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -35,7 +35,7 @@ Lemma worker_spec e γ l (Φ Ψ : X → iProp Σ) `{!Closed [] e} :
   recv N l (barrier_res γ Φ) ★ (∀ x, {{ Φ x }} e {{ _, Ψ x }})
   ⊢ WP wait #l ;; e {{ _, barrier_res γ Ψ }}.
 Proof.
-  iIntros "[Hl #He]". wp_apply wait_spec; iFrame "Hl".
+  iIntros "[Hl #He]". wp_apply wait_spec; simpl; iFrame "Hl".
   iDestruct 1 as (x) "[#Hγ Hx]".
   wp_seq. iApply wp_wand_l. iSplitR; [|by iApply "He"].
   iIntros (v) "?"; iExists x; by iSplit.
-- 
GitLab