diff --git a/coq-iris.opam b/coq-iris.opam index 93d6b5beeb84cefdda1777cf3d20417ff0be3a11..e77d9bb3960666f8a31920a43914fc7a04107687 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 c6d29f62f8f5fdb09b785e046aec0c609196e685..51d079b79b3e78bccb02384261745e66a8203c65 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 d50a4694d1a0afd6717f6daada8900bafaf5aa72..00f82ec26e336edbb86b3af185eeddeef6ea3f6d 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|].