diff --git a/coq-gpfsl.opam b/coq-gpfsl.opam
index 4793653a7b343f0012b25b71d668dccd4aca8530..165eace98bc103396e09354e9e9640d5fa1afacf 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-10-03.0.70b30af7") | (= "dev") }
+  "coq-iris"  { (= "dev.2023-10-05.2.da1ec123") | (= "dev") }
   "coq-orc11" {= version}
 ]
 
diff --git a/coq-orc11.opam b/coq-orc11.opam
index fbca1bde4e1d4b93c1db728b8503114a601e5326..dbaff5cf85aed96626bed4d30a7de2153059dc40 100644
--- a/coq-orc11.opam
+++ b/coq-orc11.opam
@@ -10,7 +10,7 @@ version: "dev"
 synopsis: "A Coq formalization of the ORC11 semantics for weak memory"
 
 depends: [
-  "coq-stdpp" { (= "dev.2023-10-03.0.83c8fcbf") | (= "dev") }
+  "coq-stdpp" { (= "dev.2023-10-05.1.c57a2eed") | (= "dev") }
 ]
 
 build: ["./make-package" "orc11" "-j%{jobs}%"]
diff --git a/gpfsl-examples/list_helper.v b/gpfsl-examples/list_helper.v
index d5c39964bd25e3501fb39ebaa1b006ec4904972d..3c7ea936d1966f446d7f7441139a3d75e9205109 100644
--- a/gpfsl-examples/list_helper.v
+++ b/gpfsl-examples/list_helper.v
@@ -458,7 +458,7 @@ Proof.
   have EqL: length L11 = length L21.
   { revert ND HL1 HL2. rewrite -Eq. by apply NoDup_lookup. }
   have Eq1: L11 = L21.
-  { rewrite -(take_app L11 ([a] ++ L12)) -(take_app L21 ([a] ++ L22)).
+  { rewrite -(take_app_length L11 ([a] ++ L12)) -(take_app_length L21 ([a] ++ L22)).
     by rewrite Eq EqL. }
   by simplify_list_eq.
 Qed.
diff --git a/gpfsl-examples/queue/proof_ms_abs_graph.v b/gpfsl-examples/queue/proof_ms_abs_graph.v
index 659b6a828688a08618fe1f9949cad578149beda0..ddb84f161c7a3ae938e0837b6c0d6eb2e4267370 100644
--- a/gpfsl-examples/queue/proof_ms_abs_graph.v
+++ b/gpfsl-examples/queue/proof_ms_abs_graph.v
@@ -3431,8 +3431,8 @@ Proof.
           have Eq': (D2' ++ [(η2, n2)] ++ [(η2', n2')]).*1
                       = (D20 ++ [(η2, n2)] ++ D22).*1. { by f_equal. }
           move : Eq'. by rewrite !fmap_app. }
-        have EqL1 := take_app D2' ([(η2, n2)] ++ [(η2', n2')]).
-        have EqL2 := take_app D20 ([(η2, n2)] ++ D22).
+        have EqL1 := take_app_length D2' ([(η2, n2)] ++ [(η2', n2')]).
+        have EqL2 := take_app_length D20 ([(η2, n2)] ++ D22).
         rewrite EqD2' (_: length D2' = length D20) in EqL1.
         - by rewrite EqL1 in EqL2.
         - by rewrite -(fmap_length fst D2') -(fmap_length fst D20) Eq1. }
diff --git a/gpfsl-examples/stack/proof_treiber_history.v b/gpfsl-examples/stack/proof_treiber_history.v
index 6b93d6413e48e4f3bea0c2219fdab7dc8d1f815c..d615e49042fc4e3ecdd518b1ec29792fe57f86d5 100644
--- a/gpfsl-examples/stack/proof_treiber_history.v
+++ b/gpfsl-examples/stack/proof_treiber_history.v
@@ -212,7 +212,7 @@ Lemma length_concat_fmap_take_plus_S (f : _ → list event_id) gen1' emo x N
 Proof.
   apply lookup_lt_Some in GEN1 as LEgen1'.
   rewrite -{1}(take_drop gen1' emo).
-  rewrite take_add_app; last first. { rewrite take_length. lia. }
+  rewrite take_app_add'; last first. { rewrite take_length. lia. }
   rewrite fmap_app concat_app app_length.
   rewrite (drop_S _ _ _ GEN1). rewrite firstn_cons fmap_cons /=.
   rewrite app_length. done.