From 4099b244f2eed16c19b7909052ae61c9a40f5c0c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 7 Feb 2025 14:15:52 +0100
Subject: [PATCH] update dependencies
---
coq-simuliris.opam | 2 +-
theories/simulation/closed_sim.v | 2 +-
theories/simulation/fairness_adequacy.v | 2 +-
theories/simulation/lifting.v | 2 +-
theories/simulation/slsls.v | 2 +-
5 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/coq-simuliris.opam b/coq-simuliris.opam
index c48ed08a..198a64d6 100644
--- a/coq-simuliris.opam
+++ b/coq-simuliris.opam
@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/simuliris.git"
synopsis: "Local Simulation proofs, the Iris style"
depends: [
- "coq-iris" { (= "dev.2025-01-25.1.8a8f05fb") | (= "dev") }
+ "coq-iris" { (= "dev.2025-02-07.0.d68b4fdb") | (= "dev") }
"coq-equations" { (= "1.3+8.19") | (= "1.3.1+8.20") | (= "1.3.1+9.0") | (= "dev") }
]
diff --git a/theories/simulation/closed_sim.v b/theories/simulation/closed_sim.v
index 5b4d62a8..53a7e70b 100644
--- a/theories/simulation/closed_sim.v
+++ b/theories/simulation/closed_sim.v
@@ -1,5 +1,5 @@
(** * Closed simulation (without the call case) *)
-From iris.bi Require Import bi fixpoint.
+From iris.bi Require Import bi fixpoint_mono.
From iris.proofmode Require Import proofmode.
From simuliris.simulation Require Import language.
From simuliris.simulation Require Export simulation slsls gen_log_rel.
diff --git a/theories/simulation/fairness_adequacy.v b/theories/simulation/fairness_adequacy.v
index 56490775..020778e7 100644
--- a/theories/simulation/fairness_adequacy.v
+++ b/theories/simulation/fairness_adequacy.v
@@ -1,5 +1,5 @@
From stdpp Require Import gmap.
-From iris.bi Require Import bi fixpoint.
+From iris.bi Require Import bi fixpoint_mono.
From iris.algebra Require Import gset gmap list.
From iris.proofmode Require Import proofmode.
From simuliris.simulation Require Import language fairness.
diff --git a/theories/simulation/lifting.v b/theories/simulation/lifting.v
index f7622c60..b36dc285 100644
--- a/theories/simulation/lifting.v
+++ b/theories/simulation/lifting.v
@@ -1,5 +1,5 @@
From simuliris.simulation Require Import language slsls.
-From iris Require Import bi.bi bi.lib.fixpoint.
+From iris Require Import bi.bi bi.lib.fixpoint_mono.
From iris.prelude Require Import options.
From iris.proofmode Require Import proofmode.
diff --git a/theories/simulation/slsls.v b/theories/simulation/slsls.v
index 51dc50b6..4be297c1 100644
--- a/theories/simulation/slsls.v
+++ b/theories/simulation/slsls.v
@@ -1,7 +1,7 @@
(** * SLSLS, Separation Logic Stuttering Local Simulation *)
From iris.algebra Require Export ofe.
-From iris.bi Require Import bi fixpoint.
+From iris.bi Require Import bi fixpoint_mono.
From iris.proofmode Require Import proofmode.
From simuliris.simulation Require Import language.
From simuliris.simulation Require Export simulation.
--
GitLab