From 9b5ef3bf8cbaa0eec96f5583643f187abcf4d5bb Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 23 Jul 2021 11:46:22 +0200
Subject: [PATCH] Bump

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

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 65c16c0e..a63c781e 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-27.0.bf367fe7") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2021-07-23.0.bc8c3ad9") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index aa0f12f6..bd81be51 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -185,7 +185,6 @@ Proof.
     assert (↑mgmtN ## userE) by solve_ndisj. set_solver. }
   { done. }
   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.
   iDestruct "H" as (A I) "(% & HA & HI & Hinv)".
   rewrite /lft_tok /= big_sepMS_singleton. iDestruct "HΛ" as (V'0) "[#HV'0 HΛ]".
-- 
GitLab