diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 20000068b4fdb576b99c7d9c5ce24af44c213546..e82d49dfa8109c51c2c60943a38c9f66b5b385e0 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -28,10 +28,10 @@ variables:
 
 ## Build jobs
 
-build-coq.8.15.1:
+build-coq.8.17.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.15.1"
+    OPAM_PINS: "coq version 8.17.0"
     DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
   tags:
@@ -40,7 +40,7 @@ build-coq.8.15.1:
 trigger-iris.timing:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.15.1   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
+    OPAM_PINS: "coq version 8.17.0   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
   tags:
   - fp-timing
   only:
diff --git a/README.md b/README.md
index e51dd4067605c9e1a54ad1e5725eaa8cfcd46406..d7439865d5014e430cd9ea85fa38a7128ad4e35d 100644
--- a/README.md
+++ b/README.md
@@ -6,7 +6,7 @@ This is the Coq development accompanying lambda-Rust.
 
 This version is known to compile with:
 
- - Coq 8.15.1
+ - Coq 8.17.0
  - A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris)
 
 ## Building from source
diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 862ba52453f6838c41dc598556c05c59b0e6e074..a1facd94e1381529537d9d9e7e57393e4f8d32c3 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2023-03-09.0.f91e8eab") | (= "dev") }
+  "coq-iris" { (= "dev.2023-05-02.4.943e9b74") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/adequacy.v b/theories/lang/adequacy.v
index ec4b64cdbbca5c7e96f1724655acd00dc795a529..5fdf7378de8e889bac7fe119398ddc48fee76cad 100644
--- a/theories/lang/adequacy.v
+++ b/theories/lang/adequacy.v
@@ -5,9 +5,9 @@ From lrust.lang Require Import proofmode notation.
 From iris.prelude Require Import options.
 
 Class lrustGpreS Σ := HeapGpreS {
-  lrustGpreS_irig :> invGpreS Σ;
-  lrustGpreS_heap :> inG Σ (authR heapUR);
-  lrustGpreS_heap_freeable :> inG Σ (authR heap_freeableUR)
+  lrustGpreS_irig :: invGpreS Σ;
+  lrustGpreS_heap :: inG Σ (authR heapUR);
+  lrustGpreS_heap_freeable :: inG Σ (authR heap_freeableUR)
 }.
 
 Definition lrustΣ : gFunctors :=
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 4836e47f9230d3abb6d80b9cc1abeb85468cad39..e3f918db4d275000f1375d3f198197d874df8ab5 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -19,8 +19,8 @@ Definition heap_freeableUR : ucmra :=
   gmapUR block (prodR fracR (gmapR Z (exclR unitO))).
 
 Class heapGS Σ := HeapGS {
-  heap_inG :> inG Σ (authR heapUR);
-  heap_freeable_inG :> inG Σ (authR heap_freeableUR);
+  heap_inG :: inG Σ (authR heapUR);
+  heap_freeable_inG :: inG Σ (authR heap_freeableUR);
   heap_name : gname;
   heap_freeable_name : gname
 }.
@@ -274,7 +274,7 @@ Section heap.
   Proof. revert i. induction n as [|n IH]=>i; first done. by apply insert_valid. Qed.
 
   Lemma heap_freeable_op_eq l q1 q2 n n' :
-    †{q1}l…n ∗ †{q2}l+ₗn … n' ⊣⊢ †{q1+q2}l…(n+n').
+    †{q1}l…n ∗ †{q2}l +ₗ n … n' ⊣⊢ †{q1+q2}l…(n+n').
   Proof.
     by rewrite heap_freeable_eq /heap_freeable_def -own_op -auth_frag_op
       singleton_op -pair_op inter_op.
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 47f69d9baf88521f35c7e79b20beba7bdcfa3604..16a15295a5fead45a95c63f310fa5ddd0916f9ae 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -402,7 +402,7 @@ Lemma shift_loc_0_nat l : l +â‚— 0%nat = l.
 Proof. destruct l as [b o]. rewrite /shift_loc /=. f_equal. lia. Qed.
 
 Global Instance shift_loc_inj l : Inj (=) (=) (shift_loc l).
-Proof. destruct l as [b o]; intros n n' [=?]; lia. Qed.
+Proof. destruct l as [b o]; intros n n' [= ?]; lia. Qed.
 
 Lemma shift_loc_block l n : (l +â‚— n).1 = l.1.
 Proof. done. Qed.
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 305e4000594021b256b4ca5701895750bdd08563..5b4e7d9d56547f38225f88ea70562aa92aeb1826 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -108,7 +108,7 @@ Definition arc_stR :=
   prodUR (optionUR (csumR (prodR (prodR fracR positiveR) (optionR (exclR unitO)))
                           (exclR unitO))) natUR.
 Class arcG Σ :=
-  RcG :> inG Σ (authR arc_stR).
+  RcG :: inG Σ (authR arc_stR).
 Definition arcΣ : gFunctors := #[GFunctor (authR arc_stR)].
 Global Instance subG_arcΣ {Σ} : subG arcΣ Σ → arcG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/lang/lib/spawn.v b/theories/lang/lib/spawn.v
index b176e3f3c5e6c7f71dede8b7893e688bbbc9e020..07a32237ac12a79036e8b03f2cfa96ea55f98ba9 100644
--- a/theories/lang/lib/spawn.v
+++ b/theories/lang/lib/spawn.v
@@ -28,7 +28,7 @@ Definition join : val :=
       "join" ["c"].
 
 (** The CMRA & functor we need. *)
-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 Σ.
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 76a60e18ab968233955e6d626f7c684f85edfd45..ae3b1cb4797e861ffa97e0173137cc20f1c82910 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -8,7 +8,7 @@ Import uPred.
 
 Class lrustGS Σ := LRustGS {
   lrustGS_invGS : invGS Σ;
-  lrustGS_heapGS :> heapGS Σ
+  lrustGS_heapGS :: heapGS Σ
 }.
 
 Global Instance lrustGS_irisGS `{!lrustGS Σ} : irisGS lrust_lang Σ := {
diff --git a/theories/lang/races.v b/theories/lang/races.v
index 0c0f6ca7c428d6391504e91bf1006cb06e2a42ff..501581fd0aaeb8c8947d36b6815c163085627ff9 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -144,7 +144,7 @@ Proof.
     - subst. by rewrite /shift_loc Z.add_0_r -surjective_pairing lookup_delete.
     - replace i with (1+(i-1)) by lia.
       rewrite lookup_delete_ne -shift_loc_assoc ?IH //; first lia.
-      destruct l; intros [=?]. lia. }
+      destruct l; intros [= ?]. lia. }
   assert (FREE' : σ' !! l = None).
   { inversion Ha1; clear Ha1; inv_head_step. auto. }
   destruct Hred2 as (κ'&e2'&σ''&ef&?).
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index f73a58ed161cad5c456f4a7baa7ad32f7f1f7304..6d1d6468644d6fe66f9830108cad0f296a8f1aa9 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -4,7 +4,7 @@ From iris.algebra Require Import frac.
 From lrust.lifetime Require Export at_borrow.
 From iris.prelude Require Import options.
 
-Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
+Class frac_borG Σ := frac_borG_inG :: inG Σ fracR.
 
 Local Definition frac_bor_inv `{!invGS Σ, !lftGS Σ userE, !frac_borG Σ}
                               (φ : Qp → iProp Σ) γ κ' :=
diff --git a/theories/lifetime/meta.v b/theories/lifetime/meta.v
index b9e4f8af89233797307c152eda21b77b22ee9a33..4fe35cf4a03762086f284cd2d99df5731c76c0ed 100644
--- a/theories/lifetime/meta.v
+++ b/theories/lifetime/meta.v
@@ -7,7 +7,7 @@ From iris.prelude Require Import options.
 [gname]) to a lifetime (as is required for types using branding). *)
 
 Class lft_metaG Σ := LftMetaG {
-  lft_meta_inG :> inG Σ (dyn_reservation_mapR (agreeR gnameO));
+  lft_meta_inG :: inG Σ (dyn_reservation_mapR (agreeR gnameO));
 }.
 Definition lft_metaΣ : gFunctors :=
   #[GFunctor (dyn_reservation_mapR (agreeR gnameO))].
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index e887cdca71b1f1365807f9bbb755ed624c162ad4..026e51efd43bd010eba574650ee9c48c2eda3fa3 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -41,25 +41,25 @@ Definition borUR := gmapUR slice_name (prodR fracR (agreeR bor_stateO)).
 Definition inhUR := gset_disjUR slice_name.
 
 Class lftGS Σ (userE : coPset) := LftG {
-  lft_box :> boxG Σ;
-  alft_inG :> inG Σ (authR alftUR);
+  lft_box :: boxG Σ;
+  alft_inG :: inG Σ (authR alftUR);
   alft_name : gname;
-  ilft_inG :> inG Σ (authR ilftUR);
+  ilft_inG :: inG Σ (authR ilftUR);
   ilft_name : gname;
-  lft_bor_inG :> inG Σ (authR borUR);
-  lft_cnt_inG :> inG Σ (authR natUR);
-  lft_inh_inG :> inG Σ (authR inhUR);
+  lft_bor_inG :: inG Σ (authR borUR);
+  lft_cnt_inG :: inG Σ (authR natUR);
+  lft_inh_inG :: inG Σ (authR inhUR);
   userE_lftN_disj : ↑lftN ## userE;
 }.
 Definition lftGS' := lftGS.
 
 Class lftGpreS Σ := LftGPreS {
-  lft_preG_box :> boxG Σ;
-  alft_preG_inG :> inG Σ (authR alftUR);
-  ilft_preG_inG :> inG Σ (authR ilftUR);
-  lft_preG_bor_inG :> inG Σ (authR borUR);
-  lft_preG_cnt_inG :> inG Σ (authR natUR);
-  lft_preG_inh_inG :> inG Σ (authR inhUR);
+  lft_preG_box :: boxG Σ;
+  alft_preG_inG :: inG Σ (authR alftUR);
+  ilft_preG_inG :: inG Σ (authR ilftUR);
+  lft_preG_bor_inG :: inG Σ (authR borUR);
+  lft_preG_cnt_inG :: inG Σ (authR natUR);
+  lft_preG_inh_inG :: inG Σ (authR inhUR);
 }.
 Definition lftGpreS' := lftGpreS.
 
diff --git a/theories/typing/lib/brandedvec.v b/theories/typing/lib/brandedvec.v
index 94e4ad987d391d8c42d0506f3f74f20f9c677146..29577ea86c9c287ce2c9d55dd4492bae9f68ed47 100644
--- a/theories/typing/lib/brandedvec.v
+++ b/theories/typing/lib/brandedvec.v
@@ -8,8 +8,8 @@ From iris.prelude Require Import options.
 
 Definition brandidx_stR := max_natUR.
 Class brandidxG Σ := BrandedIdxG {
-  brandidx_inG :> inG Σ (authR brandidx_stR);
-  brandidx_gsingletonG :> lft_metaG Σ;
+  brandidx_inG :: inG Σ (authR brandidx_stR);
+  brandidx_gsingletonG :: lft_metaG Σ;
 }.
 
 Definition brandidxΣ : gFunctors
diff --git a/theories/typing/lib/ghostcell.v b/theories/typing/lib/ghostcell.v
index bb868034786a44389e0998ad135ff7fc19078082..1cd696e9ec46a4984a1fbb867aa5439cf60d1534 100644
--- a/theories/typing/lib/ghostcell.v
+++ b/theories/typing/lib/ghostcell.v
@@ -69,8 +69,8 @@ Definition ghosttoken_stR :=
   (csumR (exclR unitO) ((prodR (agreeR lftO) fracR))).
 
 Class ghostcellG Σ := GhostcellG {
-  ghostcell_inG :> inG Σ (ghosttoken_stR);
-  ghostcell_gsingletonG :> lft_metaG Σ;
+  ghostcell_inG :: inG Σ (ghosttoken_stR);
+  ghostcell_gsingletonG :: lft_metaG Σ;
 }.
 
 Definition ghostcellΣ : gFunctors
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index bf265d14fe1c0310c9d29d8ca791e7c20b345866..9e3f2ad0d7da0768365ddf523d0e2220c7b4fa71 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -9,7 +9,7 @@ From iris.prelude Require Import options.
 Definition rc_stR :=
   prodUR (optionUR (csumR (prodR fracR positiveR) (exclR unitO))) natUR.
 Class rcG Σ :=
-  RcG :> inG Σ (authR rc_stR).
+  RcG :: inG Σ (authR rc_stR).
 Definition rcΣ : gFunctors := #[GFunctor (authR rc_stR)].
 Global Instance subG_rcΣ {Σ} : subG rcΣ Σ → rcG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index da4ced23933c370df1eee8c352e404d473c003b0..f136a89b5df3e5e0fb8c81f42037b9c27239ff7a 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -11,7 +11,7 @@ Definition refcell_stR :=
              fracR)
              positiveR).
 Class refcellG Σ :=
-  RefCellG :> inG Σ (authR refcell_stR).
+  RefCellG :: inG Σ (authR refcell_stR).
 Definition refcellΣ : gFunctors := #[GFunctor (authR refcell_stR)].
 Global Instance subG_refcellΣ {Σ} : subG refcellΣ Σ → refcellG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index ec3810b17fef648cb38e4d91944f7d66a80a5a55..a34db311822e9f10e43d43e76ca6b8545cd04f97 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -8,7 +8,7 @@ From iris.prelude Require Import options.
 Definition rwlock_stR :=
   optionUR (csumR (exclR unitO) (prodR (prodR (agreeR lftO) fracR) positiveR)).
 Class rwlockG Σ :=
-  RwLockG :> inG Σ (authR rwlock_stR).
+  RwLockG :: inG Σ (authR rwlock_stR).
 Definition rwlockΣ : gFunctors := #[GFunctor (authR rwlock_stR)].
 Global Instance subG_rwlockΣ {Σ} : subG rwlockΣ Σ → rwlockG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index a2623b755f341576851f8d20c9d39b94633a0246..11c4e6989217d52506a702747c92abdeeb840537 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -8,10 +8,10 @@ From iris.prelude Require Import options.
 
 
 Class typeGpreS Σ := PreTypeG {
-  type_preG_lrustGS :> lrustGpreS Σ;
-  type_preG_lftGS :> lftGpreS Σ;
-  type_preG_na_invG :> na_invG Σ;
-  type_preG_frac_borG :> frac_borG Σ
+  type_preG_lrustGS :: lrustGpreS Σ;
+  type_preG_lftGS :: lftGpreS Σ;
+  type_preG_na_invG :: na_invG Σ;
+  type_preG_frac_borG :: frac_borG Σ
 }.
 
 Definition typeΣ : gFunctors :=
diff --git a/theories/typing/type.v b/theories/typing/type.v
index e577ecff2e8f8ba062e73fe07ed6bdf746f26b9d..29154f26549c680a4474d3497ba45f3509a907ac 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -7,10 +7,10 @@ From lrust.typing Require Import lft_contexts.
 From iris.prelude Require Import options.
 
 Class typeGS Σ := TypeG {
-  type_lrustGS :> lrustGS Σ;
-  type_lftGS :> lftGS Σ lft_userE;
-  type_na_invG :> na_invG Σ;
-  type_frac_borrowG :> frac_borG Σ
+  type_lrustGS :: lrustGS Σ;
+  type_lftGS :: lftGS Σ lft_userE;
+  type_na_invG :: na_invG Σ;
+  type_frac_borrowG :: frac_borG Σ
 }.
 
 Definition lrustN := nroot .@ "lrust".