From d2b8a5fa5a60b316ebdbc2bb90feddf4147b9e48 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 4 Sep 2024 09:16:13 +0200
Subject: [PATCH] update dependencies

---
 coq-actris.opam                 | 2 +-
 theories/logrel/session_types.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/coq-actris.opam b/coq-actris.opam
index c14b302..1e75850 100644
--- a/coq-actris.opam
+++ b/coq-actris.opam
@@ -8,7 +8,7 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/actris/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/iris/actris.git"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2024-08-16.3.8890e30a") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2024-09-04.0.0653ba6c") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index 95af463..4d0c7ea 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -108,7 +108,7 @@ Section session_types.
   Global Instance lty_choice_proper a : Proper ((≡) ==> (≡)) (@lty_choice Σ a).
   Proof. apply ne_proper, _. Qed.
   Global Instance lty_choice_contractive a n :
-    Proper (map_relation (dist_later n) (λ _, False) (λ _, False) ==> dist n)
+    Proper (map_relation (λ _, dist_later n) (λ _ _, False) (λ _ _, False) ==> dist n)
            (@lty_choice Σ a).
   Proof.
     intros Ss Ts Heq. rewrite /lty_choice.
-- 
GitLab