From c0dff161658785c44bd35d4ab2e226efddfb1c33 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 3 Jun 2023 11:52:33 +0200
Subject: [PATCH] update dependencies

---
 coq-simuliris.opam               |  2 +-
 theories/simulang/logical_heap.v | 18 ++++++++++--------
 2 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/coq-simuliris.opam b/coq-simuliris.opam
index 21099f4c..d56248ff 100644
--- a/coq-simuliris.opam
+++ b/coq-simuliris.opam
@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/simuliris.git"
 synopsis: "Local Simulation proofs, the Iris style"
 
 depends: [
-  "coq-iris" { (= "dev.2023-05-05.0.670f2330") | (= "dev") }
+  "coq-iris" { (= "dev.2023-06-02.4.80f55f7c") | (= "dev") }
   "coq-equations" { (= "1.3+8.17") }
 ]
 
diff --git a/theories/simulang/logical_heap.v b/theories/simulang/logical_heap.v
index f2f3d5e3..4d5f76b8 100644
--- a/theories/simulang/logical_heap.v
+++ b/theories/simulang/logical_heap.v
@@ -226,10 +226,11 @@ Section heap.
   Global Instance heap_mapsto_as_fractional l q v:
     AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
   Proof. split; first done. apply _. Qed.
-  Global Instance frame_heap_mapsto p l v q1 q2 RES :
-    FrameFractionalHyps p (l ↦{q1} v) (λ q, l ↦{q} v)%I RES q1 q2 →
-    Frame p (l ↦{q1} v) (l ↦{q2} v) RES | 5.
-  Proof. apply: frame_fractional. Qed.
+  Global Instance frame_heap_mapsto p l v q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p (l ↦{q1} v) (l ↦{q2} v) (l ↦{q} v) | 5.
+  (* FIXME: somehow Φ gets inferred wrong here. *)
+  Proof. apply: (frame_fractional _ _ _ (λ q, l ↦{q} v)%I). Qed.
 
   Global Instance heap_mapsto_vec_timeless l st q vl : Timeless (l ↦∗[st]{q} vl).
   Proof. rewrite /heap_mapsto_vec. apply _. Qed.
@@ -242,10 +243,11 @@ Section heap.
   Global Instance heap_mapsto_vec_as_fractional l q vl:
     AsFractional (l ↦∗{q} vl) (λ q, l ↦∗{q} vl)%I q.
   Proof. split; first done. apply _. Qed.
-  Global Instance frame_heap_mapsto_vec p l v q1 q2 RES :
-    FrameFractionalHyps p (l ↦∗{q1} v) (λ q, l ↦∗{q} v)%I RES q1 q2 →
-    Frame p (l ↦∗{q1} v) (l ↦∗{q2} v) RES | 5.
-  Proof. apply: frame_fractional. Qed.
+  Global Instance frame_heap_mapsto_vec p l v q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p (l ↦∗{q1} v) (l ↦∗{q2} v) (l ↦∗{q} v)%I | 5.
+  (* FIXME: somehow Φ gets inferred wrong here. *)
+  Proof. apply: (frame_fractional _ _ _ (λ q, l ↦∗{q} v)%I). Qed.
 
   Global Instance heap_block_size_timeless q b n : Timeless (heap_block_size γ b q n).
   Proof. rewrite heap_block_size_eq /heap_block_size_def. apply _. Qed.
-- 
GitLab