Bump.

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}%"]

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".