From 8040549021b76339e89c72197a10d3839d89a320 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 11 Sep 2023 16:30:34 +0200
Subject: [PATCH] update dependencies
---
coq-iris.opam | 2 +-
iris/algebra/list.v | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/coq-iris.opam b/coq-iris.opam
index dd8f17bf5..b1b05537f 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -28,7 +28,7 @@ tags: [
depends: [
"coq" { (>= "8.15" & < "8.18~") | (= "dev") }
- "coq-stdpp" { (= "dev.2023-08-03.3.4be5fd62") | (= "dev") }
+ "coq-stdpp" { (= "dev.2023-09-11.1.b9418660") | (= "dev") }
]
build: ["./make-package" "iris" "-j%{jobs}%"]
diff --git a/iris/algebra/list.v b/iris/algebra/list.v
index f13aaf934..8c5aa2726 100644
--- a/iris/algebra/list.v
+++ b/iris/algebra/list.v
@@ -51,7 +51,7 @@ Proof. apply Forall2_cons_inv_r. Qed.
Definition list_ofe_mixin : OfeMixin (list A).
Proof.
split.
- - intros l k. rewrite equiv_Forall2 -Forall2_forall.
+ - intros l k. rewrite list_equiv_Forall2 -Forall2_forall.
split; induction 1; constructor; intros; try apply equiv_dist; auto.
- apply _.
- rewrite /dist /list_dist. eauto using Forall2_impl, dist_le with si_solver.
--
GitLab