From 858f21a9e6c10e5a44052ebd083f18ccd54f053f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 16 Aug 2024 10:59:21 +0200
Subject: [PATCH] Bump std++ (length_X).

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

diff --git a/coq-actris.opam b/coq-actris.opam
index 08e7857..c14b302 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-03-12.0.c1e15cdc") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2024-08-16.3.8890e30a") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 4ab5fe0..1212dfb 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -260,7 +260,7 @@ Section channel.
     iIntros "#Hlbl' [Hctx H] !>".
     wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]").
     { iExists (vsl ++ [v]), vsr.
-      rewrite app_length /=.
+      rewrite length_app /=.
       replace (length vsl + 1) with (S (length vsl)) by lia.
       iFrame "#∗". }
     iIntros "_". iApply "HΦ". iExists γl, γr, γlk. eauto 10 with iFrame.
diff --git a/theories/logrel/session_typing_rules.v b/theories/logrel/session_typing_rules.v
index 5cac0e1..5dfafee 100644
--- a/theories/logrel/session_typing_rules.v
+++ b/theories/logrel/session_typing_rules.v
@@ -181,7 +181,7 @@ Section session_typing_rules.
     iIntros (Hdom) "!>". iIntros (vs) "$". iApply wp_value.
     iIntros (c) "Hc". wp_lam.
     rewrite -subst_map_singleton.
-    iApply lty_arr_list_spec; [by rewrite fmap_length|].
+    iApply lty_arr_list_spec; [by rewrite length_fmap|].
     iIntros (ws) "H".
     rewrite big_sepL2_fmap_l.
     iDestruct (big_sepL2_length with "H") as %Heq.
-- 
GitLab