diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 7e22d5d..6096fe0 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -20,10 +20,9 @@ jobs:
           - "dev"
           - "8.18"
           - "8.17"
-          - "8.16"
       fail-fast: false
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: "iris-simp-lang.opam"
@@ -35,18 +34,16 @@ jobs:
             startGroup "Print opam config"
               opam config list; opam repo list; opam list
             endGroup
-  # NOTE: re-enable this job once Iris releases something after 4.0.0. (The only
-  # issue is that `iSolveTC` was moved to `tc_solve` in stdpp.)
-  #build-release:
-  #  name: build (released iris, coq dev)
-  #  runs-on: ubuntu-latest
-  #  strategy:
-  #    fail-fast: false
-  #  steps:
-  #    - uses: actions/checkout@v2
-  #    - uses: coq-community/docker-coq-action@v1
-  #      with:
-  #        custom_image: "coqorg/coq:dev"
+  build-release:
+    name: build (released iris, coq dev)
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+    steps:
+      - uses: actions/checkout@v4
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          custom_image: "coqorg/coq:dev"
 
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme
diff --git a/README.md b/README.md
index 8eb65e8..f86aea3 100644
--- a/README.md
+++ b/README.md
@@ -52,8 +52,8 @@ There are a few files that are optional reading which make the tutorial work:
 
 ## Compiling
 
-This development relies on a development version of Iris and Coq 8.14 or later.
-We test Coq 8.14, 8.15, 8.16, and master with Iris dev in CI. (The released
+This development relies on a development version of Iris and Coq 8.17 or later.
+We test Coq 8.17, 8.18, and master with Iris dev in CI. (The released
 version of Iris is currently incompatible.)
 
 You'll need to install Iris, which is easiest done through opam. There are
diff --git a/_CoqProject b/_CoqProject
index 6dfcf7c..7d43a95 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -2,10 +2,7 @@
 
 -arg -w -arg -redundant-canonical-projection
 -arg -w -arg -notation-overriden
-# Fixing this one requires Coq 8.15.
--arg -w -arg -deprecated-typeclasses-transparency-without-locality
-# Fixing this requires Coq 8.17
--arg -w -arg -future-coercion-class-field
+-arg -w -arg -deprecated-since-8.19
 
 src/lang.v
 src/notation.v
diff --git a/src/adequacy.v b/src/adequacy.v
index 973ea8a..e622371 100644
--- a/src/adequacy.v
+++ b/src/adequacy.v
@@ -33,8 +33,8 @@ ghost name and associated state.
 (** These assumptions are just functors in Σ, unlike simpGS which also has a
 ghost name. *)
 Class simpGpreS Σ := SimpPreG {
-  simp_preG_iris :> invGpreS Σ;
-  simp_preG_heap :> heap_mapGpreS loc val Σ;
+  simp_preG_iris :: invGpreS Σ;
+  simp_preG_heap :: heap_mapGpreS loc val Σ;
 }.
 
 Definition simpΣ : gFunctors :=
diff --git a/src/examples/spawn.v b/src/examples/spawn.v
index dfc2877..3440663 100644
--- a/src/examples/spawn.v
+++ b/src/examples/spawn.v
@@ -23,7 +23,7 @@ Definition join : val :=
 
 (** The CMRA & functor we need. *)
 (* Not bundling simpGS, as it may be shared with other users. *)
-Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitO) }.
+Class spawnG Σ := SpawnG { spawn_tokG :: inG Σ (exclR unitO) }.
 Definition spawnΣ : gFunctors := #[GFunctor (exclR unitO)].
 
 Global Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
@@ -78,4 +78,4 @@ Proof.
 Qed.
 End proof.
 
-Typeclasses Opaque join_handle.
+#[export] Typeclasses Opaque join_handle.
diff --git a/src/heap_lib.v b/src/heap_lib.v
index 9a99d3e..c415064 100644
--- a/src/heap_lib.v
+++ b/src/heap_lib.v
@@ -19,11 +19,11 @@ directly in the IPM).
 |*)
 
 Class heap_mapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
-  heap_mapGpreS_inG :> inG Σ (heap_mapR L V);
+  heap_mapGpreS_inG :: inG Σ (heap_mapR L V);
 }.
 
 Class heap_mapGS (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapGS {
-  heap_map_inG :> heap_mapGpreS L V Σ;
+  heap_map_inG :: heap_mapGpreS L V Σ;
   heap_map_name : gname;
 }.
 Global Arguments GenHeapGS L V Σ {_ _ _} _ : assert.
diff --git a/src/primitive_laws.v b/src/primitive_laws.v
index 84cda14..a882d5a 100644
--- a/src/primitive_laws.v
+++ b/src/primitive_laws.v
@@ -61,7 +61,7 @@ them in `adequacy.v`.
 
 Class simpGS Σ := SimpGS {
   simp_invGS : invGS Σ;
-  simp_heap_mapG :> heap_mapGS loc val Σ;
+  simp_heap_mapG :: heap_mapGS loc val Σ;
 }.
 
 (* Observe that this instance assumes [simpGS Σ], which already has a fixed ghost