From 44dc86c8c305e56bae0cb96448d1fca2a44512d5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 24 Oct 2018 19:42:42 +0200
Subject: [PATCH] =?UTF-8?q?Use=20new=20`|=3D{E,E'}=E2=96=B7=3D>^n`=20notat?=
 =?UTF-8?q?ion=20at=20more=20places.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/program_logic/lifting.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 1185a506f..5533cb1d8 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -130,7 +130,7 @@ Qed.
 Lemma wp_pure_step_fupd `{Inhabited (state Λ)} s E E' e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
   φ →
-  Nat.iter n (λ P, |={E,E'}▷=> P) (WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
+  (|={E,E'}▷=>^n WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ).
   iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done.
-- 
GitLab