From 593cca1fc43eabb68b2c918a3065e85718fa0e9e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 28 Mar 2025 17:40:39 +0100
Subject: [PATCH] Bump Iris (Transfinite algebra).
---
coq-iris-examples.opam | 2 +-
theories/cl_logic/clprop.v | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/coq-iris-examples.opam b/coq-iris-examples.opam
index a383ea5b..47a53e97 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 1b57a8c3..779a4e16 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.
--
GitLab