From 50b3a1f0983a2f12e19230bdf0e82d399faf4ab0 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 28 Jul 2021 09:50:51 +0200
Subject: [PATCH] Bump.

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

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index a63c781e..2d33a2f8 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-07-23.0.bc8c3ad9") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2021-07-27.0.774a97d1") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index ba52c8be..51ab71b8 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -244,8 +244,8 @@ Proof.
   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Λ').
-    destruct (decide (Λ = Λ')) as [<-|]; rewrite ?lookup_insert ?lookup_insert_ne //=.
-    assert ({[Λ]} ⊆ κ) by by apply gmultiset_elem_of_singleton_subseteq. auto. }
+    destruct (decide (Λ =  Λ')) as [<-|]; rewrite ?lookup_insert ?lookup_insert_ne //=.
+    assert ({[Λ]} ⊆ κ) by by apply gmultiset_singleton_subseteq_l. auto. }
   iModIntro. iModIntro. iExists A', I.
   rewrite /own_alft_auth /to_alftUR fmap_insert. iFrame "HA HI".
   rewrite HI !big_sepS_union //. iSplitL "HinvD".
-- 
GitLab