update dependencies

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") }
 ]
 

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.