diff --git a/coq-gpfsl.opam b/coq-gpfsl.opam
index d82c21a00721bc04968e7fc6bb7be730fdf0c6d8..1184346842f079d07698a43b48fb3a98d430ef01 100644
--- a/coq-gpfsl.opam
+++ b/coq-gpfsl.opam
@@ -10,8 +10,8 @@ version: "dev"
 synopsis: "A combination of GPS and FSL in the promising semantics WITHOUT promises"
 
 depends: [
-  "coq-iris"  { (= "dev.2022-07-27.1.d01b4bc8") | (= "dev") }
-  "coq-orc11" { (= "dev.2022-07-27.0.cadba960") | (= "dev") }
+  "coq-iris"  { (= "dev.2022-08-03.0.949ab7bc") | (= "dev") }
+  "coq-orc11" { (= "dev.2022-07-30.0.e76351a5") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/base_logic/adequacy.v b/theories/base_logic/adequacy.v
index 9619f3e0021b048a376ffc95e64e68b2c5b94a57..23e27bf6fe9f547ff14c5d8210d446589f35f96c 100644
--- a/theories/base_logic/adequacy.v
+++ b/theories/base_logic/adequacy.v
@@ -55,7 +55,7 @@ Lemma noprol_adequacy Σ `{!noprolGpreS Σ} e (σ : state) 𝓥 φ :
 Proof.
   (* TODO: we cannot use [ownP_adequacy] because it fixes a state_interp. We
     have to embed [ownP_adequacy]'s proof here instead. *)
-  intros WFσ H𝓥 Hwp; eapply (wp_adequacy_lc _ _); iIntros (Hinv ??).
+  intros WFσ H𝓥 Hwp; eapply (wp_adequacy _ _); iIntros (Hinv ?).
   set (M := mem_cut σ.(mem) σ.(na)).
   iMod (gen_heap_init (to_hist M)) as (HEAPG) "(Hist & hists & metas)".
   iMod (own_alloc (● (∅ : hist_freeableUR))) as (hist_freeable_name) "hf".
diff --git a/theories/base_logic/history.v b/theories/base_logic/history.v
index cc8bdec142eab5a7101a31b6b6bde1a519a2a4bd..03e79f0cafe710d67fbbe2f5bc9971130e21613a 100644
--- a/theories/base_logic/history.v
+++ b/theories/base_logic/history.v
@@ -170,7 +170,7 @@ Definition hist_inv_content `{!noprolG Σ} : iProp Σ :=
 Definition histN : namespace := nroot .@ "history".
 
 Definition hist_inv `{!noprolG Σ} : iProp Σ :=
-  @inv _ (ownP_invG) histN hist_inv_content.
+  @inv _ _ (ownP_invG) histN hist_inv_content.
 
 Definition hist_interp `{!noprolG Σ} σ : iProp Σ :=
   (own ownP_name (●E σ) ∗ hist_inv)%I.