update dependencies

coq-iris.opam

@@ -28,7 +28,7 @@ tags: [
 
 depends: [
   "coq" { (>= "8.13" & < "8.17~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2023-03-21.2.4e1880d2") | (= "dev") }
+  "coq-stdpp" { (= "dev.2023-03-24.1.504d165a") | (= "dev") }
 ]
 
 build: ["./make-package" "iris" "-j%{jobs}%"]

iris_unstable/base_logic/mono_list.v

@@ -121,7 +121,7 @@ Section mono_list_own.
     iDestruct 1 as (l1 Hl1) "H1". iDestruct 1 as (l2 Hl2) "H2".
     iDestruct (mono_list_lb_valid with "H1 H2") as %Hpre.
     iPureIntro.
-    destruct Hpre as [Hpre|Hpre]; eapply prefix_lookup in Hpre; eauto; congruence.
+    destruct Hpre as [Hpre|Hpre]; eapply prefix_lookup_Some in Hpre; eauto; congruence.
   Qed.
 
   Lemma mono_list_auth_idx_lookup γ q l i a :
@@ -130,7 +130,7 @@ Section mono_list_own.
     iIntros "Hauth". iDestruct 1 as (l1 Hl1) "Hl1".
     iDestruct (mono_list_auth_lb_valid with "Hauth Hl1") as %[_ Hpre].
     iPureIntro.
-    eapply prefix_lookup in Hpre; eauto; congruence.
+    eapply prefix_lookup_Some in Hpre; eauto; congruence.
   Qed.
 
   Lemma mono_list_lb_own_get γ q l :