From b3985249a180368f902cf149f56e73b04765a5c4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 11 Aug 2022 11:26:35 +0200
Subject: [PATCH] Bump Iris.

---
 coq-lambda-rust.opam                              | 2 +-
 theories/typing/function.v                        | 2 +-
 theories/typing/lib/rc/rc.v                       | 4 ++--
 theories/typing/lib/refcell/ref_code.v            | 2 +-
 theories/typing/lib/refcell/refmut_code.v         | 2 +-
 theories/typing/lib/rwlock/rwlockreadguard_code.v | 2 +-
 6 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index db0fc708..d8d0d4ed 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2022-08-03.0.949ab7bc") | (= "dev") }
+  "coq-iris" { (= "dev.2022-08-11.1.c9223a52") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 4111d6e4..7de88219 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -95,7 +95,7 @@ Section fn.
       { intros Hprop. apply Hprop, list_fmap_ne; last first.
         - symmetry. eapply Forall2_impl; first apply Hfp. intros.
           apply dist_later_dist, type_dist2_dist_later. done.
-        - apply _. }
+        - solve_proper. }
       clear. intros n tid p i x y. rewrite list_dist_lookup=>/(_ i).
       case _ : (x !! i)=>[tyx|]; case  _ : (y !! i)=>[tyy|];
         inversion_clear 1; [solve_proper|done].
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index a597e9b3..b9049edc 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -368,7 +368,7 @@ Section code.
                                (?&?&[=]&?)]]; first done. setoid_subst.
         iDestruct "Hproto" as (q'') "(Hl1 & Hl2 & Hl† & >Hqq' & Hν & Hν†)".
         iDestruct "Hqq'" as %Hqq'. wp_read. iApply "HΦ". iFrame "Hl1". iRight.
-        iSplit; first by rewrite !pos_op_plus; auto with lia. iSplit; iIntros "H↦".
+        iSplit; first by rewrite !pos_op_add; auto with lia. iSplit; iIntros "H↦".
         * iMod ("Hclose" with "[- Htok Hν1]") as "$"; last by auto 10 with iFrame.
           iFrame. iExists _. iFrame. auto with iFrame.
         * iMod (own_update_2 with "Hst Htok") as "Hst".
@@ -378,7 +378,7 @@ Section code.
           iApply "Hclose". iFrame. iExists _. iFrame. iExists (q+q'')%Qp. iFrame.
           iSplitL; first last.
           { rewrite [(_+_)%Qp]assoc [(q'+_)%Qp]comm. auto. }
-          rewrite pos_op_plus Z.sub_1_r -Pos2Z.inj_pred; last lia.
+          rewrite pos_op_add Z.sub_1_r -Pos2Z.inj_pred; last lia.
           by rewrite Pos.add_1_l Pos.pred_succ.
   Qed.
 
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 88fa78bc..3c1162b3 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -173,7 +173,7 @@ Section ref_functions.
         iApply "H†". replace 1%Qp with (q'+q'')%Qp by naive_solver. iFrame.
       - simpl in *. setoid_subst. iExists (Some (ν, false, q0, n')). iFrame.
         iAssert (lrc ↦ #(Z.pos n'))%I with "[H↦lrc]" as "$".
-        { rewrite pos_op_plus Z.sub_1_r -Pos2Z.inj_pred; last lia.
+        { rewrite pos_op_add Z.sub_1_r -Pos2Z.inj_pred; last lia.
           by rewrite Pos.add_1_l Pos.pred_succ. }
         iMod (own_update with "H●◯") as "$".
         { apply auth_update_dealloc.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index c295c787..5fd3f1e5 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -148,7 +148,7 @@ Section refmut_functions.
           apply (cancel_local_update_unit (writing_stR q _)), _. }
         iDestruct "INV" as "(H† & Hq & _)".
         rewrite /= (_:Z.neg (1%positive â‹… n') + 1 = Z.neg n');
-          last (rewrite pos_op_plus; lia). iFrame.
+          last (rewrite pos_op_add; lia). iFrame.
         iApply step_fupd_intro; [set_solver+|]. iSplitL; [|done].
         iDestruct "Hq" as (q' ?) "?". iExists (q+q')%Qp. iFrame.
         rewrite assoc (comm _ q'' q) //. }
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 279656a0..5659b7a6 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -117,7 +117,7 @@ Section rwlockreadguard_functions.
           iSplitL "H● H◯"; last by eauto with iFrame.
           iApply (own_update_2 with "H● H◯"). apply auth_update_dealloc.
           assert (n = 1%positive â‹… Pos.pred n) as EQn.
-          { rewrite pos_op_plus -Pplus_one_succ_l Pos.succ_pred // =>?. by subst. }
+          { rewrite pos_op_add -Pplus_one_succ_l Pos.succ_pred // =>?. by subst. }
           rewrite {1}EQn -{1}(agree_idemp (to_agree _)) 2!pair_op Cinr_op Some_op.
           apply (cancel_local_update_unit (reading_st q ν)) , _. }
       iApply (wp_step_fupd with "INV"); first set_solver.
-- 
GitLab