From 302e8e895a0b53c3ce9ce5f9d54436addae9634b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 20 Apr 2021 20:17:11 +0200
Subject: [PATCH] Bump std++ (multisets).
---
coq-lambda-rust.opam | 2 +-
theories/lifetime/model/creation.v | 12 ++++++------
2 files changed, 7 insertions(+), 7 deletions(-)
diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index e7b8837e..6004d44f 100644
--- a/coq-lambda-rust.opam
+++ b/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}%"]
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 244e3ddb..1bcedb89 100644
--- a/theories/lifetime/model/creation.v
+++ b/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Λ').
--
GitLab