From 64bb048116d1c62f9f1aaf24bae2ee8277acd947 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 20 Jul 2016 11:21:11 +0200
Subject: [PATCH] Stronger masks for the WP of assert.

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

diff --git a/heap_lang/lib/assert.v b/heap_lang/lib/assert.v
index 5da29d450..3cc335765 100644
--- a/heap_lang/lib/assert.v
+++ b/heap_lang/lib/assert.v
@@ -7,8 +7,8 @@ Definition assert : val :=
 Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
 Global Opaque assert.
 
-Lemma wp_assert {Σ} (Φ : val → iProp heap_lang Σ) e `{!Closed [] e} :
-  WP e {{ v, v = #true ∧ ▷ Φ #() }} ⊢ WP assert: e {{ Φ }}.
+Lemma wp_assert {Σ} E (Φ : val → iProp heap_lang Σ) e `{!Closed [] e} :
+  WP e @ E {{ v, v = #true ∧ ▷ Φ #() }} ⊢ WP assert: e @ E {{ Φ }}.
 Proof.
   iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
   iApply wp_wand_r; iFrame "HΦ"; iIntros (v) "[% ?]"; subst.
-- 
GitLab