From 4e3fabc0dd91d9fd4cbe14110af180a56c99628e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 20 Apr 2021 19:15:39 +0200
Subject: [PATCH] Bump std++ (multisets).

---
 coq-lambda-rust.opam                  | 2 +-
 theories/lifetime/model/creation.v    | 3 ++-
 theories/lifetime/model/definitions.v | 4 ++--
 3 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index c341ec86..35fef32b 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2021-03-15.2.730f24ec") | (= "dev") }
+  "coq-iris" { (= "dev.2021-04-20.0.7a260d80") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index a9ee1e62..5000f19b 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -175,7 +175,8 @@ Proof.
     split; last done. by eapply gmultiset_elem_of_subseteq. }
   { intros κ ???. rewrite elem_of_difference elem_of_filter elem_of_dom. auto. }
   iModIntro. iMod ("Hclose" with "[-]") as "_"; last first.
-  { iModIntro. rewrite /lft_dead. iExists Λ. rewrite elem_of_singleton. auto. }
+  { iModIntro. rewrite /lft_dead. iExists Λ.
+    rewrite gmultiset_elem_of_singleton. auto. }
   iNext. iExists (<[Λ:=false]>A), I.
   rewrite /own_alft_auth /to_alftUR fmap_insert. iFrame "HA HI".
   rewrite HI !big_sepS_union //.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 022461a9..f1e0adff 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -19,7 +19,7 @@ End lft_notation.
 Definition static : lft := (∅ : gmultiset _).
 Instance lft_intersect : Meet lft := λ κ κ', κ ⊎ κ'.
 
-Definition positive_to_lft (p : positive) : lft := {[ p ]}.
+Definition positive_to_lft (p : positive) : lft := {[+ p +]}.
 
 Inductive bor_state :=
   | Bor_in
@@ -341,7 +341,7 @@ Proof. rewrite /lft_ctx. apply _. Qed.
 Global Instance positive_to_lft_inj : Inj eq eq positive_to_lft.
 Proof.
   unfold positive_to_lft. intros x y Hxy.
-  apply (elem_of_singleton_1 (C := lft)). rewrite -Hxy.
+  apply gmultiset_elem_of_singleton. rewrite -Hxy.
   set_solver.
 Qed.
 End basic_properties.
-- 
GitLab