Merge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coq

opam.pins

-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq d1ec2aec60d1f069d5ed15282d7a2cfd1e8fb499
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 8b9f59ab3630176149621661c8f3ee7b456dfe5f

theories/typing/type.v

@@ -341,7 +341,6 @@ Section subtyping.
   Lemma type_incl_trans ty1 ty2 ty3 :
     type_incl ty1 ty2 -∗ type_incl ty2 ty3 -∗ type_incl ty1 ty3.
   Proof.
-    (* TODO: this iIntros takes suspiciously long. *)
     iIntros "(% & #Ho12 & #Hs12) (% & #Ho23 & #Hs23)".
     iSplit; first (iPureIntro; etrans; done).
     iSplit; iAlways; iIntros.
@@ -462,12 +461,11 @@ Section weakening.
     E1 ⊆+ E2 → L1 ⊆+ L2 →
     subtype E1 L1 ty1 ty2 → subtype E2 L2 ty1 ty2.
   Proof.
-    (* TODO: There's no lemma relating `contains` to membership (∈)...?? *)
-    iIntros (HE12 [L' HL12]%submseteq_Permutation Hsub) "#LFT HE HL".
+    iIntros (HE12 ? Hsub) "#LFT HE HL".
     iApply (Hsub with "LFT [HE] [HL]").
     - rewrite /elctx_interp_0. by iApply big_sepL_submseteq.
     - iDestruct "HL" as %HL. iPureIntro. intros ??. apply HL.
-      rewrite HL12. set_solver.
+      eauto using elem_of_submseteq.
   Qed.
 End weakening.
 

theories/typing/unsafe/refcell/ref.v

@@ -28,7 +28,7 @@ Section ref.
              ▷ (α ⊑ β) ∗ ▷ &na{β, tid, refcell_invN}(refcell_inv tid lrc γ β ty') ∗
              &na{κ, tid, refcell_refN}(own γ (◯ reading_st q ν)) |}%I.
   Next Obligation.
-    iIntros (???[|[[]|][|[[]|][]]]); try iIntros "[]". by iIntros "_".
+    iIntros (???[|[[]|][|[[]|][]]]); try iIntros "[]"; auto.
   Qed.
   Next Obligation.
     iIntros (α ty E κ l tid q ?) "#LFT Hb Htok".
@@ -49,9 +49,7 @@ Section ref.
     iMod (bor_sep with "LFT Hb") as "[Hinv Hb]". done.
     iMod (bor_persistent_tok with "LFT Hinv Htok") as "[#Hinv $]". done.
     iMod (bor_sep with "LFT Hb") as "[Hκν Hb]". done.
-    (* FIXME : I cannot write #Hκν directly. *)
-    iDestruct (frac_bor_lft_incl with "LFT >[Hκν]") as "Hκν";
-      last iDestruct "Hκν" as "#Hκν".
+    iDestruct (frac_bor_lft_incl with "LFT >[Hκν]") as "#Hκν".
     { iApply bor_fracture; try done. by rewrite Qp_mult_1_r. }
     iMod (bor_na with "Hb") as "#Hb". done. eauto 20.
   Qed.