diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index bcea9d2e95110b8ab5e503cb97a67f354836dab5..a9597b39f9bc02898ff5abd4369f3fc02f33080b 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -81,7 +81,7 @@ Proof.
   rewrite -(wp_lift_pure_det_step (Fork e) (Lit LitUnit) (Some e)) //=;
     last by intros; inv_step; eauto.
   apply later_mono, sep_intro_True_l; last done.
-  by rewrite -(wp_value' _ _ (Lit _)) //; apply const_intro.
+  by rewrite -(wp_value _ _ (Lit _)) //; apply const_intro.
 Qed.
 
 (* For the lemmas involving substitution, we only derive a preliminary version.
@@ -100,7 +100,7 @@ Lemma wp_un_op E op l l' Q :
   ▷ Q (LitV l') ⊑ wp E (UnOp op (Lit l)) Q.
 Proof.
   intros. rewrite -(wp_lift_pure_det_step (UnOp op _) (Lit l') None)
-    ?right_id -?wp_value' //; intros; inv_step; eauto.
+    ?right_id -?wp_value //; intros; inv_step; eauto.
 Qed.
 
 Lemma wp_bin_op E op l1 l2 l' Q :
@@ -108,7 +108,7 @@ Lemma wp_bin_op E op l1 l2 l' Q :
   ▷ Q (LitV l') ⊑ wp E (BinOp op (Lit l1) (Lit l2)) Q.
 Proof.
   intros Heval. rewrite -(wp_lift_pure_det_step (BinOp op _ _) (Lit l') None)
-    ?right_id -?wp_value' //; intros; inv_step; eauto.
+    ?right_id -?wp_value //; intros; inv_step; eauto.
 Qed.
 
 Lemma wp_if_true E e1 e2 Q : ▷ wp E e1 Q ⊑ wp E (If (Lit $ LitBool true) e1 e2) Q.
@@ -128,7 +128,7 @@ Lemma wp_fst E e1 v1 e2 v2 Q :
   ▷ Q v1 ⊑ wp E (Fst $ Pair e1 e2) Q.
 Proof.
   intros. rewrite -(wp_lift_pure_det_step (Fst _) e1 None)
-    ?right_id -?wp_value' //; intros; inv_step; eauto.
+    ?right_id -?wp_value //; intros; inv_step; eauto.
 Qed.
 
 Lemma wp_snd E e1 v1 e2 v2 Q :
@@ -136,7 +136,7 @@ Lemma wp_snd E e1 v1 e2 v2 Q :
   ▷ Q v2 ⊑ wp E (Snd $ Pair e1 e2) Q.
 Proof.
   intros. rewrite -(wp_lift_pure_det_step (Snd _) e2 None)
-    ?right_id -?wp_value' //; intros; inv_step; eauto.
+    ?right_id -?wp_value //; intros; inv_step; eauto.
 Qed.
 
 Lemma wp_case_inl' E e0 v0 x1 e1 x2 e2 Q :
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index a459db55cafcab3d6305db015a5dfc8ed06d9f70..b790ed7fc47c90e22d41859efa1583f6a9a431d5 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -47,7 +47,7 @@ Module LiftingTests.
     { by rewrite lookup_insert. }
     { done. }
     rewrite -later_intro. apply wand_intro_l. rewrite right_id.
-    rewrite -wp_seq -wp_value -later_intro.
+    rewrite -wp_seq -wp_value' -later_intro.
     rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
     { by rewrite lookup_insert. }
     rewrite -later_intro. apply wand_intro_l. rewrite right_id.
@@ -69,7 +69,7 @@ Module LiftingTests.
     rewrite (comm uPred_and (â–  _)%I) assoc; apply const_elim_r=>?.
     (* first need to do the rec to get a later *)
     rewrite -(wp_bindi (AppLCtx _)) /=.
-    rewrite -wp_rec // =>-/=; rewrite -wp_value' //=.
+    rewrite -wp_rec // =>-/=; rewrite -wp_value //=.
     (* FIXME: ssr rewrite fails with "Error: _pattern_value_ is used in conclusion." *)
     rewrite ->(later_intro (Q _)).
     rewrite -!later_and; apply later_mono.
@@ -83,7 +83,7 @@ Module LiftingTests.
       by rewrite left_id impl_elim_l.
     - assert (n1 = n2 - 1) as -> by omega.
       rewrite -wp_if_false -!later_intro.
-      by rewrite -wp_value' // and_elim_r.
+      by rewrite -wp_value // and_elim_r.
   Qed.
 
   Lemma Pred_spec n E Q : ▷ Q (LitV (n - 1)) ⊑ wp E (Pred 'n)%L Q.
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 0b9f597d9f82588737a5156f25dcf63e800bb6ae..7a480e0a5a1f8c0844f51e870d759c496f67d5bb 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -33,7 +33,7 @@ Lemma ht_val E v :
   {{ True : iProp Λ Σ }} of_val v @ E {{ λ v', v = v' }}.
 Proof.
   apply (always_intro _ _), impl_intro_l.
-  by rewrite -wp_value; apply const_intro.
+  by rewrite -wp_value'; apply const_intro.
 Qed.
 Lemma ht_vs E P P' Q Q' e :
   ((P ={E}=> P') ∧ {{ P' }} e @ E {{ Q' }} ∧ ∀ v, Q' v ={E}=> Q v)
diff --git a/program_logic/hoare_lifting.v b/program_logic/hoare_lifting.v
index 97e4ae95ade2d66f9a60c24bb4657062cc3f34d2..8037950c963f89d562770afcc7e14c23ab8c792a 100644
--- a/program_logic/hoare_lifting.v
+++ b/program_logic/hoare_lifting.v
@@ -68,7 +68,7 @@ Proof.
     by repeat apply and_intro; try apply const_intro.
   * apply (always_intro _ _), impl_intro_l; rewrite and_elim_l.
     rewrite -always_and_sep_r; apply const_elim_r=>-[[v Hv] ?].
-    rewrite -(of_to_val e2 v) // -wp_value.
+    rewrite -(of_to_val e2 v) // -wp_value'; [].
     rewrite -(exist_intro σ2) -(exist_intro ef) (of_to_val e2) //.
     by rewrite -always_and_sep_r; apply and_intro; try apply const_intro.
 Qed.
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index ab3bdf53f27f2812727c10e1a06e10831df6a9ba..72f586b2c752589a2e38e51c9551c574a0e13029 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -75,7 +75,7 @@ Proof.
   apply const_elim_l=>-[v2' [Hv ?]] /=.
   rewrite -pvs_intro.
   rewrite (forall_elim v2') (forall_elim σ2') (forall_elim ef) const_equiv //.
-  by rewrite left_id wand_elim_r -(wp_value' _ _ e2' v2').
+  by rewrite left_id wand_elim_r -(wp_value _ _ e2' v2').
 Qed.
 
 Lemma wp_lift_atomic_det_step {E Q e1} σ1 v2 σ2 ef :
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index f62849532d3b81d1791b301663e44b32294774b2..784e2290d8a1833dcb479fb379e97541f539b201 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -105,7 +105,7 @@ Lemma wp_step_inv E Ef Q e k n σ r rf :
   wp_go (E ∪ Ef) (λ e, wp E e Q) (λ e, wp coPset_all e (λ _, True%I)) k rf e σ.
 Proof. intros He; destruct 3; [by rewrite ?to_of_val in He|eauto]. Qed.
 
-Lemma wp_value E Q v : Q v ⊑ wp E (of_val v) Q.
+Lemma wp_value' E Q v : Q v ⊑ wp E (of_val v) Q.
 Proof. by constructor; apply pvs_intro. Qed.
 Lemma pvs_wp E e Q : pvs E E (wp E e Q) ⊑ wp E e Q.
 Proof.
@@ -204,8 +204,8 @@ Global Instance wp_mono' E e :
 Proof. by intros Q Q' ?; apply wp_mono. Qed.
 Lemma wp_strip_pvs E e P Q : P ⊑ wp E e Q → pvs E E P ⊑ wp E e Q.
 Proof. move=>->. by rewrite pvs_wp. Qed.
-Lemma wp_value' E Q e v : to_val e = Some v → Q v ⊑ wp E e Q.
-Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value. Qed.
+Lemma wp_value E Q e v : to_val e = Some v → Q v ⊑ wp E e Q.
+Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed.
 Lemma wp_frame_l E e Q R : (R ★ wp E e Q) ⊑ wp E e (λ v, R ★ Q v).
 Proof. setoid_rewrite (comm _ R); apply wp_frame_r. Qed.
 Lemma wp_frame_later_l E e Q R :