From 709da7352f2d80cf9328367753244ceb3f8731c1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 20 Feb 2016 16:38:55 +0100
Subject: [PATCH] tweak wp_tactics behavior for the case of ending up with a
 value

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

diff --git a/barrier/barrier.v b/barrier/barrier.v
index 1cd80abe2..1765e0820 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 127966266..94f223fae 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 0928595ec..3356f91ca 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' =>
-- 
GitLab