From e71bd415a6b75dc3082ac923ab3d5955651245b1 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sat, 24 Dec 2016 13:56:28 +0100
Subject: [PATCH] fix build.

---
 theories/lang/derived.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/theories/lang/derived.v b/theories/lang/derived.v
index 11795f1f..00d92652 100644
--- a/theories/lang/derived.v
+++ b/theories/lang/derived.v
@@ -71,7 +71,10 @@ Lemma wp_lam E xl e e' el Φ :
   Closed (xl +b+ []) e →
   subst_l xl el e = Some e' →
   ▷ WP e' @ E {{ Φ }} -∗ WP App (Lam xl e) el @ E {{ Φ }}.
-Proof. iIntros (???) "?". by iApply (wp_rec _ _ BAnon). Qed.
+Proof.
+  iIntros (???) "?". iApply (wp_rec _ _ BAnon)=>//.
+    by rewrite /= option_fmap_id.
+Qed.
 
 Lemma wp_let E x e1 e2 v Φ :
   to_val e1 = Some v →
-- 
GitLab