Commit 5011fae3 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump std++.

parent 3fc3d3ff
......@@ -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}%"]
......
......@@ -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}.
......
......@@ -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|].
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment