diff --git a/coq-reloc.opam b/coq-reloc.opam
index 6cb19182a9edf03d19006a4ec7059f7ad9125210..3f22923fd75dd53a724caf17aea7bf8acfbd552a 100644
--- a/coq-reloc.opam
+++ b/coq-reloc.opam
@@ -6,7 +6,7 @@ bug-reports: "https://gitlab.mpi-sws.org/dfrumin/reloc/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/dfrumin/reloc.git"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2023-05-03.3.85295b18") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2023-06-02.4.80f55f7c") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
 
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index 1ee22f31ddd96ae7c451222390e4407741e42a22..69cabd270f4e88e5dfe391742f69dc072231e4bf 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -32,17 +32,17 @@ Section definitionsS.
 
   Definition heapS_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
     own cfg_name (◯ (∅, {[ l := (q, to_agree (Some v)) ]})).
-  Definition heapS_mapsto_aux : { x | x = @heapS_mapsto_def }. by eexists. Qed.
-  Definition heapS_mapsto := proj1_sig heapS_mapsto_aux.
+  Definition heapS_mapsto_aux : seal (@heapS_mapsto_def). by eexists. Qed.
+  Definition heapS_mapsto := heapS_mapsto_aux.(unseal).
   Definition heapS_mapsto_eq :
-    @heapS_mapsto = @heapS_mapsto_def := proj2_sig heapS_mapsto_aux.
+    @heapS_mapsto = @heapS_mapsto_def := heapS_mapsto_aux.(seal_eq).
 
   Definition tpool_mapsto_def (j : nat) (e: expr) : iProp Σ :=
     own cfg_name (◯ ({[ j := Excl e ]}, ∅)).
-  Definition tpool_mapsto_aux : { x | x = @tpool_mapsto_def }. by eexists. Qed.
-  Definition tpool_mapsto := proj1_sig tpool_mapsto_aux.
+  Definition tpool_mapsto_aux : seal (@tpool_mapsto_def). by eexists. Qed.
+  Definition tpool_mapsto := tpool_mapsto_aux.(unseal).
   Definition tpool_mapsto_eq :
-    @tpool_mapsto = @tpool_mapsto_def := proj2_sig tpool_mapsto_aux.
+    @tpool_mapsto = @tpool_mapsto_def := tpool_mapsto_aux.(seal_eq).
 
   Definition mkstate (σ : gmap loc (option val)) (κs : gset proph_id) :=
     {| heap := σ; used_proph_id := κs |}.
@@ -59,7 +59,6 @@ Section definitionsS.
   Global Instance spec_ctx_persistent : Persistent spec_ctx.
   Proof. apply _. Qed.
 End definitionsS.
-Global Typeclasses Opaque heapS_mapsto tpool_mapsto spec_ctx.
 
 Notation "l ↦ₛ{ q } v" := (heapS_mapsto l q v)
   (at level 20, q at level 50, format "l  ↦ₛ{ q }  v") : bi_scope.
@@ -160,9 +159,9 @@ Section mapsto.
   Global Instance mapstoS_as_fractional l q v :
     AsFractional (l ↦ₛ{q} v) (λ q, l ↦ₛ{q} v)%I q.
   Proof. split. done. apply _. Qed.
-  Global Instance frame_mapstoS 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.
+  Global Instance frame_mapstoS p l v q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p (l ↦ₛ{q1} v) (l ↦ₛ{q2} v) (l ↦ₛ{q} v) | 5.
   Proof. apply: frame_fractional. Qed.
 
   Lemma mapstoS_agree l q1 q2 v1 v2 : l ↦ₛ{q1} v1 -∗ l ↦ₛ{q2} v2 -∗ ⌜v1 = v2⌝.