Bump Iris and fix some minor things.

opam.pins

-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq a1bf05fe892801c43a9d61e8cb7cf7cb1f1eced3
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 1e241cca15302ae89d41f14251c2dafbd7efebb6

theories/typing/lib/rc.v

@@ -88,7 +88,7 @@ Section rc.
         iExists _, _, _. iFrame. done. }
       iDestruct "HX" as (γ ν q') "(#Hinv & Hrc & Htok & #Hshr)".
       iMod ("Hclose2" with "[] [Hrc Htok]") as "[HX Htok]".
-      { iNext. iIntros "HX". iModIntro. (* FIXME: iNext here doesn't strip of the next from in front of the evar. *)
+      { iNext. iIntros "HX". iModIntro. iNext.
         iRight. iExists γ, ν, q'. iExact "HX". }
       { iNext. by iFrame "#∗". }
       iAssert (|={F ∖ ↑shrN}=> C)%I with "[HX]" as ">#HC".

theories/typing/sum.v

@@ -205,11 +205,10 @@ Section sum.
       { rewrite <-HF. simpl. rewrite <-union_subseteq_r.
         apply shr_locsE_subseteq. omega. }
       iDestruct (na_own_acc with "Htl") as "[$ Htlclose]".
-      { (* Really, we don't even have a lemma for anti-monotonicity of difference...? *)
-        cut (shr_locsE (shift_loc l 1) (ty_size (nth i tyl ∅)) ⊆
-                  shr_locsE (shift_loc l 1) (list_max (map ty_size tyl))).
-        - simpl. set_solver+.
-        - apply shr_locsE_subseteq. omega. }
+      { apply difference_mono_l.
+        trans (shr_locsE (shift_loc l 1) (list_max (map ty_size tyl))).
+        - apply shr_locsE_subseteq. omega.
+        - set_solver+. }
       destruct (Qp_lower_bound q'1 q'2) as (q' & q'01 & q'02 & -> & ->).
       rewrite -(heap_mapsto_pred_op _ q' q'02); last (by intros; apply ty_size_eq).
       rewrite (fractional (Φ := λ q, _ ↦{q} _ ∗ _ ↦∗{q}: _)%I).