diff --git a/semantics.opam b/semantics.opam
index 627e21ea85a387ba3abc6201b90aee61e92e97e6..fe4d8e489b87cdaa5c090ccf7689bd4f89c10456 100644
--- a/semantics.opam
+++ b/semantics.opam
@@ -9,10 +9,10 @@ bug-reports: "https://gitlab.mpi-sws.org/FP/semantics-course/issues"
 version: "dev"
 
 depends: [
-  "coq" { (>= "8.14" & < "8.18~") | (= "dev") }
-  "coq-iris-heap-lang" { (= "dev.2023-05-19.0.89b39c82") | (= "dev") }
-  "coq-equations" { (= "1.2.4+8.13") | (= "1.3+8.14") | (= "1.3+8.15")  | (= "1.3+8.16") | (= "1.3+8.17") }
-  "coq-autosubst" { (= "1.7") | (= "dev")  }
+  "coq" { (>= "8.18" & < "8.19~") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2023-10-03.0.70b30af7") | (= "dev") }
+  "coq-equations" { (= "1.3+8.18") }
+  "coq-autosubst" { (= "1.8") | (= "dev")  }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/program_logics/heap_lang/primitive_laws.v b/theories/program_logics/heap_lang/primitive_laws.v
index 6ce0ff7c144a0f31cdfb31a10aa6ac2c4665829a..e31f12fa73b31e178746a922b1dc143bb0932e6f 100644
--- a/theories/program_logics/heap_lang/primitive_laws.v
+++ b/theories/program_logics/heap_lang/primitive_laws.v
@@ -68,10 +68,11 @@ Proof. apply mapsto_valid. Qed.
 Lemma mapsto_valid_2 l dq1 dq2 v1 v2 :
   l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝.
 Proof.
-  iIntros "H1 H2". iDestruct (mapsto_valid_2 with "H1 H2") as %[? [=?]]. done.
+  iIntros "H1 H2". 
+  iDestruct (mapsto_valid_2 with "H1 H2") as %[? [=]]. done.
 Qed.
 Lemma mapsto_agree l dq1 dq2 v1 v2 : l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜v1 = v2⌝.
-Proof. iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %[=?]. done. Qed.
+Proof. iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %[=]. done. Qed.
 
 Lemma mapsto_combine l dq1 dq2 v1 v2 :
   l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ l ↦{dq1 ⋅ dq2} v1 ∗ ⌜v1 = v2⌝.
diff --git a/theories/program_logics/resource_algebras.v b/theories/program_logics/resource_algebras.v
index 381ea9a318207072c61218d39ff0d8b8b335a0ed..66fa150c809e70b73db90803cd61c3d45b3fb781 100644
--- a/theories/program_logics/resource_algebras.v
+++ b/theories/program_logics/resource_algebras.v
@@ -675,9 +675,9 @@ Section sum.
         f_equiv. eauto using lra_pcore_l.
     - intros [a|b|] ? [= Ha]; subst; auto; rewrite csum_pcore in Ha.
       + destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
-        feed inversion (lra_pcore_idemp a ca); auto; rewrite csum_pcore; by simplify_option_eq.
+        oinversion (lra_pcore_idemp a ca); auto; rewrite csum_pcore; by simplify_option_eq.
       + destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
-        feed inversion (lra_pcore_idemp b cb); auto; rewrite csum_pcore; by simplify_option_eq.
+        oinversion (lra_pcore_idemp b cb); auto; rewrite csum_pcore; by simplify_option_eq.
     - intros x y ? [->|[(a&a'&->&->&?)|(b&b'&->&->&?)]]%csum_included [= Ha].
       + exists CsumBot. rewrite csum_included; eauto.
       + destruct (pcore a) as [ca|] eqn:?; rewrite csum_pcore; rewrite csum_pcore in Ha; simplify_option_eq.
diff --git a/theories/type_systems/systemf/binary_logrel.v b/theories/type_systems/systemf/binary_logrel.v
index 4717a13cee9b3f52823c40bfcd40924b2148dcaf..01d568a1dc31da1717bc880bfb5209f4b111903f 100644
--- a/theories/type_systems/systemf/binary_logrel.v
+++ b/theories/type_systems/systemf/binary_logrel.v
@@ -1051,7 +1051,7 @@ Lemma sem_typing_ctx_equiv Δ Γ e1 e2 A :
 Proof.
   intros Hsem ? ? C Hty. eapply sem_typed_congruence in Hty; last done.
   all: try done.
-  feed pose proof (Hty ∅ ∅ δ_any) as He; first constructor.
+  opose proof* (Hty ∅ ∅ δ_any) as He; first constructor.
   revert He. rewrite !subst_map_empty.
   simp type_interp. destruct 1 as (v1 & v2 & Hbs1 & Hbs2 & Hv).
   simp type_interp in Hv. destruct Hv as (z & -> & ->). eauto.