From a1171d022f5baa98470247494f8b7f3d86c8a73b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 25 Aug 2016 22:31:56 +0200
Subject: [PATCH] Use simpl more to get rid of %V scopes following 6d038c53.

---
 tests/counter.v  | 4 ++--
 tests/one_shot.v | 2 +-
 tests/tree_sum.v | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/tests/counter.v b/tests/counter.v
index 1a6f6c753..c5e84d11d 100644
--- a/tests/counter.v
+++ b/tests/counter.v
@@ -94,7 +94,7 @@ Lemma newcounter_spec N :
   heapN ⊥ N →
   heap_ctx ⊢ {{ True }} newcounter #() {{ v, ∃ l, v = #l ∧ C l 0 }}.
 Proof.
-  iIntros (?) "#Hh !# _ /=". rewrite /newcounter. wp_seq. wp_alloc l as "Hl".
+  iIntros (?) "#Hh !# _ /=". rewrite /newcounter /=. wp_seq. wp_alloc l as "Hl".
   iVs (own_alloc (Auth 0)) as (γ) "Hγ"; first done.
   rewrite (auth_frag_op 0 0) //; iDestruct "Hγ" as "[Hγ Hγf]".
   iVs (inv_alloc N _ (I γ l) with "[Hl Hγ]") as "#?".
@@ -128,7 +128,7 @@ Lemma read_spec l n :
   {{ C l n }} read #l {{ v, ∃ m : nat, ■ (v = #m ∧ n ≤ m) ∧ C l m }}.
 Proof.
   iIntros "!# Hl /=". iDestruct "Hl" as (N γ) "(% & #Hh & #Hinv & Hγf)".
-  rewrite /read. wp_let. iInv N as (c) "[Hl Hγ]" "Hclose". wp_load.
+  rewrite /read /=. wp_let. iInv N as (c) "[Hl Hγ]" "Hclose". wp_load.
   iDestruct (own_valid γ (Frag n ⋅ Auth c) with "[#]") as % ?%auth_frag_valid.
   { iApply own_op. by iFrame. }
   rewrite (auth_frag_op c c); last lia; iDestruct "Hγ" as "[Hγ Hγf']".
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 111a9f554..3e610b65d 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -42,7 +42,7 @@ Lemma wp_one_shot (Φ : val → iProp Σ) :
   ⊢ WP one_shot_example #() {{ Φ }}.
 Proof.
   iIntros "[#? Hf] /=".
-  rewrite /one_shot_example. wp_seq. wp_alloc l as "Hl". wp_let.
+  rewrite /one_shot_example /=. wp_seq. wp_alloc l as "Hl". wp_let.
   iVs (own_alloc Pending) as (γ) "Hγ"; first done.
   iVs (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
   { iNext. iLeft. by iSplitL "Hl". }
diff --git a/tests/tree_sum.v b/tests/tree_sum.v
index 18a8a4d89..73a023c11 100644
--- a/tests/tree_sum.v
+++ b/tests/tree_sum.v
@@ -60,7 +60,7 @@ Lemma sum_wp `{!heapG Σ} v t Φ :
   heap_ctx ★ is_tree v t ★ (is_tree v t -★ Φ #(sum t))
   ⊢ WP sum' v {{ Φ }}.
 Proof.
-  iIntros "(#Hh & Ht & HΦ)". rewrite /sum'.
+  iIntros "(#Hh & Ht & HΦ)". rewrite /sum' /=.
   wp_let. wp_alloc l as "Hl". wp_let.
   wp_apply sum_loop_wp; iFrame "Hh Ht Hl".
   rewrite Z.add_0_r.
-- 
GitLab