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

coq-tutorial-popl20.opam

@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/tutorial-popl20.git"
 synopsis: "The Iris tutorial at POPL 2020"
 
 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/symbol_ghost.v

@@ -56,7 +56,7 @@ Section symbol_ghost.
   Lemma symbol_obs γ s n : counter γ n -∗ symbol γ s -∗ ⌜(s < n)%nat⌝.
   Proof.
     iIntros "Hc Hs".
-    iDestruct (own_valid_2 with "Hc Hs") as %[?%max_nat_included _]%auth_both_valid_discrete.
+    iCombine "Hc Hs" gives %[?%max_nat_included _]%auth_both_valid_discrete.
     iPureIntro. simpl in *. lia.
   Qed.
 End symbol_ghost.

solutions/two_state_ghost.v

@@ -54,7 +54,7 @@ Section two_state_ghost.
     two_state_auth γ b -∗ two_state_final γ -∗ ⌜b = true⌝.
   Proof.
     iIntros "H1 H2".
-    iDestruct (own_valid_2 with "H1 H2") as %[Hinc _]%auth_both_valid_discrete.
+    iCombine "H1 H2" gives %[Hinc _]%auth_both_valid_discrete.
     apply option_included in Hinc as [|([]&[]&_&?&_)];
       destruct b; naive_solver.
   Qed.