tweak wp_tactics behavior for the case of ending up with a value

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.

heap_lang/tests.v

@@ -60,7 +60,7 @@ Section LiftingTests.
     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 {{ Φ }}.

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' =>