From 3efd62f5b5c2befeb66015ac59968607e1faa941 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Wed, 8 Dec 2021 17:54:03 +0100
Subject: [PATCH] Bumped stdpp

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

diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index e55928c..2005837 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -209,7 +209,7 @@ Proof.
     iApply iProto_le_trans; [|iApply (iProto_le_texist_intro_r _ x)]; simpl.
     iIntros "H". by iDestruct (HP with "H") as "$". }
   rewrite -wp_bind. eapply bi.wand_apply;
-    [by eapply (recv_spec _ (tele_app tv) (tele_app tP') (tele_app tp))|f_equiv].
+    [by eapply (recv_spec _ (tele_app tv) (tele_app tP') (tele_app tp))|f_equiv; first done].
   rewrite -bi.later_intro; apply bi.forall_intro=> x.
   specialize (HΦ x). destruct (envs_app _ _) as [Δ'|] eqn:HΔ'=> //.
   rewrite envs_app_sound //; simpl. by rewrite right_id HΦ.
-- 
GitLab