From 226ad3bc0ff792099e59f2e074a5edeaa83da4ab Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 9 Apr 2020 16:34:11 +0200
Subject: [PATCH] =?UTF-8?q?wp=5Frec=5Fl=C3=B6b:=20make=20an=20assumption?=
 =?UTF-8?q?=20persistent?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 324dfa1da..05f0a8f3b 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -223,13 +223,13 @@ Implicit Types l : loc.
 induction directly, but this demonstrates that we can state the expected
 reasoning principle for recursive functions, without any visible â–·. *)
 Lemma wp_rec_löb s E f x e Φ Ψ :
-  □ ((∀ v, Ψ v -∗ WP (rec: f x := e)%V v @ s; E {{ Φ }}) -∗
+  □ ( □ (∀ v, Ψ v -∗ WP (rec: f x := e)%V v @ s; E {{ Φ }}) -∗
      ∀ v, Ψ v -∗ WP (subst' x v (subst' f (rec: f x := e) e)) @ s; E {{ Φ }}) -∗
   ∀ v, Ψ v -∗ WP (rec: f x := e)%V v @ s; E {{ Φ }}.
 Proof.
   iIntros "#Hrec". iLöb as "IH". iIntros (v) "HΨ".
   iApply lifting.wp_pure_step_later; first done.
-  iNext. iApply ("Hrec" with "[] HΨ"). iIntros (w) "HΨ".
+  iNext. iApply ("Hrec" with "[] HΨ"). iIntros "!#" (w) "HΨ".
   iApply ("IH" with "HΨ").
 Qed.
 
-- 
GitLab