Bump std++ (multisets).

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}%"]

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 //.

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.