From 13701476aea97082468aeae8a6dc416a736d3a5b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 8 Feb 2025 08:10:44 +0100
Subject: [PATCH] bump Iris
---
theories/examples/folly_queue/refinement.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/examples/folly_queue/refinement.v b/theories/examples/folly_queue/refinement.v
index fd8e564..9dadb62 100644
--- a/theories/examples/folly_queue/refinement.v
+++ b/theories/examples/folly_queue/refinement.v
@@ -1,6 +1,6 @@
From reloc Require Import reloc lib.lock.
From iris.algebra Require Import numbers csum excl auth list gmap gset.
-From iris.bi.lib Require Export fixpoint.
+From iris.bi.lib Require Export fixpoint_mono.
From reloc.examples.folly_queue Require Import
set turnSequencer singleElementQueue CG_queue mpmcqueue.
--
GitLab