diff --git a/_CoqProject b/_CoqProject
index 5898a24d48df2b440a1b5877372d1172c164a146..26c948832c84aef416aa43fc4e017ec07f22c3da 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -2,8 +2,6 @@
 # `-Q $PACKAGE[/ ]` so that we can filter out the right ones for each package.
 -Q stdpp stdpp
 -Q stdpp_unstable stdpp.unstable
-# Fixing this one requires Coq 8.17
--arg -w -arg -future-coercion-class-field
 # Fixing this one requires Coq 8.19
 -arg -w -arg -argument-scope-delimiter
 
diff --git a/stdpp/base.v b/stdpp/base.v
index a2aeb5380058252743c4864f3b3a23c335dccf47..73a43ae55c64dd0309275b43b07d0a72b64b329f 100644
--- a/stdpp/base.v
+++ b/stdpp/base.v
@@ -383,7 +383,7 @@ an explicit class instead of a notation for two reasons:
   Using the [RelDecision], the [f] is hidden under a lambda, which prevents
   unnecessary evaluation. *)
 Class RelDecision {A B} (R : A → B → Prop) :=
-  decide_rel x y :> Decision (R x y).
+  decide_rel x y :: Decision (R x y).
 Global Hint Mode RelDecision ! ! ! : typeclass_instances.
 Global Arguments decide_rel {_ _} _ {_} _ _ : simpl never, assert.
 Notation EqDecision A := (RelDecision (=@{A})).
@@ -513,14 +513,14 @@ Definition strict {A} (R : relation A) : relation A := λ X Y, R X Y ∧ ¬R Y X
 Global Instance: Params (@strict) 2 := {}.
 
 Class PartialOrder {A} (R : relation A) : Prop := {
-  partial_order_pre :> PreOrder R;
-  partial_order_anti_symm :> AntiSymm (=) R
+  partial_order_pre :: PreOrder R;
+  partial_order_anti_symm :: AntiSymm (=) R
 }.
 Global Hint Mode PartialOrder ! ! : typeclass_instances.
 
 Class TotalOrder {A} (R : relation A) : Prop := {
-  total_order_partial :> PartialOrder R;
-  total_order_trichotomy :> Trichotomy (strict R)
+  total_order_partial :: PartialOrder R;
+  total_order_trichotomy :: Trichotomy (strict R)
 }.
 Global Hint Mode TotalOrder ! ! : typeclass_instances.
 
@@ -1502,7 +1502,7 @@ Global Hint Mode SemiSet - ! - - - - : typeclass_instances.
 
 Class Set_ A C `{ElemOf A C, Empty C, Singleton A C,
     Union C, Intersection C, Difference C} : Prop := {
-  set_semi_set :> SemiSet A C;
+  set_semi_set :: SemiSet A C;
   elem_of_intersection (X Y : C) (x : A) : x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y;
   elem_of_difference (X Y : C) (x : A) : x ∈ X ∖ Y ↔ x ∈ X ∧ x ∉ Y
 }.
@@ -1510,7 +1510,7 @@ Global Hint Mode Set_ - ! - - - - - - : typeclass_instances.
 
 Class TopSet A C `{ElemOf A C, Empty C, Top C, Singleton A C,
     Union C, Intersection C, Difference C} : Prop := {
-  top_set_set :> Set_ A C;
+  top_set_set :: Set_ A C;
   elem_of_top' (x : A) : x ∈@{C} ⊤; (* We prove [elem_of_top : x ∈@{C} ⊤ ↔ True]
   in [sets.v], which is more convenient for rewriting. *)
 }.
@@ -1551,7 +1551,7 @@ Qed.
 anyway so as to avoid cycles in type class search. *)
 Class FinSet A C `{ElemOf A C, Empty C, Singleton A C, Union C,
     Intersection C, Difference C, Elements A C, EqDecision A} : Prop := {
-  fin_set_set :> Set_ A C;
+  fin_set_set :: Set_ A C;
   elem_of_elements (X : C) x : x ∈ elements X ↔ x ∈ X;
   NoDup_elements (X : C) : NoDup (elements X)
 }.
@@ -1575,7 +1575,7 @@ in a type constructor of type [Type → Type]. *)
 Class MonadSet M `{∀ A, ElemOf A (M A),
     ∀ A, Empty (M A), ∀ A, Singleton A (M A), ∀ A, Union (M A),
     !MBind M, !MRet M, !FMap M, !MJoin M} : Prop := {
-  monad_set_semi_set A :> SemiSet A (M A);
+  monad_set_semi_set A :: SemiSet A (M A);
   elem_of_bind {A B} (f : A → M B) (X : M A) (x : B) :
     x ∈ X ≫= f ↔ ∃ y, x ∈ f y ∧ y ∈ X;
   elem_of_ret {A} (x y : A) : x ∈@{M A} mret y ↔ x = y;
@@ -1606,9 +1606,9 @@ Global Instance: Params (@fresh) 3 := {}.
 Global Arguments fresh : simpl never.
 
 Class Infinite A := {
-  infinite_fresh :> Fresh A (list A);
+  infinite_fresh :: Fresh A (list A);
   infinite_is_fresh (xs : list A) : fresh xs ∉ xs;
-  infinite_fresh_Permutation :> Proper (@Permutation A ==> (=)) fresh;
+  infinite_fresh_Permutation :: Proper (@Permutation A ==> (=)) fresh;
 }.
 Global Hint Mode Infinite ! : typeclass_instances.
 Global Arguments infinite_fresh : simpl never.
diff --git a/stdpp/fin_map_dom.v b/stdpp/fin_map_dom.v
index f4e9ee310212cabc8c9931d14cfd955c195e1f17..dc42f862c4c58150b0add9c10f9c983e2d86c671 100644
--- a/stdpp/fin_map_dom.v
+++ b/stdpp/fin_map_dom.v
@@ -12,8 +12,8 @@ Class FinMapDom K M D `{∀ A, Dom (M A) D, FMap M,
     OMap M, Merge M, ∀ A, MapFold K A (M A), EqDecision K,
     ElemOf K D, Empty D, Singleton K D,
     Union D, Intersection D, Difference D} := {
-  finmap_dom_map :> FinMap K M;
-  finmap_dom_set :> Set_ K D;
+  finmap_dom_map :: FinMap K M;
+  finmap_dom_set :: Set_ K D;
   elem_of_dom {A} (m : M A) i : i ∈ dom m ↔ is_Some (m !! i)
 }.