diff --git a/coq-simuliris.opam b/coq-simuliris.opam
index fe51302affb3935350b908d847e4e4c78621d4b6..391e36d5d0be0fe42f202ba674cced8d17e06f03 100644
--- a/coq-simuliris.opam
+++ b/coq-simuliris.opam
@@ -8,8 +8,8 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/simuliris.git"
 synopsis: "Local Simulation proofs, the Iris style"
 
 depends: [
-  "coq-iris" { (= "dev.2024-10-30.0.27f837c1") | (= "dev") }
-  "coq-equations" { (= "1.3+8.19") | (= "1.3.1+8.20") }
+  "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") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/simulang/logical_heap.v b/theories/simulang/logical_heap.v
index 44bd5ba29ac0044eeec8c78ce1e6c704ff5808fc..4f5a9f8d4e1d8b6462bceb91ba7d02102df2282b 100644
--- a/theories/simulang/logical_heap.v
+++ b/theories/simulang/logical_heap.v
@@ -113,7 +113,7 @@ Section to_heap.
   Implicit Types σ : gmap loc (lock_state * val).
 
   Lemma to_heap_valid σ : ✓ to_heap σ.
-  Proof. intros l. rewrite lookup_fmap. case (σ !! l)=> [[[|n] v]|] //=. Qed.
+  Proof. intros l. rewrite lookup_fmap. case: (σ !! l)=> [[[|n] v]|] //=. Qed.
 
   Lemma lookup_to_heap_None σ l : σ !! l = None → to_heap σ !! l = None.
   Proof. by rewrite /to_heap lookup_fmap=> ->. Qed.
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.
diff --git a/theories/stacked_borrows/type.v b/theories/stacked_borrows/type.v
index 23bec750665ead64bfe751320488ba6eb73512aa..af14372236dad7f9c27e422677fa47c4dcef7688 100644
--- a/theories/stacked_borrows/type.v
+++ b/theories/stacked_borrows/type.v
@@ -263,10 +263,10 @@ Proof.
      | GenNode 5 Ts => Sum (go <$> Ts)
      | _ => FixedSize 0
      end) _).
-  fix FIX 1. intros [| | |Ts|Ts|Ts]; f_equal=>//; revert Ts; clear -FIX.
-  - fix FIX_INNER 1. intros []; [done|]. by simpl; f_equal.
-  - fix FIX_INNER 1. intros []; [done|]. by simpl; f_equal.
-  - fix FIX_INNER 1. intros []; [done|]. by simpl; f_equal.
+  fix FIX 1. intros [| | |Ts|Ts|Ts]; csimpl; f_equal=>//; revert Ts; clear -FIX.
+  - fix FIX_INNER 1. intros []; [done|]. by f_equal/=.
+  - fix FIX_INNER 1. intros []; [done|]. by f_equal/=.
+  - fix FIX_INNER 1. intros []; [done|]. by f_equal/=.
 Qed.
 
 (** Finding sum types *)