From 26e93ebf7d4cfcd4c1c278c2e57ad0ae12a97ab6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 10 Mar 2017 12:20:16 +0100
Subject: [PATCH] rename wp_fupd_step -> wp_step_fupd. All other lemmas call
 them step_fupd.

---
 theories/program_logic/weakestpre.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 70acaa8dc..2e5428ddc 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -162,7 +162,7 @@ Proof.
     iDestruct "H" as %(? & ? & ? & ?). by edestruct (Hatomic _ _ _ _ Hstep).
 Qed.
 
-Lemma wp_fupd_step E1 E2 e P Φ :
+Lemma wp_step_fupd E1 E2 e P Φ :
   to_val e = None → E2 ⊆ E1 →
   (|={E1,E2}▷=> P) -∗ WP e @ E2 {{ v, P ={E1}=∗ Φ v }} -∗ WP e @ E1 {{ Φ }}.
 Proof.
@@ -218,7 +218,7 @@ Lemma wp_frame_step_l E1 E2 e Φ R :
   to_val e = None → E2 ⊆ E1 →
   (|={E1,E2}▷=> R) ∗ WP e @ E2 {{ Φ }} ⊢ WP e @ E1 {{ v, R ∗ Φ v }}.
 Proof.
-  iIntros (??) "[Hu Hwp]". iApply (wp_fupd_step with "Hu"); try done.
+  iIntros (??) "[Hu Hwp]". iApply (wp_step_fupd with "Hu"); try done.
   iApply (wp_mono with "Hwp"). by iIntros (?) "$$".
 Qed.
 Lemma wp_frame_step_r E1 E2 e Φ R :
-- 
GitLab