Bump Iris (Transfinite algebra).

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" }
 ]
 

theories/examples/folly_queue/set.v

 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

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.

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.