diff --git a/coq-simuliris.opam b/coq-simuliris.opam
index c48ed08a218ec73b83ed345815c162b031abe23f..198a64d6b6d336955dc94970bcdf84c8597a24dc 100644
--- a/coq-simuliris.opam
+++ b/coq-simuliris.opam
@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/simuliris.git"
 synopsis: "Local Simulation proofs, the Iris style"
 
 depends: [
-  "coq-iris" { (= "dev.2025-01-25.1.8a8f05fb") | (= "dev") }
+  "coq-iris" { (= "dev.2025-02-07.0.d68b4fdb") | (= "dev") }
   "coq-equations" { (= "1.3+8.19") | (= "1.3.1+8.20") | (= "1.3.1+9.0") | (= "dev") }
 ]
 
diff --git a/theories/simulation/closed_sim.v b/theories/simulation/closed_sim.v
index 5b4d62a851e054cfb89e03927579aa29cc80c344..53a7e70beb2c5f36a7c5fce14f4de24319a532f5 100644
--- a/theories/simulation/closed_sim.v
+++ b/theories/simulation/closed_sim.v
@@ -1,5 +1,5 @@
 (** * Closed simulation (without the call case) *)
-From iris.bi Require Import bi fixpoint.
+From iris.bi Require Import bi fixpoint_mono.
 From iris.proofmode Require Import proofmode.
 From simuliris.simulation Require Import language.
 From simuliris.simulation Require Export simulation slsls gen_log_rel.
diff --git a/theories/simulation/fairness_adequacy.v b/theories/simulation/fairness_adequacy.v
index 56490775e397dca9dc1f4190a5396855386996dc..020778e7b877aef20ff7669ee24caea7007e8aff 100644
--- a/theories/simulation/fairness_adequacy.v
+++ b/theories/simulation/fairness_adequacy.v
@@ -1,5 +1,5 @@
 From stdpp Require Import gmap.
-From iris.bi Require Import bi fixpoint.
+From iris.bi Require Import bi fixpoint_mono.
 From iris.algebra Require Import gset gmap list.
 From iris.proofmode Require Import proofmode.
 From simuliris.simulation Require Import language fairness.
diff --git a/theories/simulation/lifting.v b/theories/simulation/lifting.v
index f7622c60f239fc0441d0837a8f93648e23bee8ee..b36dc2853184573d9446734b100bed0b2cdf2f40 100644
--- a/theories/simulation/lifting.v
+++ b/theories/simulation/lifting.v
@@ -1,5 +1,5 @@
 From simuliris.simulation Require Import language slsls.
-From iris Require Import bi.bi bi.lib.fixpoint.
+From iris Require Import bi.bi bi.lib.fixpoint_mono.
 From iris.prelude Require Import options.
 From iris.proofmode Require Import proofmode.
 
diff --git a/theories/simulation/slsls.v b/theories/simulation/slsls.v
index 51dc50b69dbb644297f8f610b1112672452e14dc..4be297c1195143f40155c74f59276ed9e4019cde 100644
--- a/theories/simulation/slsls.v
+++ b/theories/simulation/slsls.v
@@ -1,7 +1,7 @@
 (** * SLSLS, Separation Logic Stuttering Local Simulation *)
 
 From iris.algebra Require Export ofe.
-From iris.bi Require Import bi fixpoint.
+From iris.bi Require Import bi fixpoint_mono.
 From iris.proofmode Require Import proofmode.
 From simuliris.simulation Require Import language.
 From simuliris.simulation Require Export simulation.