diff --git a/coq-gpfsl.opam b/coq-gpfsl.opam
index d4e0f8056e59899da27c6e2aa89ef8b0c3f1d9e6..592fa6d7057f3c7c2769de6225a5e9bffe014593 100644
--- a/coq-gpfsl.opam
+++ b/coq-gpfsl.opam
@@ -10,7 +10,7 @@ version: "dev"
 synopsis: "A combination of GPS and FSL in the promising semantics WITHOUT promises"
 
 depends: [
-  "coq-iris"  { (= "dev.2023-07-24.5.6eb056bb") | (= "dev") }
+  "coq-iris"  { (= "dev.2023-07-25.2.621d76cf") | (= "dev") }
   "coq-orc11" {= version}
 ]
 
diff --git a/gpfsl-examples/queue/proof_hw_graph.v b/gpfsl-examples/queue/proof_hw_graph.v
index ef9d5a70eb90970d9995392acf7fa41590bd97dc..c2dbb52ec373b83dd25a3cc4e927ad3a837399c3 100644
--- a/gpfsl-examples/queue/proof_hw_graph.v
+++ b/gpfsl-examples/queue/proof_hw_graph.v
@@ -942,7 +942,7 @@ Proof.
   iIntros "SP". iExists v. iApply (own_mono with "SP").
   apply prod_included; split; [|done].
   apply prod_included; split; [done|].
-  apply auth_frag_mono, (singleton_mono (A:=per_slotUR)).
+  apply auth_frag_mono, (singleton_included_mono (A:=per_slotUR)).
   do 2 (apply prod_included; split; [|done]).
   apply prod_included. split; [done|by apply ucmra_unit_least].
 Qed.