Bump Iris (beautify code for `iCombine .. gives`).

coq-iris-tutorial-popl21.opam

@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/tutorial-popl18.git"
 synopsis: "The Iris tutorial at POPL 2021"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2022-08-11.5.b6b4b694") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2023-03-09.0.f91e8eab") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]

solutions/ex_04_parallel_add.v

@@ -100,7 +100,7 @@ Section proof2.
     own γ (●E n) -∗ own γ (◯E m) -∗ ⌜ n = m ⌝.
   Proof.
     iIntros "Hγ● Hγ◯".
-    by iDestruct (own_valid_2 with "Hγ● Hγ◯") as %?%excl_auth_agree_L.
+    by iCombine "Hγ● Hγ◯" gives %?%excl_auth_agree_L.
   Qed.
 
   Lemma ghost_var_update γ n' n m :
@@ -203,7 +203,7 @@ Section proof3.
     - iIntros (??) "[Hγ1◯ Hγ2◯] !>". wp_seq.
       iInv "Hinv" as (n) "(Hr & Hγ●)" "Hclose".
       wp_load. iCombine "Hγ1◯ Hγ2◯" as "Hγ◯".
-      iDestruct (own_valid_2 with "Hγ● Hγ◯") as %->%frac_auth_agree_L.
+      iCombine "Hγ● Hγ◯" gives %->%frac_auth_agree_L.
       iMod ("Hclose" with "[Hr Hγ●]") as "_".
       { iExists _. iFrame. } 
       by iApply "Post".

solutions/ex_05_parallel_add_mul.v

@@ -45,7 +45,7 @@ Section proof.
     own γ (●E b) -∗ own γ (◯E c) -∗ ⌜ b = c ⌝.
   Proof.
     iIntros "Hγ● Hγ◯".
-    by iDestruct (own_valid_2 with "Hγ● Hγ◯") as %<-%excl_auth_agree_L.
+    by iCombine "Hγ● Hγ◯" gives %<-%excl_auth_agree_L.
   Qed.
 
   Lemma ghost_var_update γ b' b c :