From f899efbd7c49ed4ead30ac67b1595602f0b091ec Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 14 Jun 2023 22:24:25 +0200
Subject: [PATCH] update dependencies

---
 coq-iris-examples.opam                |  2 +-
 theories/hocap/concurrent_runners.v   | 12 +++---------
 theories/hocap/lib/oneshot.v          |  2 +-
 theories/lecture_notes/modular_incr.v |  3 +--
 4 files changed, 6 insertions(+), 13 deletions(-)

diff --git a/coq-iris-examples.opam b/coq-iris-examples.opam
index a0d35970..bd826f2d 100644
--- a/coq-iris-examples.opam
+++ b/coq-iris-examples.opam
@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/examples.git"
 synopsis: "A collection of case studies for Iris -- not meant to be used as a dependency of anything"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2023-06-02.4.80f55f7c") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2023-06-14.0.f0e415b6") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
 
diff --git a/theories/hocap/concurrent_runners.v b/theories/hocap/concurrent_runners.v
index 62d5f2f8..0b9142ef 100644
--- a/theories/hocap/concurrent_runners.v
+++ b/theories/hocap/concurrent_runners.v
@@ -262,9 +262,7 @@ Section contents.
       iDestruct "HQ" as "[[HQ Htoken2]|Hshot]"; last first.
       { iExFalso. iApply (shot_not_pending with "Hshot Htoken"). }
       iMod (shoot v γ with "[Htoken Htoken2]") as "#Hshot".
-      { iApply (fractional_split_2 with "Htoken Htoken2").
-        assert ((1 / 2 + 1 / 2)%Qp = 1%Qp) as -> by apply Qp.div_2.
-        apply _. }
+      { iCombine "Htoken Htoken2" as "?". done. }
       iMod ("Hcl" with "[Hstate Hres]") as "_".
       { iNext. iRight. iRight. iExists _. iFrame. iFrame "HFIN".
         iRight. eauto. }
@@ -305,9 +303,7 @@ Section contents.
     iInv (N.@"task") as "[>(Hstate & Hres & Hpending & HINIT')|[Hstatus|Hstatus]]" "Hcl".
     - wp_store.
       iMod (INIT_SET_RES v γ' with "[HINIT HINIT']") as "[HSETRES HSETRES']".
-      { iApply (fractional_split_2 with "HINIT HINIT'").
-        assert ((1 / 2 + 1 / 2)%Qp = 1%Qp) as -> by apply Qp.div_2.
-        apply _. }
+      { iSplitL "HINIT"; done. }
       iMod ("Hcl" with "[HSETRES Hstate Hres Hpending]") as "_".
       { iNext. iRight. iLeft. iExists _; iFrame. }
       iModIntro. wp_seq.
@@ -317,9 +313,7 @@ Section contents.
         wp_store.
         iDestruct (SET_RES_agree with "HSETRES HSETRES'") as %->.
         iMod (SET_RES_FIN v v with "[HSETRES HSETRES']") as "#HFIN".
-        { iApply (fractional_split_2 with "HSETRES HSETRES'").
-          assert ((1 / 2 + 1 / 2)%Qp = 1%Qp) as -> by apply Qp.div_2.
-          apply _. }
+        { iSplitL "HSETRES"; done. }
         iMod ("Hcl" with "[-HΦ]") as "_".
         { iNext. do 2 iRight. iExists _; iFrame. iFrame "HFIN". iLeft. iFrame.  }
         iModIntro. by iApply "HΦ".
diff --git a/theories/hocap/lib/oneshot.v b/theories/hocap/lib/oneshot.v
index 3cc02aea..1f2b7f61 100644
--- a/theories/hocap/lib/oneshot.v
+++ b/theories/hocap/lib/oneshot.v
@@ -34,7 +34,7 @@ Proof.
   iCombine "Hs1 Hs2" gives %Hfoo.
   iPureIntro. by apply to_agree_op_inv_L.
 Qed.
-Global Instance pending_fractional `{oneshotG Σ} γ : Fractional (pending γ)%I.
+Global Instance pending_fractional `{oneshotG Σ} γ : Fractional (pending γ).
 Proof.
   intros p q. rewrite /pending.
   rewrite -own_op. by f_equiv.
diff --git a/theories/lecture_notes/modular_incr.v b/theories/lecture_notes/modular_incr.v
index 1f608317..999aa895 100644
--- a/theories/lecture_notes/modular_incr.v
+++ b/theories/lecture_notes/modular_incr.v
@@ -85,8 +85,7 @@ Section cnt_model.
   Proof.
     iIntros "H1 H2".
     iDestruct (makeElem_eq with "H1 H2") as %->.
-    iCombine "H1" "H2" as "H".
-    by rewrite makeElem_op.
+    iCombine "H1" "H2" as "H". done.
   Qed.
 
   Lemma makeElem_update γ (n m k : Z):
-- 
GitLab