diff --git a/coq-diaframe.opam b/coq-diaframe.opam
index 00be89a3317db24f402eef20476add300fe5bbca..f1403ae9327adc5bf80a7792fb8acc2e63a66b72 100644
--- a/coq-diaframe.opam
+++ b/coq-diaframe.opam
@@ -7,7 +7,7 @@ authors: "Ike Mulder <me@ikemulder.nl>"
 homepage: "https://gitlab.mpi-sws.org/iris/diaframe/"
 bug-reports: "https://gitlab.mpi-sws.org/iris/diaframe/-/issues"
 depends: [
-  "coq-iris" { (>= "dev.2024-08-16.3.8890e30a" & <= "dev.2024-09-10.0.f14ebfde" ) | = "dev" | = "4.1.0" }
+  "coq-iris" { (>= "dev.2024-08-16.3.8890e30a" & <= "dev.2024-09-11.3.0203d5ca" ) | = "dev" | = "4.1.0" }
   "coq" { >= "8.18" & < "8.20~" }
 ]
 build: [make "-j%{jobs}%" "diaframe"]
diff --git a/diaframe/lib/own/validity_tactics.v b/diaframe/lib/own/validity_tactics.v
index 8acbc48d7f7ae45054c182c03cb9a1f06b5b5da7..edfa1121d826a0d84ea0ef4f0ccf43fb03c10d26 100644
--- a/diaframe/lib/own/validity_tactics.v
+++ b/diaframe/lib/own/validity_tactics.v
@@ -64,7 +64,7 @@ Proof.
 Qed.
 
 Ltac iCombineOwn_tac' Hs_raw destructstr := 
-  let Hs := words Hs_raw in
+  let Hs := String.words Hs_raw in
   let get_hyp_type Hname := 
     let Δ := match goal with | |- environments.envs_entails ?Δ _ => Δ end in
     let lookup := eval pm_eval in (environments.envs_lookup (INamed Hname) Δ) in
diff --git a/diaframe/steps/ipm_hyp_utils.v b/diaframe/steps/ipm_hyp_utils.v
index 052745f5e39422af8bea9cb69b95eaa265578fa8..84b698fb00c158271bd56998700bc9a40e69c757 100644
--- a/diaframe/steps/ipm_hyp_utils.v
+++ b/diaframe/steps/ipm_hyp_utils.v
@@ -48,7 +48,7 @@ Ltac2 string_to_coq_string (s : string) : constr :=
   let coq_byte_list : constr list 
     := List.init (String.length s) (fun i => char_to_coq_byte (String.get s i)) in
   let coq_bytes : constr := list_to_coq_list coq_byte_list in
-  let raw_result : constr := '(string_of_list_byte $coq_bytes) in
+  let raw_result : constr := '(String.string_of_list_byte $coq_bytes) in
   let result := Std.eval_cbv cbv_flags raw_result in
   result.