diff --git a/coq-gpfsl.opam b/coq-gpfsl.opam
index ca37ce20cca2db6ec1b87278d7cf653379a8a44f..6558f991b34773aba23a6aae8dfea2133d6c0143 100644
--- a/coq-gpfsl.opam
+++ b/coq-gpfsl.opam
@@ -10,7 +10,7 @@ version: "dev"
 synopsis: "A combination of GPS and FSL in the promising semantics WITHOUT promises"
 
 depends: [
-  "coq-iris"  { (= "dev.2023-05-11.0.7d395a7e") | (= "dev") }
+  "coq-iris"  { (= "dev.2023-06-04.0.695533ab") | (= "dev") }
   "coq-orc11" {= version}
 ]
 
diff --git a/coq-orc11.opam b/coq-orc11.opam
index 241f4e363cf6657b1b3e2f05240afe0d4ab14ac7..bd3a67835cbe4ab3ea0a831f16c3788c87982e01 100644
--- a/coq-orc11.opam
+++ b/coq-orc11.opam
@@ -10,7 +10,7 @@ version: "dev"
 synopsis: "A Coq formalization of the ORC11 semantics for weak memory"
 
 depends: [
-  "coq-stdpp" { (= "dev.2023-05-10.0.f34a9e18") | (= "dev") }
+  "coq-stdpp" { (= "dev.2023-06-01.0.d1254759") | (= "dev") }
 ]
 
 build: ["./make-package" "orc11" "-j%{jobs}%"]
diff --git a/gpfsl-examples/queue/proof_ms_abs_graph.v b/gpfsl-examples/queue/proof_ms_abs_graph.v
index 4e576642534c6d5d52dd0c56dbd59859cfe380a2..659b6a828688a08618fe1f9949cad578149beda0 100644
--- a/gpfsl-examples/queue/proof_ms_abs_graph.v
+++ b/gpfsl-examples/queue/proof_ms_abs_graph.v
@@ -658,7 +658,7 @@ Definition QueueInv_no_exist γg q Q G γ γh γl η0 s0 D L T : vProp :=
 
 #[global] Instance own_nodes_timeless E T η s D L :
   Timeless (own_nodes E T η s D L).
-Proof. apply big_sepL2_timeless => _ [??] [??]. apply _. Qed.
+Proof. apply big_sepL2_timeless => ? [??] [??]. apply _. Qed.
 #[global] Instance QueueInv_no_exist_timeless γg q Q G γ γh γl η0 s0 D L T :
   Timeless (QueueInv_no_exist γg q Q G γ γh γl η0 s0 D L T) := _.
 
diff --git a/gpfsl-examples/stack/proof_treiber_at.v b/gpfsl-examples/stack/proof_treiber_at.v
index 4dbf3a7677b6975fe2ed67dd8e5bb5425785640e..3090bebc4584bb3a4ca75626a68cc7c6d43d86df 100644
--- a/gpfsl-examples/stack/proof_treiber_at.v
+++ b/gpfsl-examples/stack/proof_treiber_at.v
@@ -119,7 +119,7 @@ Definition all_slocs (LVs : list (option loc * view)) : vProp :=
 #[global] Instance all_slocs_objective LVs : Objective (all_slocs LVs).
 Proof. apply big_sepL_objective => _ [[n|] V]; apply _. Qed.
 #[global] Instance all_slocs_timeless LVs : Timeless (all_slocs LVs).
-Proof. apply big_sepL_timeless => _ [[n|] V]; apply _. Qed.
+Proof. apply big_sepL_timeless => ? [[n|] V]; apply _. Qed.
 
 Definition Head_inv_no_exists s γ t0 Vb Vh LVs S : vProp :=
   let vh := (hd_error S) in
diff --git a/gpfsl-examples/stack/proof_treiber_graph.v b/gpfsl-examples/stack/proof_treiber_graph.v
index e1043f1b158a6466850530e2c26c815588712f74..e214c7024401a65c75f72c30bd2683e45309fbcb 100644
--- a/gpfsl-examples/stack/proof_treiber_graph.v
+++ b/gpfsl-examples/stack/proof_treiber_graph.v
@@ -282,7 +282,7 @@ Definition all_slocs (LVs : list (option loc * view)) : vProp :=
 #[global] Instance all_slocs_objective LVs : Objective (all_slocs LVs).
 Proof. apply big_sepL_objective => _ [[n|] V]; apply _. Qed.
 #[global] Instance all_slocs_timeless LVs : Timeless (all_slocs LVs).
-Proof. apply big_sepL_timeless => _ [[n|] V]; apply _. Qed.
+Proof. apply big_sepL_timeless => ? [[n|] V]; apply _. Qed.
 
 (* Locs of the Stack: Head, popped nodes, and nodes *)
 Definition StackLocs_no_exist s (E : event_list) γh T S t0 LVs Vh : vProp :=
diff --git a/gpfsl-examples/stack/proof_treiber_history.v b/gpfsl-examples/stack/proof_treiber_history.v
index 351552c88d79086b056f33dcc9dfd2325beeb743..6b93d6413e48e4f3bea0c2219fdab7dc8d1f815c 100644
--- a/gpfsl-examples/stack/proof_treiber_history.v
+++ b/gpfsl-examples/stack/proof_treiber_history.v
@@ -1083,7 +1083,7 @@ Definition AllLinks mo : vProp :=
 Proof. apply big_sepL_objective => _ [[n|] V]; apply _. Qed.
 
 #[global] Instance AllLinks_timeless mo : Timeless (AllLinks mo).
-Proof. apply big_sepL_timeless => _ [[n|] V]; apply _. Qed.
+Proof. apply big_sepL_timeless => ? [[n|] V]; apply _. Qed.
 
 Definition toHeadHist (start : time) mo : absHist :=
   map_seqP start ((λ olv, (#(oloc_to_lit olv.1), olv.2)) <$> mo).
diff --git a/gpfsl/base_logic/history.v b/gpfsl/base_logic/history.v
index b665547bf2dedf54f08a07eb9d9d1a0b04f74a67..fe0238729f919772e1b9a14c304ce40841fc9767 100644
--- a/gpfsl/base_logic/history.v
+++ b/gpfsl/base_logic/history.v
@@ -323,10 +323,10 @@ Section hist.
   Global Instance hist_as_fractional l q C:
     AsFractional (hist l q C) (λ q, hist l q C)%I q.
   Proof. split; [done|apply _]. Qed.
-  Global Instance frame_hist p l C q1 q2 RES :
-    FrameFractionalHyps p (hist l q1 C) (λ q, hist l q C)%I RES q1 q2 →
-    Frame p (hist l q1 C) (hist l q2 C) RES | 5.
-  Proof. apply: frame_fractional. Qed.
+  Global Instance frame_hist p l C q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p (hist l q1 C) (hist l q2 C) (hist l q C) | 5.
+  Proof. apply: (frame_fractional (λ q, hist l q C)). Qed.
 
   Lemma hist_agree l p1 p2 C1 C2:
     hist l p1 C1 ∗ hist l p2 C2 ⊢ ⌜C1 = C2⌝.
@@ -395,9 +395,9 @@ Section hist.
   Global Instance naread_as_fractional l q rs:
     AsFractional (naread l q rs) (λ q, naread l q rs)%I q.
   Proof. split; [done|apply _]. Qed.
-  Global Instance frame_naread p l rs q1 q2 RES :
-    FrameFractionalHyps p (naread l q1 rs) (λ q, naread l q rs)%I RES q1 q2 →
-    Frame p (naread l q1 rs) (naread l q2 rs) RES | 5.
+  Global Instance frame_naread p l rs q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p (naread l q1 rs) (naread l q2 rs) (naread l q rs) | 5.
   Proof. apply: frame_fractional. Qed.
 
   Lemma naread_combine l q1 q2 rs1 rs2:
@@ -455,9 +455,9 @@ Section hist.
   Global Instance atread_as_fractional l q rs:
     AsFractional (atread l q rs) (λ q, atread l q rs)%I q.
   Proof. split; [done|apply _]. Qed.
-  Global Instance frame_atread p l rs q1 q2 RES :
-    FrameFractionalHyps p (atread l q1 rs) (λ q, atread l q rs)%I RES q1 q2 →
-    Frame p (atread l q1 rs) (atread l q2 rs) RES | 5.
+  Global Instance frame_atread p l rs q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p (atread l q1 rs) (atread l q2 rs) (atread l q rs) | 5.
   Proof. apply: frame_fractional. Qed.
 
   Lemma atread_combine l q1 q2 rs1 rs2:
@@ -516,9 +516,9 @@ Section hist.
   Global Instance atwrite_as_fractional l q rs:
     AsFractional (atwrite l q rs) (λ q, atwrite l q rs)%I q.
   Proof. split; [done|apply _]. Qed.
-  Global Instance frame_atwrite p l rs q1 q2 RES :
-    FrameFractionalHyps p (atwrite l q1 rs) (λ q, atwrite l q rs)%I RES q1 q2 →
-    Frame p (atwrite l q1 rs) (atwrite l q2 rs) RES | 5.
+  Global Instance frame_atwrite p l rs q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p (atwrite l q1 rs) (atwrite l q2 rs) (atwrite l q rs) | 5.
   Proof. apply: frame_fractional. Qed.
 
   Lemma atwrite_agree l q1 q2 rs1 rs2:
diff --git a/gpfsl/base_logic/na.v b/gpfsl/base_logic/na.v
index 405f79fd0595d3463c9c4d95d6684de3d129575d..74c7ab9d0ddafc3c28989fba2bab376bb19399b7 100644
--- a/gpfsl/base_logic/na.v
+++ b/gpfsl/base_logic/na.v
@@ -122,9 +122,9 @@ Section na_props.
     AsFractional (l p↦{q} C) (λ q, l p↦{q} C)%I q.
   Proof. split; [done|apply _]. Qed.
 
-  Global Instance frame_own_loc_prim p l v q1 q2 RES :
-    FrameFractionalHyps p (l p↦{q1} v) (λ q, l p↦{q} v)%I RES q1 q2 →
-    Frame p (l p↦{q1} v) (l p↦{q2} v) RES | 5.
+  Global Instance frame_own_loc_prim p l v q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p (l p↦{q1} v) (l p↦{q2} v) (l p↦{q} v) | 5.
   Proof. apply: frame_fractional. Qed.
 
   Global Instance own_loc_prim_timeless l q C : Timeless (l p↦{q} C) := _.
@@ -168,9 +168,9 @@ Section na_props.
   Global Instance own_loc_na_asfractional l q v :
     AsFractional (l ↦{q} v) (λ q, (l ↦{q} v)%I) q.
   Proof. split; [done|apply _]. Qed.
-  Global Instance frame_own_loc_na 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_own_loc_na 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.
 
   Global Instance own_loc_na_timeless l q v: Timeless (l ↦{q} v).
@@ -285,10 +285,10 @@ Section na_props.
   Global Instance own_loc_vec_as_fractional l q n :
     AsFractional (own_loc_vec l q n) (λ q, own_loc_vec l q n)%I q.
   Proof. split; [done|apply _]. Qed.
-  Global Instance frame_own_loc_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_own_loc_vec 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 (λ q, l ↦∗{q} v)%I). Qed.
 
   Lemma own_loc_na_vec_nil l q : l ↦∗{q} [] ⊣⊢ True.
   Proof. rewrite /own_loc_na_vec bi.True_emp //. Qed.
diff --git a/gpfsl/gps/middleware_SW.v b/gpfsl/gps/middleware_SW.v
index 2ee1efa904d1ccf84cefe3c04e8fd0eaff519c9a..974de830a338d62998bfb90245d035aeb268e8f0 100644
--- a/gpfsl/gps/middleware_SW.v
+++ b/gpfsl/gps/middleware_SW.v
@@ -106,10 +106,10 @@ Section SingleWriter.
     AsFractional (GPS_SWSharedReader t s v q γ)
                  (λ q, GPS_SWSharedReader t s v q γ) q.
   Proof. split; [done|apply _]. Qed.
-  Global Instance frame_GPS_SWSharedReader p t s v γ q1 q2 RES :
-    FrameFractionalHyps p (GPS_SWSharedReader t s v q1 γ)
-                        (λ q, GPS_SWSharedReader t s v q γ) RES q1 q2 →
-    Frame p (GPS_SWSharedReader t s v q1 γ) (GPS_SWSharedReader t s v q2 γ) RES | 5.
+  Global Instance frame_GPS_SWSharedReader p t s v γ q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p (GPS_SWSharedReader t s v q1 γ) (GPS_SWSharedReader t s v q2 γ)
+            (GPS_SWSharedReader t s v q γ) | 5.
 Proof. apply: frame_fractional. Qed.
 
   (** Properties of Assertions *)
diff --git a/gpfsl/logic/view_invariants.v b/gpfsl/logic/view_invariants.v
index 21b8cbcbe583cdc1e2020ea64b826efe7ba9ba92..83a08929f36a9665b16d879ec7b19498935322d0 100644
--- a/gpfsl/logic/view_invariants.v
+++ b/gpfsl/logic/view_invariants.v
@@ -74,9 +74,9 @@ Qed.
   AsFractional (view_tok γ q) (view_tok γ) q.
 Proof. split; [done|apply _]. Qed.
 
-#[global] Instance frame_view_tok p γ q1 q2 RES :
-  FrameFractionalHyps p (view_tok γ q1) (view_tok γ) RES q1 q2 →
-  Frame p (view_tok γ q1) (view_tok γ q2) RES | 5.
+#[global] Instance frame_view_tok p γ q1 q2 q :
+  FrameFractionalQp q1 q2 q →
+  Frame p (view_tok γ q1) (view_tok γ q2) (view_tok γ q) | 5.
 Proof. apply: frame_fractional. Qed.
 
 Lemma view_tok_valid γ q : view_tok γ q -∗ ⌜ ✓ q ⌝.