Bump Iris and fix several TODOs and FIXMEs.

opam.pins

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

theories/lang/lifting.v

@@ -51,8 +51,7 @@ Proof.
   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
   iMod (heap_alloc with "Hσ") as "[Hσ Hl]"; [done..|].
   iModIntro; iSplit=> //. iFrame.
-  (* FIXME: Merging these two into one "iApply" doesn't work. *)
-  iSpecialize ("HΦ" $! _ (length init)). iApply ("HΦ" $! (list_to_vec init)).
+  iApply ("HΦ" $! _ _ (list_to_vec init)).
   rewrite vec_to_list_of_list. auto.
 Qed.
 

theories/lifetime/model/raw_reborrow.v

@@ -40,8 +40,7 @@ Proof.
   iMod (slice_empty with "Hislice Hbox") as "[HP Hbox]"; first done.
   { by rewrite lookup_fmap HB. }
   iMod (own_bor_update_2 with "HB● Hi") as "[HB● Hi]".
-  { eapply auth_update. (* FIXME: eapply singleton_local_update loops. *)
-    apply: singleton_local_update; last eapply
+  { eapply auth_update, singleton_local_update; last eapply
      (exclusive_local_update _ (1%Qp, to_agree (Bor_rebor κ'))); last done.
     rewrite /to_borUR lookup_fmap. by rewrite HB. }
   iAssert (▷?q lft_inv A κ)%I with "[H◯ HB● HB Hvs' Hinh' Hbox]" as "Hκ".

theories/typing/own.v

@@ -155,8 +155,7 @@ Section own.
     iIntros (Hsync κ tid1 tid2 l) "H". iDestruct "H" as (l') "[Hm #Hshr]".
     iExists _. iFrame "Hm". iAlways. iIntros (F q) "% Htok".
     iMod ("Hshr" with "[] Htok") as "Hfin"; first done. iModIntro. iNext.
-    iClear "Hshr". (* FIXME: Using "{HShr} [HShr $]" for the intro pattern in the following line doesn't work. *)
-    iMod "Hfin" as "[Hshr $]". by iApply Hsync.
+    iMod "Hfin" as "{Hshr} [Hshr $]". by iApply Hsync.
   Qed.
 End own.
 
@@ -225,9 +224,7 @@ Section typing.
     typed_body E L C T (let: x := new [ #n ] in e).
   Proof.
     intros ???? Htyp. eapply type_let. done. by apply type_new_instr. solve_typing.
-    iIntros (v). iApply typed_body_mono; [done| |done|].
-    (* FIXME : why can't we iApply Htyp? *)
-    2:by iDestruct (Htyp v) as "$".
+    iIntros (v). iApply typed_body_mono; [done| |done|by iApply (Htyp v)].
     by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl, own_mono.
   Qed.
 

theories/typing/programs.v

@@ -262,9 +262,8 @@ Section typing_rules.
   Proof.
     iIntros (Hsz Hwrt Hread) "!#". iIntros (tid qE) "#LFT Htl HE HL HT".
     iApply (type_memcpy_iris with "[] [] [$LFT $Htl $HE $HL HT]"); try done.
-    (* TODO: This is kind of silly, why can't I iApply the assumptions directly? *)
-    { iPoseProof Hwrt as "Hwrt". done. }
-    { iPoseProof Hread as "Hread". done. }
+    { iApply Hwrt. }
+    { iApply Hread. }
     { by rewrite tctx_interp_cons tctx_interp_singleton. }
     rewrite tctx_interp_cons tctx_interp_singleton. auto.
   Qed.

theories/typing/type_context.v

@@ -155,11 +155,7 @@ Section type_context.
 
   Global Instance tctx_ty_copy T p ty :
     CopyC T → Copy ty → CopyC ((p ◁ ty) :: T).
-  Proof.
-    (* TODO RJ: Should we have instances that PersistentP respects equiv? *)
-    intros ???. rewrite /PersistentP tctx_interp_cons.
-    apply uPred.sep_persistent; by apply _.
-  Qed.
+  Proof. intros ???. rewrite tctx_interp_cons. apply _. Qed.
 
   (** Send typing contexts *)
   Class SendC (T : tctx) :=

theories/typing/unsafe/spawn.v

@@ -23,14 +23,8 @@ Section join_handle.
          end%I;
        ty_shr κ tid l := True%I |}.
   Next Obligation. by iIntros (ty tid [|[[]|][]]) "H"; try iDestruct "H" as "[]". Qed.
-  Next Obligation.
-    (* FIXME: Replacing the % by a _ below fails. *)
-    iIntros "* % _ _ $". auto.
-  Qed.
-  Next Obligation.
-    (* FIXME: for some reason, `iIntros "*" does not do anything here. *)
-    iIntros (?) "* _ _ _". auto.
-  Qed.
+  Next Obligation. iIntros "* _ _ _ $". auto. Qed.
+  Next Obligation. iIntros (?) "**"; auto. Qed.
 
   Lemma join_handle_subtype ty1 ty2 :
     type_incl ty1 ty2 -∗ type_incl (join_handle ty1) (join_handle ty2).