diff --git a/barrier/barrier.v b/barrier/barrier.v
index 1cd80abe246705d56c47b616516d8097b658d9a2..1765e0820f5cb04b2e3317501d3592a1533e0d0d 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -298,7 +298,7 @@ Section proof.
     { (* Is this really the best way to strip the later? *)
       erewrite later_sep. apply sep_mono; last apply later_intro.
       rewrite ->later_sep. apply sep_mono_l. rewrite ->later_sep. done. }
-    wp_if. wp_value.
+    wp_if. 
     eapply wand_apply_r; [done..|]. eapply wand_apply_r; [done..|].
     apply: (eq_rewrite Q' Q (λ x, x)%I); last by eauto with I.
     rewrite eq_sym. eauto with I.
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 127966266dcd3bc85621bda81e487e0fd1ea335b..94f223fae6214752d7af7043826b0f525eb88aff 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -54,13 +54,13 @@ Section LiftingTests.
     revert n1; apply löb_all_1=>n1.
     rewrite (comm uPred_and (â–  _)%I) assoc; apply const_elim_r=>?.
     (* first need to do the rec to get a later *)
-    wp_rec>.
+    wp_rec>. 
     (* FIXME: ssr rewrite fails with "Error: _pattern_value_ is used in conclusion." *)
     rewrite ->(later_intro (Φ _)); rewrite -!later_and; apply later_mono.
     wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
     - rewrite (forall_elim (n1 + 1)) const_equiv; last omega.
       by rewrite left_id impl_elim_l.
-    - wp_value. assert (n1 = n2 - 1) as -> by omega; auto with I.
+    - assert (n1 = n2 - 1) as -> by omega; auto with I.
   Qed.
 
   Lemma Pred_spec n E Φ : ▷ Φ (LitV (n - 1)) ⊑ || Pred 'n @ E {{ Φ }}.
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 0928595ec8618f5de3750c3f244b93ceab89b084..3356f91ca7686c6341dafae3557b6a03764a5865 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -25,18 +25,14 @@ Ltac wp_finish :=
   match goal with
   | |- _ ⊑ ▷ _ => etransitivity; [|apply later_mono; go; reflexivity]
   | |- _ ⊑ wp _ _ _ =>
-     etransitivity; [|eapply wp_value; reflexivity];
+     etransitivity; [|eapply wp_value_pvs; reflexivity];
      (* sometimes, we will have to do a final view shift, so only apply
      wp_value if we obtain a consecutive wp *)
-     match goal with |- _ ⊑ wp _ _ _ => simpl | _ => fail end
+     try (eapply pvs_intro;
+          match goal with |- _ ⊑ wp _ _ _ => simpl | _ => fail end)
   | _ => idtac
   end in simpl; revert_intros go.
 
-Tactic Notation "wp_value" :=
-  match goal with
-  | |- _ ⊑ wp ?E ?e ?Q => etransitivity; [|eapply wp_value; reflexivity]; simpl
-  end.
-
 Tactic Notation "wp_rec" ">" :=
   match goal with
   | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>