diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 43405f905e1e2d32f5a6df74e95ca2d03d6630f0..2d7e19c922b0aa67c4d363a489fb57e783b1c507 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"
   tags:
   - fp-timing
diff --git a/README.md b/README.md
index 881a385d29bfb6f0abc3635673825b52a074a6d4..88b3518b71204f1a962383a46d7e9e4f497e8732 100644
--- a/README.md
+++ b/README.md
@@ -10,7 +10,7 @@ See the small ReLoC [docs/guide.md](docs/guide.md) and the Iris [ProofGuide.md](
 
 ## Building
 
-This project has been tested with Coq 8.15.1.
+This project has been tested with Coq 8.17.0.
 
 ### OPAM
 
diff --git a/coq-reloc.opam b/coq-reloc.opam
index f06d4d12b08c0e76e67cf4750ab75bd7a5cbe9dc..1c86cf8993b2f4a740b0f39e83fa8d2c2527b028 100644
--- a/coq-reloc.opam
+++ b/coq-reloc.opam
@@ -6,7 +6,7 @@ bug-reports: "https://gitlab.mpi-sws.org/dfrumin/reloc/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/dfrumin/reloc.git"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2023-03-17.1.a7a250e6") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2023-05-02.4.943e9b74") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
 
diff --git a/theories/examples/folly_queue/refinement.v b/theories/examples/folly_queue/refinement.v
index 5d5ad0b8f8fc31d0cfe45f27ab9bf03789e3d0c4..77be85f3be9e8fe4c6ce6eb79439bdb2606f401e 100644
--- a/theories/examples/folly_queue/refinement.v
+++ b/theories/examples/folly_queue/refinement.v
@@ -17,8 +17,8 @@ Definition requestReg := gmap nat ref_id.
 Definition requestRegR := authR $ gmapUR nat (agreeR ref_idO).
 
 Class queueG Σ := {
-  queue_listUR :> inG Σ listUR;
-  queue_requestUR :> inG Σ requestRegR;
+  queue_listUR :: inG Σ listUR;
+  queue_requestUR :: inG Σ requestRegR;
 }.
 
 (* For the [lia] tactic. *)
diff --git a/theories/examples/folly_queue/set.v b/theories/examples/folly_queue/set.v
index 07fbcfd6a132bdd52a0c05cf6ffbbcb9a2f2b328..843ea31518a4963b501b3a90a873bacbb6fa09d2 100644
--- a/theories/examples/folly_queue/set.v
+++ b/theories/examples/folly_queue/set.v
@@ -19,8 +19,8 @@ Definition set_singleton `{!EqDecision A} (a : A) :=
   set_cf (λ a', if decide (a = a') then true else false).
 
 Definition set_nat := set_of nat.
-Definition set_even := set_cf even.
-Definition set_odd := set_cf odd.
+Definition set_even := set_cf Nat.even.
+Definition set_odd := set_cf Nat.odd.
 
 Lemma split_even_odd : set_nat ≡ set_even ⋅ set_odd.
 Proof.
@@ -35,7 +35,7 @@ Definition set_above n := set_cf (λ n', n <=? n').
 Definition set_upto n := set_cf (λ n', n' <? n).
 
 Lemma set_above_lookup n m : n ≤ m → set_above n m = Excl' ().
-Proof. rewrite /set_above /set_cf. by intros ->%leb_le. Qed.
+Proof. rewrite /set_above /set_cf. by intros ->%Nat.leb_le. Qed.
 
 Lemma set_above_lookup_none n m : m < n → (set_above n) m = None.
 Proof. rewrite /set_above /set_cf. by intros ->%Nat.leb_gt. Qed.
@@ -120,8 +120,7 @@ Proof.
   rewrite /set_singleton. rewrite /set_cf.
   rewrite discrete_fun_lookup_op.
   destruct (le_lt_dec n n').
-  - autorewrite with natb.
-    destruct (le_lt_or_eq n n' l); autorewrite with natb; done.
+  - case_decide; subst; by autorewrite with natb.
   - autorewrite with natb. done.
 Qed.
 
@@ -131,7 +130,7 @@ Proof.
   rewrite discrete_fun_lookup_op.
   destruct (le_gt_dec m n).
   - rewrite (set_upto_lookup (n + 1)); last lia.
-    destruct (le_lt_or_eq m n l).
+    assert (m < n ∨ m = n) as [] by lia.
     * autorewrite with natb. done.
     * subst. autorewrite with natb. done.
   - autorewrite with natb. done.
@@ -142,12 +141,12 @@ Definition set_prop {A : Type} (f : A → Prop) `{!∀ a, Decision (f a)} : setU
   λ a, if decide (f a) then Some (Excl ()) else None.
 
 (* All even numbers except for the first n. *)
-Definition set_even_drop n := set_cf (λ n', (even n') && (2 * n <=? n')).
+Definition set_even_drop n := set_cf (λ n', (Nat.even n') && (2 * n <=? n')).
 
 (* All odd numbers except for the first n. *)
-Definition set_odd_drop n := set_cf (λ n', (odd n') && (2 * n + 1 <=? n')).
+Definition set_odd_drop n := set_cf (λ n', (Nat.odd n') && (2 * n + 1 <=? n')).
 
-Lemma set_even_drop_lookup n m : Even m → 2 * n ≤ m → set_even_drop n m = Excl' ().
+Lemma set_even_drop_lookup n m : Nat.Even m → 2 * n ≤ m → set_even_drop n m = Excl' ().
 Proof.
   intros He Hle.
   rewrite /set_even_drop /set_cf.
diff --git a/theories/examples/folly_queue/singleElementQueue.v b/theories/examples/folly_queue/singleElementQueue.v
index ad60984448a683a811d23e6d6446494330241ec4..c3388d4b38137cafca4e6ab30be7b5aab3b9c1f8 100644
--- a/theories/examples/folly_queue/singleElementQueue.v
+++ b/theories/examples/folly_queue/singleElementQueue.v
@@ -61,7 +61,7 @@ Section spec.
 
   (* The resource for the turn sequencer. *)
   Definition TSR R (ℓ : loc) (n : nat) : iProp Σ :=
-    (if even n
+    (if Nat.even n
      then ℓ ↦ NONEV
      else ∃ v, ℓ ↦ SOMEV v ∗ R ((n - 1) / 2) v)%I.
 
diff --git a/theories/examples/folly_queue/turnSequencer.v b/theories/examples/folly_queue/turnSequencer.v
index d59d6e34123957f8589b3c019652c64ef446f9cf..aa8aa44f8119a39a65a5e4d0ff4210e84e71ad1b 100644
--- a/theories/examples/folly_queue/turnSequencer.v
+++ b/theories/examples/folly_queue/turnSequencer.v
@@ -28,7 +28,7 @@ Definition waitForTurn : val :=
 Definition turnSequencer : val :=
   (newTS, completeTurn, waitForTurn).
 
-Class TSG Σ := { TSG_tickets :> inG Σ (setUR nat) }.
+Class TSG Σ := { TSG_tickets :: inG Σ (setUR nat) }.
 
 (* Alternative spec for the TS. *)
 Section spec.
diff --git a/theories/examples/red_blue_flag.v b/theories/examples/red_blue_flag.v
index 4e2731f6a2987166847c0498c772dfa1508fc1ae..f38f314bf56e6ede8dbef8c74cf1c9a3cd3d3e02 100644
--- a/theories/examples/red_blue_flag.v
+++ b/theories/examples/red_blue_flag.v
@@ -57,8 +57,8 @@ Definition offerR :=
         (prodR fracR (agreeR ref_idO)).
 
 Class offerPreG Σ := OfferPreG {
-  offer_inG :> inG Σ offerR;
-  offer_token_inG :> inG Σ fracR;
+  offer_inG :: inG Σ offerR;
+  offer_token_inG :: inG Σ fracR;
 }.
 
 Section offer_theory.
diff --git a/theories/examples/stack_helping/helping_wrapper.v b/theories/examples/stack_helping/helping_wrapper.v
index 8e68dd470d0d0d6fa0c051f6142d7c99510b2d2b..773fd83a1a6ed09eb55e47646fdddb56619abe4d 100644
--- a/theories/examples/stack_helping/helping_wrapper.v
+++ b/theories/examples/stack_helping/helping_wrapper.v
@@ -61,7 +61,7 @@ Definition offerRegR :=
   gmapUR loc (agreeR (prodO valO (prodO gnameO ref_idO))).
 
 Class offerRegPreG Σ := OfferRegPreG {
-  offerReg_inG :> inG Σ (authUR offerRegR)
+  offerReg_inG :: inG Σ (authUR offerRegR)
 }.
 
 Definition offerize (x : (val * gname * ref_id)) :
diff --git a/theories/examples/stack_helping/offers.v b/theories/examples/stack_helping/offers.v
index b7819466841f7d880c8916ee69d5105c51ce0c9a..3c5db986817402a099a05df9ce10598216d1a7e5 100644
--- a/theories/examples/stack_helping/offers.v
+++ b/theories/examples/stack_helping/offers.v
@@ -13,7 +13,7 @@ Definition take_offer : val :=
   λ: "v", if: CAS (Snd "v") #0 #1 then SOME (Fst "v") else NONE.
 
 Definition offerR := exclR unitR.
-Class offerG Σ := { offer_inG :> inG Σ offerR }.
+Class offerG Σ := { offer_inG :: inG Σ offerR }.
 Definition offerΣ : gFunctors := #[GFunctor offerR].
 Global Instance subG_offerΣ {Σ} : subG offerΣ Σ → offerG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/examples/stack_helping/stack.v b/theories/examples/stack_helping/stack.v
index bf2533f034e1ebf3bc8c827c8f49370ee1ceb8a0..e206268f89d39ea6c7c7b46747b189ef3e98c74e 100644
--- a/theories/examples/stack_helping/stack.v
+++ b/theories/examples/stack_helping/stack.v
@@ -87,7 +87,7 @@ Definition offerRegR :=
   gmapUR loc (agreeR (prodO valO (prodO gnameO ref_idO))).
 
 Class offerRegPreG Σ := OfferRegPreG {
-  offerReg_inG :> inG Σ (authR offerRegR)
+  offerReg_inG :: inG Σ (authR offerRegR)
 }.
 
 Definition offerize (x : (val * gname * ref_id)) :
diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v
index 22f7b55a50820836b7036a40941fc495b4ed3257..5b58aadb8499e790782b5dbae25e9cf27e8ebdb3 100644
--- a/theories/examples/symbol.v
+++ b/theories/examples/symbol.v
@@ -46,7 +46,7 @@ Definition symbol2 : val := λ: <>,
 
 (** * The actual refinement proof.
       Requires monotonic state *)
-Class msizeG Σ := MSizeG { msize_inG :> inG Σ (authR max_natUR) }.
+Class msizeG Σ := MSizeG { msize_inG :: inG Σ (authR max_natUR) }.
 Definition msizeΣ : gFunctors := #[GFunctor (authR max_natUR)].
 
 Global Instance subG_msizeΣ {Σ} : subG msizeΣ Σ → msizeG Σ.
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index b8949c23eaccde71b697b5b9c92856157b446c30..4d57628e47be2ddf2ea407d536182ee72fb8dbc9 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -18,7 +18,7 @@ Definition lrel_lock `{relocG Σ} : lrel Σ :=
   ∃ A, (() → A) * (A → ()) * (A → ()).
 
 Class tlockG Σ :=
-  tlock_G :> inG Σ (authR (gset_disjUR nat)).
+  tlock_G :: inG Σ (authR (gset_disjUR nat)).
 Definition tlockΣ : gFunctors :=
   #[ GFunctor (authR $ gset_disjUR nat) ].
 Global Instance subG_tlockΣ {Σ} : subG tlockΣ Σ → tlockG Σ.
@@ -28,7 +28,7 @@ Definition lockPool := gset ((loc * loc * gname) * loc).
 Definition lockPoolR := gsetUR ((loc * loc * gname) * loc).
 
 Class lockPoolG Σ :=
-  lockPool_inG :> inG Σ (authR lockPoolR).
+  lockPool_inG :: inG Σ (authR lockPoolR).
 Definition lockPoolΣ := #[ GFunctor (authR $ lockPoolR) ].
 Global Instance subG_lockPoolΣ {Σ} : subG lockPoolΣ Σ → lockPoolG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/examples/various.v b/theories/examples/various.v
index b35c5d81b1a3b803d70b7e56b6dcad50d78fdf18..dcd92d43098dd68a0ffb101e9448cedd95397e22 100644
--- a/theories/examples/various.v
+++ b/theories/examples/various.v
@@ -8,7 +8,7 @@ From reloc Require Export reloc.
 From reloc.lib Require Export lock counter Y.
 
 Definition oneshotR := csumR (exclR unitR) (agreeR unitR).
-Class oneshotG Σ := { oneshot_inG :> inG Σ oneshotR }.
+Class oneshotG Σ := { oneshot_inG :: inG Σ oneshotR }.
 Definition oneshotΣ : gFunctors := #[GFunctor oneshotR].
 Global Instance subG_oneshotΣ {Σ} : subG oneshotΣ Σ → oneshotG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/experimental/hocap/counter.v b/theories/experimental/hocap/counter.v
index 27d42bbde1b456bd883fe8f020bad9a847a5a52a..fed03f4cef53b1a76374e2d3a59efa4d3951c6d2 100644
--- a/theories/experimental/hocap/counter.v
+++ b/theories/experimental/hocap/counter.v
@@ -6,7 +6,7 @@ From iris.algebra Require Export auth frac excl.
 From iris.bi.lib Require Export fractional.
 
 Class cnt_hocapG Σ := CntG {
-    cnt_hocapG_inG :> inG Σ (authR $ optionUR (prodR fracR (agreeR natO)));
+    cnt_hocapG_inG :: inG Σ (authR $ optionUR (prodR fracR (agreeR natO)));
 }.
 
 Definition cnt_hocapΣ := GFunctor (authR (optionUR (prodR fracR (agreeR natO)))).
diff --git a/theories/lib/lock.v b/theories/lib/lock.v
index 43b32f56bf9692e4c09a4c1cdc05ee633054545a..574b51afa5479d44c122ba8a2e6892ffcae6044a 100644
--- a/theories/lib/lock.v
+++ b/theories/lib/lock.v
@@ -15,7 +15,7 @@ Definition with_lock : val := λ: "e" "l" "x",
   let: "v" := "e" "x" in
   release "l";; "v".
 
-Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitO) }.
+Class lockG Σ := LockG { lock_tokG :: inG Σ (exclR unitO) }.
 Definition lockΣ : gFunctors := #[GFunctor (exclR unitO)].
 
 Global Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
diff --git a/theories/logic/adequacy.v b/theories/logic/adequacy.v
index 41f9db969bd955c30b9e2b0d895cf80e11275941..664e046c2e0d709459940e619299f3609140537a 100644
--- a/theories/logic/adequacy.v
+++ b/theories/logic/adequacy.v
@@ -6,8 +6,8 @@ From iris.heap_lang Require Export adequacy.
 From reloc.logic Require Export spec_ra model.
 
 Class relocPreG Σ := RelocPreG {
-  reloc_preG_heap :> heapGpreS Σ;
-  reloc_preG_cfg  :> inG Σ (authR cfgUR)
+  reloc_preG_heap :: heapGpreS Σ;
+  reloc_preG_cfg  :: inG Σ (authR cfgUR)
 }.
 
 Definition relocΣ : gFunctors := #[heapΣ; GFunctor (authR cfgUR)].
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index d6cb8965276452cd01f54c4d9b9d48a765de5159..d5502dde1ab504aac458f369676cccfd487906a3 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -17,10 +17,10 @@ Definition tpoolUR : ucmra := gmapUR nat (exclR exprO).
 Definition cfgUR := prodUR tpoolUR (heapUR loc (option val)).
 
 (** The CMRA for the thread pool. *)
-Class cfgSG Σ := CFGSG { cfg_inG :> inG Σ (authR cfgUR); cfg_name : gname }.
+Class cfgSG Σ := CFGSG { cfg_inG :: inG Σ (authR cfgUR); cfg_name : gname }.
 Class relocG Σ := RelocG {
-  relocG_heapG :> heapGS Σ;
-  relocG_cfgG :> cfgSG Σ;
+  relocG_heapG :: heapGS Σ;
+  relocG_cfgG :: cfgSG Σ;
 }.
 
 Definition to_heap {L V} `{Countable L} : gmap L V → heapUR L V :=
diff --git a/theories/prelude/arith.v b/theories/prelude/arith.v
index 84ea7e73445a3ba5eef271a19286926cfbf13db3..1843b6316e68314508a53e0d244f8dcfca4d4910 100644
--- a/theories/prelude/arith.v
+++ b/theories/prelude/arith.v
@@ -77,7 +77,7 @@ Proof.
 Qed.
 
 Lemma ltb_lt_1 n m : n < m → (n <? m) = true.
-Proof. apply ltb_lt. Qed.
+Proof. apply Nat.ltb_lt. Qed.
 
 (* This is just [Nat.mul_comm] with things ordered differently. *)
 Lemma div_mod' (x y : nat) : y ≠ 0 →  (x `div` y) * y + x `mod` y = x.
@@ -87,12 +87,12 @@ Proof. symmetry. rewrite Nat.mul_comm. apply Nat.div_mod. done. Qed.
 Lemma mod0 (a : nat) : 0 `mod` a = 0.
 Proof.
   destruct a; first done.
-  by apply Nat.mod_0_l.
+  by apply Nat.Div0.mod_0_l.
 Qed.
 Lemma div0 (a : nat) : 0 `div` a = 0.
 Proof.
   destruct a; first done.
-  by apply Nat.div_0_l.
+  by apply Nat.Div0.div_0_l.
 Qed.
 
 
@@ -121,4 +121,3 @@ Proof.
   - destruct l; done.
   - destruct l; simpl; first lia. intros H%IH. lia.
 Qed.
-
diff --git a/theories/prelude/bijections.v b/theories/prelude/bijections.v
index 9a11fcf1474747a8ff5302d97cf9149726d4d83f..af6c5245723dab4b2286c57ae8d9d50f9bf90bd8 100644
--- a/theories/prelude/bijections.v
+++ b/theories/prelude/bijections.v
@@ -44,9 +44,9 @@ Qed.
 
 Definition bijUR := gsetUR (A * B).
 Class pBijPreG Σ := PBijPreG
-{ pBijPreG_inG :> inG Σ (authR bijUR) }.
+{ pBijPreG_inG :: inG Σ (authR bijUR) }.
 Class pBijG Σ := PBijG
-{ pBijG_inG :> inG Σ (authR bijUR)
+{ pBijG_inG :: inG Σ (authR bijUR)
 ; pBijG_name : gname }.
 Definition pBijΣ : gFunctors := #[ GFunctor (authR bijUR) ].
 Global Instance subG_pBijΣ {Σ} : subG pBijΣ Σ → pBijPreG Σ.
diff --git a/theories/typing/contextual_refinement_alt.v b/theories/typing/contextual_refinement_alt.v
index e52c6a44f2d90180b97e87f9539c66dac820d8d4..976ee6455f054608f41b33e8f744319c9a235fb1 100644
--- a/theories/typing/contextual_refinement_alt.v
+++ b/theories/typing/contextual_refinement_alt.v
@@ -95,7 +95,7 @@ Proof.
       { apply nsteps_once_inv. by eapply pure_exec. }
       destruct_and!. simplify_eq/=.
       eapply IH; eauto.
-    + eapply (IH m (lt_n_Sn m) (t1 ++ e2 :: t2 ++ efs)); eauto.
+    + eapply (IH m (Nat.lt_succ_diag_r m) (t1 ++ e2 :: t2 ++ efs)); eauto.
 Qed.
 
 Lemma ctx_refines_alt_impl Γ e1 e2 τ :