From 0392605fa9668270b18167f99d7d365b08883087 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 18 Jun 2021 09:46:47 +0200
Subject: [PATCH] update dependencies

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

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 48f00a75..0a58cdf7 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-06-06.0.5b953c99") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2021-06-18.0.336531e4") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index d4ed860e..aa0f12f6 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -206,7 +206,7 @@ Proof.
     by inversion EQ. }
   iDestruct (exists_Vs with "Hinv") as (Vs) "(>% & >% & Hinv)".
   iMod (own_update_2 with "HA HΛ") as "[HA HΛ]".
-  { destruct (equiv_Some_inv_r' _ _ Eqs) as (? & ? & ?).
+  { apply Some_equiv_eq in Eqs as (? & ? & ?).
     by eapply auth_update, singleton_local_update,
        (exclusive_local_update _ (Cinr (to_agree (to_latT (Vs {[Λ]}))))). }
   iDestruct "HΛ" as "#HΛ". iModIntro; iNext.
-- 
GitLab