diff --git a/coq-iris-examples.opam b/coq-iris-examples.opam
index a383ea5b1ceebd2a84efd791ba61f552a2e66b56..47a53e975f1a972f3b7cec03432015a322c418c1 100644
--- a/coq-iris-examples.opam
+++ b/coq-iris-examples.opam
@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/examples.git"
 synopsis: "A collection of case studies for Iris -- not meant to be used as a dependency of anything"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2025-03-25.0.79d33e24") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2025-03-28.0.fa344cbe") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
 
diff --git a/theories/cl_logic/clprop.v b/theories/cl_logic/clprop.v
index 1b57a8c3b063f1401a7777b0df2e589f9c22175a..779a4e16c802309f4a5f525a05c712b52992a92f 100644
--- a/theories/cl_logic/clprop.v
+++ b/theories/cl_logic/clprop.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export ofe.
+From iris.algebra Require Export ofe stepindex_finite.
 From iris.bi Require Import notation.
 From iris.prelude Require Import options.