From 3dc4997caaa07578f38c783b6b1cd51c3006e301 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 20 Feb 2016 15:26:36 +0100
Subject: [PATCH] fix wp and wp> to be consistent with the other wp tactics
 (">" does *not* strip laters)

---
 heap_lang/tests.v      | 10 +++++-----
 heap_lang/wp_tactics.v |  4 ++--
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 34b146d67..787b7a8ca 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -33,10 +33,10 @@ Section LiftingTests.
      nclose N ⊆ E → heap_ctx N ⊑ || heap_e @ E {{ λ v, v = '2 }}.
   Proof.
     rewrite /heap_e=>HN. rewrite -(wp_mask_weaken N E) //.
-    wp> eapply wp_alloc; eauto. apply forall_intro=>l; apply wand_intro_l.
-    wp_rec. wp> eapply wp_load; eauto with I. apply sep_mono_r, wand_intro_l.
-    wp_bin_op. wp> eapply wp_store; eauto with I. apply sep_mono_r, wand_intro_l.
-    wp_rec. wp> eapply wp_load; eauto with I. apply sep_mono_r, wand_intro_l.
+    wp eapply wp_alloc; eauto. apply forall_intro=>l; apply wand_intro_l.
+    wp_rec. wp eapply wp_load; eauto with I. apply sep_mono_r, wand_intro_l.
+    wp_bin_op. wp eapply wp_store; eauto with I. apply sep_mono_r, wand_intro_l.
+    wp_rec. wp eapply wp_load; eauto with I. apply sep_mono_r, wand_intro_l.
       by apply const_intro.
   Qed.
 
@@ -76,7 +76,7 @@ Section LiftingTests.
   Lemma Pred_user E :
     (True : iProp) ⊑ || let: "x" := Pred '42 in Pred "x" @ E {{ λ v, v = '40 }}.
   Proof.
-    intros. ewp> apply Pred_spec. wp_rec. ewp> apply Pred_spec. auto with I.
+    intros. ewp apply Pred_spec. wp_rec. ewp apply Pred_spec. auto with I.
   Qed.
 End LiftingTests.
 
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 2f3722446..b9c546ec3 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -82,11 +82,11 @@ Tactic Notation "wp_focus" open_constr(efoc) :=
     match e' with efoc => unify e' efoc; wp_bind K end)
   end.
 
-Tactic Notation "wp" tactic(tac) :=
+Tactic Notation "wp" ">" tactic(tac) :=
   match goal with
   | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => wp_bind K; tac)
   end.
-Tactic Notation "wp" ">" tactic(tac) := (wp tac); wp_strip_later.
+Tactic Notation "wp" tactic(tac) := (wp> tac); wp_strip_later.
 
 (* In case the precondition does not match *)
 Tactic Notation "ewp" tactic(tac) := wp (etransitivity; [|tac]).
-- 
GitLab