diff --git a/coq-gpfsl.opam b/coq-gpfsl.opam
index 6558f991b34773aba23a6aae8dfea2133d6c0143..d4e0f8056e59899da27c6e2aa89ef8b0c3f1d9e6 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-06-04.0.695533ab") | (= "dev") }
+  "coq-iris"  { (= "dev.2023-07-24.5.6eb056bb") | (= "dev") }
   "coq-orc11" {= version}
 ]
 
diff --git a/gpfsl-examples/queue/proof_hw_graph.v b/gpfsl-examples/queue/proof_hw_graph.v
index 4a860da70f6975f3452a36be843739f4873cbb67..ef9d5a70eb90970d9995392acf7fa41590bd97dc 100644
--- a/gpfsl-examples/queue/proof_hw_graph.v
+++ b/gpfsl-examples/queue/proof_hw_graph.v
@@ -1294,7 +1294,7 @@ Proof.
   iIntros "SD". rewrite /slot_dequeued /slot_enqueued.
   iApply (own_mono with "SD").
   apply pair_included; split; [|done]. apply pair_included; split; [done|].
-  apply auth_frag_mono, singleton_included. right. simpl.
+  apply auth_frag_mono, singleton_included. apply Some_included. right. simpl.
   apply pair_included; split; [|done]. apply pair_included; split; [done|].
   apply option_included. by left.
 Qed.
diff --git a/gpfsl/algebra/to_agree.v b/gpfsl/algebra/to_agree.v
index a50bd8367bbadc00fb0161eb689518ad6d06316e..074dc2d5d67cf74a32c2fbe9429363bd72436813 100644
--- a/gpfsl/algebra/to_agree.v
+++ b/gpfsl/algebra/to_agree.v
@@ -162,7 +162,7 @@ Proof.
   have ?: ✓ (to_agreeM m ⋅ to_agreeM {[k := a]}).
   { rewrite -to_agreeM_insert //. apply to_agreeM_valid. }
   rewrite to_agreeM_insert //. apply local_update_valid.
-  intros _ _ [<-%to_agreeM_agree|INCL%to_agreeM_included].
+  intros _ _ [<-%to_agreeM_agree|INCL%to_agreeM_included]%Some_included_1.
   - rewrite to_agreeM_insert //. by apply agreeM_local_update_retain.
   - rewrite to_agreeM_insert.
     + by apply agreeM_local_update_retain.