From be8849c2951ade7688ad7089ba8766abaa9805c8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 20 Sep 2017 20:52:59 +0200
Subject: [PATCH] Get rid of wp_value.

The tactic was doing something weird and only once used.
---
 theories/heap_lang/lib/par.v   | 4 ++--
 theories/heap_lang/proofmode.v | 8 --------
 2 files changed, 2 insertions(+), 10 deletions(-)

diff --git a/theories/heap_lang/lib/par.v b/theories/heap_lang/lib/par.v
index 6e289acc3..5b681ca30 100644
--- a/theories/heap_lang/lib/par.v
+++ b/theories/heap_lang/lib/par.v
@@ -27,8 +27,8 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) e (f1 f2 : val) (Φ : val → iProp
   (▷ ∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) -∗
   WP par e {{ Φ }}.
 Proof.
-  iIntros (?) "Hf1 Hf2 HΦ".
-  rewrite /par. wp_value. wp_let. wp_proj.
+  iIntros (<-%of_to_val) "Hf1 Hf2 HΦ".
+  rewrite /par /=. wp_let. wp_proj.
   wp_apply (spawn_spec parN with "Hf1"); try wp_done; try solve_ndisj.
   iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
   iApply (wp_wand with "Hf2"); iIntros (v) "H2". wp_let.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 8f2f4b961..8e4629a2c 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -24,14 +24,6 @@ Ltac wp_done :=
 
 Ltac wp_value_head := etrans; [|eapply wp_value; wp_done]; simpl.
 
-Tactic Notation "wp_value" :=
-  iStartProof;
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    wp_bind_core K; wp_value_head) || fail "wp_value: cannot find value in" e
-  | _ => fail "wp_value: not a wp"
-  end.
-
 Lemma of_val_unlock v e : of_val v = e → of_val (locked v) = e.
 Proof. by unlock. Qed.
 
-- 
GitLab