From 5011fae3552d3ad74095d5761630b9383abe4dd2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 12 Mar 2021 07:12:38 +0100
Subject: [PATCH] Bump std++.
---
coq-iris.opam | 2 +-
iris/algebra/lib/gset_bij.v | 2 +-
iris/base_logic/lib/gset_bij.v | 2 +-
3 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/coq-iris.opam b/coq-iris.opam
index 93d6b5bee..e77d9bb39 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -14,7 +14,7 @@ iris.prelude, iris.algebra, iris.si_logic, iris.bi, iris.proofmode, iris.base_lo
depends: [
"coq" { (>= "8.11" & < "8.14~") | (= "dev") }
- "coq-stdpp" { (= "dev.2021-03-05.0.9a0f8631") | (= "dev") }
+ "coq-stdpp" { (= "dev.2021-03-11.0.6d001c9d") | (= "dev") }
]
build: ["./make-package" "iris" "-j%{jobs}%"]
diff --git a/iris/algebra/lib/gset_bij.v b/iris/algebra/lib/gset_bij.v
index c6d29f62f..51d079b79 100644
--- a/iris/algebra/lib/gset_bij.v
+++ b/iris/algebra/lib/gset_bij.v
@@ -108,7 +108,7 @@ Definition gset_bijUR A B `{Countable A, Countable B} : ucmra :=
Definition gset_bij_auth `{Countable A, Countable B}
(dq : dfrac) (L : gset (A * B)) : gset_bij A B := â—V{dq} L â‹… â—¯V L.
Definition gset_bij_elem `{Countable A, Countable B}
- (a : A) (b : B) : gset_bij A B := â—¯V {[a, b]}.
+ (a : A) (b : B) : gset_bij A B := â—¯V {[ (a, b) ]}.
Section gset_bij.
Context `{Countable A, Countable B}.
diff --git a/iris/base_logic/lib/gset_bij.v b/iris/base_logic/lib/gset_bij.v
index d50a4694d..00f82ec26 100644
--- a/iris/base_logic/lib/gset_bij.v
+++ b/iris/base_logic/lib/gset_bij.v
@@ -139,7 +139,7 @@ Section gset_bij.
gset_bij_own_auth γ (DfracOwn 1) ({[(a, b)]} ∪ L) ∗ gset_bij_own_elem γ a b.
Proof.
iIntros (??) "Hauth".
- iAssert (gset_bij_own_auth γ (DfracOwn 1) ({[a, b]} ∪ L)) with "[> Hauth]" as "Hauth".
+ iAssert (gset_bij_own_auth γ (DfracOwn 1) ({[(a, b)]} ∪ L)) with "[> Hauth]" as "Hauth".
{ rewrite gset_bij_own_auth_eq. iApply (own_update with "Hauth").
by apply gset_bij_auth_extend. }
iModIntro. iSplit; [done|].
--
GitLab