From 2686709642ba19ebae56dfffaede7fa1c1f4dcc2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 21 Sep 2023 16:30:27 +0200
Subject: [PATCH] Bump Iris.
---
coq-iris.opam | 2 +-
iris/algebra/big_op.v | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/coq-iris.opam b/coq-iris.opam
index ea197dc71..e88b35623 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -28,7 +28,7 @@ tags: [
depends: [
"coq" { (>= "8.16" & < "8.19~") | (= "dev") }
- "coq-stdpp" { (= "dev.2023-09-14.0.4ff443de") | (= "dev") }
+ "coq-stdpp" { (= "dev.2023-09-21.2.7f6df4fa") | (= "dev") }
]
build: ["./make-package" "iris" "-j%{jobs}%"]
diff --git a/iris/algebra/big_op.v b/iris/algebra/big_op.v
index bf135d11a..98b6366c7 100644
--- a/iris/algebra/big_op.v
+++ b/iris/algebra/big_op.v
@@ -444,7 +444,7 @@ Section gmap.
{ by rewrite map_filter_empty !big_opM_empty. }
destruct (decide (φ (k, v))).
- rewrite map_filter_insert_True //.
- assert (filter φ m !! k = None) by (apply map_filter_lookup_None; eauto).
+ assert (filter φ m !! k = None) by (apply map_lookup_filter_None; eauto).
by rewrite !big_opM_insert // decide_True // IH.
- rewrite map_filter_insert_not' //; last by congruence.
rewrite !big_opM_insert // decide_False // IH. by rewrite left_id.
--
GitLab