From fb31118ea8978b0f82f00ab8408960f7a3c11c64 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 28 Jul 2021 13:04:31 +0200
Subject: [PATCH] Bump std++ (filter_insert).
---
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 bd42daa32..91d6e3eca 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -15,7 +15,7 @@ iris.prelude, iris.algebra, iris.si_logic, iris.bi, iris.proofmode, iris.base_lo
depends: [
"coq" { (>= "8.12" & < "8.15~") | (= "dev") }
- "coq-stdpp" { (= "dev.2021-07-27.2.7d34364f") | (= "dev") }
+ "coq-stdpp" { (= "dev.2021-07-28.2.c4a352b1") | (= "dev") }
]
build: ["./make-package" "iris" "-j%{jobs}%"]
diff --git a/iris/algebra/big_op.v b/iris/algebra/big_op.v
index cdbc6298b..f6a7dd782 100644
--- a/iris/algebra/big_op.v
+++ b/iris/algebra/big_op.v
@@ -411,7 +411,7 @@ Section gmap.
induction m as [|k v m ? IH] using map_ind.
{ by rewrite map_filter_empty !big_opM_empty. }
destruct (decide (φ (k, v))).
- - rewrite map_filter_insert //.
+ - rewrite map_filter_insert_True //.
assert (filter φ m !! k = None) by (apply map_filter_lookup_None; eauto).
by rewrite !big_opM_insert // decide_True // IH.
- rewrite map_filter_insert_not' //; last by congruence.
--
GitLab