Bump Iris, fix some stuff.

opam.pins

-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 0429c257e3088cf77c8852a2cbeff2b02671b8b5
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq f987ca782d1301d319cf6c4ba8e2ab449ebe903a

theories/lang/lib/lock.v

@@ -61,12 +61,8 @@ Section proof.
     wp_seq. wp_alloc l vl as "Hl" "H†". inv_vec vl=>x.
     rewrite heap_mapsto_vec_singleton. (* FIXME shouldn't this also compute now, like bigops do? *)
     wp_let. wp_write.
-    iMod (newlock_inplace with "[HR] Hl") as (γ) "?".
-    { (* FIXME: Can we make it so that we can just say "HR" instead of "[HR]", and the
-         later does not matter? Or at least, "$HR" should work.  Why can't we frame
-         below later? *)
-      done. }
-    iApply "HΦ". done.
+    iMod (newlock_inplace with "HR Hl") as (γ) "?".
+    by iApply "HΦ".
   Qed.
 
   Lemma try_acquire_spec γ l R :

theories/lifetime/lifetime.v

@@ -51,7 +51,8 @@ Lemma bor_or E κ P Q :
   lft_ctx -∗ &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q).
 Proof.
   iIntros (?) "#LFT H". rewrite uPred.or_alt.
-  iMod (bor_exists with "LFT H") as ([]) "H"; auto.
+  (* The (A:=...) is needed due to Coq bug #5458 *)
+  iMod (bor_exists (A:=bool) with "LFT H") as ([]) "H"; auto.
 Qed.
 
 Lemma bor_later E κ P :