Merge branch 'ci/update-actris-to-dev.2024-09-04.0.d2b8a5fa' into 'master'

Update Actris to dev.2024-09-04.0.d2b8a5fa.

See merge request !24

supplements/coq-diaframe-actris.opam

@@ -10,7 +10,7 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/diaframe/-/issues"
 depends: [
   "coq-diaframe-heap-lang" {= version}
   "coq" { = "8.18.0" }
-  "coq-actris" { = "dev.2024-08-16.0.858f21a9" | = "~dev" }
+  "coq-actris" { = "dev.2024-09-04.0.d2b8a5fa" | = "~dev" }
 ]
 build: [make "-j%{jobs}%" "diaframe-actris"]
 install: [make "install-diaframe-actris"]

supplements/diaframe_actris/par_map.v

@@ -119,7 +119,7 @@ Section actris_test.
     iSteps as "Hmap Hlk Hclient". iLöb as "IH".
     wp_lam.
     iSteps as (ms _ n _ Hnms) "??" /
-           as (ms _ n _ Hnms [|]) "??? _".
+           as (ms _ n _ Hnms [|]) "????".
     { iPureIntro. destruct n; eauto. right. fold_leibniz. by apply Hnms. }
     - iSteps; iPureIntro; multiset_solver.
     - iSteps.
@@ -167,7 +167,7 @@ Section actris_test.
     {{ ys', RET #(); llist IA l [] ∗ llist IB k (ys' ++ ys) ∗ ⌜ys' ≡ₚ (xs ++ elements X) ≫= map⌝ }}.
   Proof.
     iStartProof2 => /=. iLöb as "IH" forall (n l xs X ys).
-    iStep as (HnX) "???". wp_lam. iSteps as "Hc" / as (n b) "Hc HSnX".
+    iStep as (HnX) "???". wp_lam. iSteps as "Hc" / as (n b) "HSnX Hc".
     { destruct HnX as [-> ->]; try lia.
       iSteps.
       iExists []; simpl.