From 19cd2645fad66ec5f36c5d26844653a1dd588897 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 2 Oct 2021 10:39:27 -0400
Subject: [PATCH] update dependencies; fix for f_equiv becoming a bit weaker

---
 opam                         | 2 +-
 theories/channel/proofmode.v | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/opam b/opam
index 3cde3f3..5d8b829 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2021-07-28.0.3424ace5") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2021-10-01.0.b9315f85") | (= "dev") }
 ]
diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index 4c55908..e55928c 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -389,7 +389,7 @@ Proof.
   rewrite envs_entails_eq /ProtoNormalize /= right_id=> ? Hp HΦ.
   rewrite envs_lookup_sound //; simpl.
   rewrite (iProto_mapsto_le _ _ (p1 <{P1}&{P2}> p2)%proto) -bi.later_intro -Hp left_id.
-  rewrite -wp_bind. eapply bi.wand_apply; [by eapply branch_spec|f_equiv].
+  rewrite -wp_bind. eapply bi.wand_apply; [by eapply branch_spec|f_equiv; first done].
   rewrite -bi.later_intro; apply bi.forall_intro=> b.
   specialize (HΦ b). destruct (envs_app _ _) as [Δ'|] eqn:HΔ'=> //.
   rewrite envs_app_sound //; simpl. by rewrite right_id HΦ.
@@ -443,7 +443,7 @@ Proof.
   rewrite envs_lookup_sound //; simpl.
   rewrite (iProto_mapsto_le _ _ (p1 <{P1}+{P2}> p2)%proto) -bi.later_intro -Hp left_id.
   rewrite -wp_bind. eapply bi.wand_apply; [by eapply select_spec|].
-  rewrite -assoc; f_equiv.
+  rewrite -assoc; f_equiv; first done.
   destruct (envs_split _ _ _) as [[Δ1 Δ2]|] eqn:? => //.
   destruct (envs_app _ _ _) as [Δ2'|] eqn:? => //.
   rewrite envs_split_sound //; rewrite (envs_app_sound Δ2) //; simpl.
-- 
GitLab