Bump Iris.

opam.pins

-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 3d6525a57844edcc8868ec9271a0966bcc2a5e89
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 4a154f085ab5be64d30eec3967f1ab46b5467061

theories/lang/heap.v

@@ -139,13 +139,11 @@ Section heap.
   Global Instance heap_freeable_timeless q l n : TimelessP (†{q}l…n).
   Proof. rewrite heap_freeable_eq /heap_freeable_def. apply _. Qed.
 
-  Lemma heap_mapsto_agree l q1 q2 v1 v2 :
-    l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2⌝.
+  Lemma heap_mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2⌝.
   Proof.
     rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid uPred.discrete_valid.
     eapply pure_elim; [done|]=> /auth_own_valid /=.
-    rewrite op_singleton pair_op singleton_valid. case.
-    rewrite /= to_agree_comp_valid=>? Heq. fold_leibniz. eauto.
+    rewrite op_singleton pair_op singleton_valid=> -[? /agree_op_invL'->]; eauto.
   Qed.
 
   Lemma heap_mapsto_vec_nil l q : l ↦∗{q} [] ⊣⊢ True.

theories/lifetime/model/primitive.v

@@ -58,6 +58,7 @@ Proof.
   iIntros "HI"; iDestruct 1 as (γs) "[? _]".
   by iApply (own_ilft_auth_agree with "HI").
 Qed.
+
 Lemma own_bor_op κ x y : own_bor κ (x ⋅ y) ⊣⊢ own_bor κ x ∗ own_bor κ y.
 Proof.
   iSplit.
@@ -65,7 +66,7 @@ Proof.
   iIntros "[Hx Hy]".
   iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
   iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
-  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_inv /(inj to_agree) <-.
+  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_invL' <-.
   iExists γs. iSplit. done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_bor_into_op κ x x1 x2 :
@@ -99,7 +100,7 @@ Proof.
   iIntros "[Hx Hy]".
   iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
   iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
-  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_inv /(inj to_agree) <-.
+  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_invL'=> <-.
   iExists γs. iSplit; first done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_cnt_into_op κ x x1 x2 :
@@ -133,7 +134,7 @@ Proof.
   iIntros "[Hx Hy]".
   iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
   iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
-  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_inv /(inj to_agree) <-.
+  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_invL' <-.
   iExists γs. iSplit. done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_inh_into_op κ x x1 x2 :