Bump std++ (multisets).

coq-lambda-rust.opam

@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2021-04-14.2.89510b36") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2021-04-20.0.13632051") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]

theories/lifetime/model/creation.v

@@ -171,7 +171,7 @@ Proof.
     - iDestruct "H" as "[[Hκ %]|[Hκ %]]".
       + iLeft. iFrame "Hκ". iPureIntro. by apply lft_alive_in_insert.
       + iRight. iFrame "Hκ". iPureIntro. by apply lft_dead_in_insert. }
-  iModIntro; iExists {[ Λ ]}. iSplitL.
+  iModIntro; iExists {[+ Λ +]}. iSplitL.
   { rewrite /lft_tok big_sepMS_singleton. iExists _. iFrame.
     iDestruct (monPred_in_intro True%I with "[//]") as (V) "[H _]".
     by rewrite -(lat_bottom_sqsubseteq V). }
@@ -180,7 +180,7 @@ Proof.
   { assert (↑mgmtN ## E0) by (pose proof E0_lftN_disj; solve_ndisj). set_solver. }
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
   { rewrite <-union_subseteq_l. solve_ndisj. }
-  iMod (ilft_create _ _ {[Λ]} with "HA HI Hinv") as "H". clear A I.
+  iMod (ilft_create _ _ {[+ Λ +]} with "HA HI Hinv") as "H". clear A I.
   iDestruct "H" as (A I) "(% & HA & HI & Hinv)".
   rewrite /lft_tok /= big_sepMS_singleton. iDestruct "HΛ" as (V'0) "[#HV'0 HΛ]".
   iDestruct (own_valid_2 with "HA HΛ")
@@ -237,12 +237,12 @@ Proof.
     case Hκ=>// Hd. by destruct (lft_alive_and_dead_in A κ). }
   iModIntro. iMod ("Hclose" with "[-]") as "_"; last first.
   { iModIntro. rewrite /lft_dead. iExists Λ, _. iIntros "{$HΛ}".
-    rewrite elem_of_singleton. iSplit; [done|].
-    assert (Hhv : lft_has_view A {[Λ]} (Vs {[Λ]})) by auto.
-    move: (Hhv Λ). rewrite elem_of_singleton. revert EQAΛ.
+    rewrite gmultiset_elem_of_singleton. iSplit; [done|].
+    assert (Hhv : lft_has_view A {[+ Λ +]} (Vs {[+ Λ +]})) by auto.
+    move: (Hhv Λ). rewrite gmultiset_elem_of_singleton. revert EQAΛ.
     case: (A!!Λ)=>[[??]|]; [|intros EQ; by inversion EQ]. simpl.
     intros [_ ->]%(inj Some)%(inj2 pair)=>/(_ eq_refl) <- //. }
-  set (A' := <[Λ:=(false, Vs {[Λ]})]>A).
+  set (A' := <[Λ:=(false, Vs {[+ Λ +]})]>A).
   assert (Hhv : ∀ κ, κ ∈ dom (gset _) I → lft_has_view A' κ (Vs κ)).
   { intros κ Hκ Λ' HΛ'. assert (Hhv : lft_has_view A κ (Vs κ)) by auto.
     specialize (Hhv Λ' HΛ').