From 37a694fd785615f94c6ff3c7de6318a27a189ee2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 28 Mar 2025 17:42:53 +0100
Subject: [PATCH] Bump Iris (Transfinite algebra).
---
coq-reloc.opam | 2 +-
theories/examples/folly_queue/set.v | 2 +-
theories/examples/stack_helping/helping_wrapper.v | 5 +----
theories/examples/stack_helping/stack.v | 5 +----
4 files changed, 4 insertions(+), 10 deletions(-)
diff --git a/coq-reloc.opam b/coq-reloc.opam
index 3c9ab2e..53b41d0 100644
--- a/coq-reloc.opam
+++ b/coq-reloc.opam
@@ -6,7 +6,7 @@ bug-reports: "https://gitlab.mpi-sws.org/dfrumin/reloc/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/dfrumin/reloc.git"
depends: [
- "coq-iris-heap-lang" { (= "dev.2025-02-07.0.d68b4fdb") | (= "dev") }
+ "coq-iris-heap-lang" { (= "dev.2025-03-28.0.fa344cbe") | (= "dev") }
"coq-autosubst" { = "dev" }
]
diff --git a/theories/examples/folly_queue/set.v b/theories/examples/folly_queue/set.v
index 843ea31..483f4a9 100644
--- a/theories/examples/folly_queue/set.v
+++ b/theories/examples/folly_queue/set.v
@@ -1,5 +1,5 @@
From stdpp Require Import base decidable.
-From iris.algebra Require Import numbers cmra excl.
+From iris.algebra Require Import numbers cmra excl stepindex_finite.
From reloc.prelude Require Import arith.
(* A camera of, potentially, infinite sets. Most of the lemmas are about sets of
diff --git a/theories/examples/stack_helping/helping_wrapper.v b/theories/examples/stack_helping/helping_wrapper.v
index acb7334..3efaf58 100644
--- a/theories/examples/stack_helping/helping_wrapper.v
+++ b/theories/examples/stack_helping/helping_wrapper.v
@@ -145,10 +145,7 @@ Section offerReg_rules.
rewrite left_id.
done.
}
- { (** TODO: this is silly *)
- assert (RightId (≡) (◯ ∅ : authUR offerRegR) (⋅)).
- { apply (@ucmra_unit_right_id (authUR offerRegR)). }
- rewrite right_id. iFrame "Hown". }
+ { done. }
iDestruct "Hown" as "[Ho Hown]".
rewrite right_id. iFrame.
assert ({[o := to_agree (v, (γ, k))]} ⋅ to_offer_reg N ≡ to_offer_reg N) as Hfoo.
diff --git a/theories/examples/stack_helping/stack.v b/theories/examples/stack_helping/stack.v
index 38b1971..5613a50 100644
--- a/theories/examples/stack_helping/stack.v
+++ b/theories/examples/stack_helping/stack.v
@@ -171,10 +171,7 @@ Section offerReg_rules.
rewrite left_id.
done.
}
- { (** TODO: this is silly *)
- assert (RightId (≡) (◯ ∅ : authUR offerRegR) (⋅)).
- { apply (@ucmra_unit_right_id (authUR offerRegR)). }
- rewrite right_id. iFrame "Hown". }
+ { done. }
iDestruct "Hown" as "[Ho Hown]".
rewrite right_id. iFrame.
assert ({[o := to_agree (v, (γ, k))]} ⋅ to_offer_reg N ≡ to_offer_reg N) as Hfoo.
--
GitLab