diff --git a/_CoqProject b/_CoqProject
index d01ced3e2f877bf794702b5c3e64e29d90bad7ad..2b206438b9f12910a380eb94b9dfe59ced3871ad 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.15.
--arg -w -arg -deprecated-typeclasses-transparency-without-locality
 # Fixing this one requires Coq 8.17
 -arg -w -arg -future-coercion-class-field
 
diff --git a/stdpp/base.v b/stdpp/base.v
index 45e5a5f87df22c93a78b4f764e819957ba8c136a..52068077f8da11ce4ef9242fa8a1aa4c3cc8f25b 100644
--- a/stdpp/base.v
+++ b/stdpp/base.v
@@ -109,7 +109,7 @@ Global Hint Extern 0 (TCIf _ _ _) =>
 (** The constant [tc_opaque] is used to make definitions opaque for just type
 class search. Note that [simpl] is set up to always unfold [tc_opaque]. *)
 Definition tc_opaque {A} (x : A) : A := x.
-Typeclasses Opaque tc_opaque.
+Global Typeclasses Opaque tc_opaque.
 Global Arguments tc_opaque {_} _ /.
 
 (** Below we define type class versions of the common logical operators. It is
@@ -602,7 +602,7 @@ Global Arguments id _ _ / : assert.
 Global Arguments compose _ _ _ _ _ _ / : assert.
 Global Arguments flip _ _ _ _ _ _ / : assert.
 Global Arguments const _ _ _ _ / : assert.
-Typeclasses Transparent id compose flip const.
+Global Typeclasses Transparent id compose flip const.
 
 Definition fun_map {A A' B B'} (f: A' → A) (g: B → B') (h : A → B) : A' → B' :=
   g ∘ h ∘ f.
@@ -859,7 +859,7 @@ Section prod_setoid.
             (≡@{A*B*C*D}) ==> (≡@{E})) uncurry4 := _.
 End prod_setoid.
 
-Typeclasses Opaque prod_equiv.
+Global Typeclasses Opaque prod_equiv.
 
 Global Instance prod_leibniz `{LeibnizEquiv A, LeibnizEquiv B} :
   LeibnizEquiv (A * B).
@@ -918,7 +918,7 @@ Global Instance inl_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inl
 Global Instance inr_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inr A B) := _.
 Global Instance inl_equiv_inj `{Equiv A, Equiv B} : Inj (≡) (≡) (@inl A B) := _.
 Global Instance inr_equiv_inj `{Equiv A, Equiv B} : Inj (≡) (≡) (@inr A B) := _.
-Typeclasses Opaque sum_equiv.
+Global Typeclasses Opaque sum_equiv.
 
 (** ** Option *)
 Global Instance option_inhabited {A} : Inhabited (option A) := populate None.
diff --git a/stdpp/boolset.v b/stdpp/boolset.v
index 7cddb6afa3c5f7f323cfe574917bb37f67454867..5e1b5e1dd3e6fd1f79b2d4ebdfab4450d856fc5b 100644
--- a/stdpp/boolset.v
+++ b/stdpp/boolset.v
@@ -31,6 +31,6 @@ Qed.
 Global Instance boolset_elem_of_dec {A} : RelDecision (∈@{boolset A}).
 Proof. refine (λ x X, cast_if (decide (boolset_car X x))); done. Defined.
 
-Typeclasses Opaque boolset_elem_of.
+Global Typeclasses Opaque boolset_elem_of.
 Global Opaque boolset_empty boolset_singleton boolset_union
   boolset_intersection boolset_difference.
diff --git a/stdpp/coGset.v b/stdpp/coGset.v
index 57590d44c03fbf4206fbf3c5a582a6bf7a099ed6..2b3e4c94d50fb7f5a79fade702f3dac195a160a4 100644
--- a/stdpp/coGset.v
+++ b/stdpp/coGset.v
@@ -192,5 +192,5 @@ Lemma elem_of_coGset_to_top_set `{Countable A, TopSet A C} X x :
   x ∈@{C} coGset_to_top_set X ↔ x ∈ X.
 Proof. destruct X; set_solver. Qed.
 
-Typeclasses Opaque coGset_elem_of coGset_empty coGset_top coGset_singleton.
-Typeclasses Opaque coGset_union coGset_intersection coGset_difference.
+Global Typeclasses Opaque coGset_elem_of coGset_empty coGset_top coGset_singleton.
+Global Typeclasses Opaque coGset_union coGset_intersection coGset_difference.
diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index 9e7f68a42bde9ee8ae53f04e5a5fa2b78543f140..12eb7e76688efffa65ff60b1a012b84d5d74771c 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -177,7 +177,7 @@ Fixpoint map_seqZ `{Insert Z A M, Empty M} (start : Z) (xs : list A) : M :=
 
 Global Instance map_lookup_total `{!Lookup K A (M A), !Inhabited A} :
   LookupTotal K A (M A) | 20 := λ i m, default inhabitant (m !! i).
-Typeclasses Opaque map_lookup_total.
+Global Typeclasses Opaque map_lookup_total.
 
 (** Given a finite map [m : M] with keys [K] and values [A], the image [map_img m]
 gives a finite set containing with the values [A] of [m]. The type of [map_img]
@@ -185,7 +185,7 @@ is generic to support different map and set implementations. A possible instance
 is [SA:=gset A]. *)
 Definition map_img `{FinMapToList K A M,
   Singleton A SA, Empty SA, Union SA} : M → SA := map_to_set (λ _ x, x).
-Typeclasses Opaque map_img.
+Global Typeclasses Opaque map_img.
 
 (** Given a finite map [m] with keys [K] and values [A], the preimage
 [map_preimg m] gives a finite map with keys [A] and values being sets of [K].
@@ -196,7 +196,7 @@ Definition map_preimg `{FinMapToList K A MKA, Empty MASK,
     PartialAlter A SK MASK, Empty SK, Singleton K SK, Union SK}
     (m : MKA) : MASK :=
   map_fold (λ i, partial_alter (λ mX, Some $ {[ i ]} ∪ default ∅ mX)) ∅ m.
-Typeclasses Opaque map_preimg.
+Global Typeclasses Opaque map_preimg.
 
 (** * Theorems *)
 Section theorems.
diff --git a/stdpp/fin_sets.v b/stdpp/fin_sets.v
index 740d79a2e805395fec6000750469f55ebdfe3901..527b6291bae4f7840c662a6e4b4b370410d91857 100644
--- a/stdpp/fin_sets.v
+++ b/stdpp/fin_sets.v
@@ -10,38 +10,38 @@ Set Default Proof Using "Type*".
 
 (** Operations *)
 Global Instance set_size `{Elements A C} : Size C := length ∘ elements.
-Typeclasses Opaque set_size.
+Global Typeclasses Opaque set_size.
 
 Definition set_fold `{Elements A C} {B}
   (f : A → B → B) (b : B) : C → B := foldr f b ∘ elements.
-Typeclasses Opaque set_fold.
+Global Typeclasses Opaque set_fold.
 
 Global Instance set_filter
     `{Elements A C, Empty C, Singleton A C, Union C} : Filter A C := λ P _ X,
   list_to_set (filter P (elements X)).
-Typeclasses Opaque set_filter.
+Global Typeclasses Opaque set_filter.
 
 Definition set_map `{Elements A C, Singleton B D, Empty D, Union D}
     (f : A → B) (X : C) : D :=
   list_to_set (f <$> elements X).
-Typeclasses Opaque set_map.
+Global Typeclasses Opaque set_map.
 Global Instance: Params (@set_map) 8 := {}.
 
 Definition set_bind `{Elements A SA, Empty SB, Union SB}
     (f : A → SB) (X : SA) : SB :=
   ⋃ (f <$> elements X).
-Typeclasses Opaque set_bind.
+Global Typeclasses Opaque set_bind.
 Global Instance: Params (@set_bind) 6 := {}.
 
 Definition set_omap `{Elements A C, Singleton B D, Empty D, Union D}
     (f : A → option B) (X : C) : D :=
   list_to_set (omap f (elements X)).
-Typeclasses Opaque set_omap.
+Global Typeclasses Opaque set_omap.
 Global Instance: Params (@set_omap) 8 := {}.
 
 Global Instance set_fresh `{Elements A C, Fresh A (list A)} : Fresh A C :=
   fresh ∘ elements.
-Typeclasses Opaque set_fresh.
+Global Typeclasses Opaque set_fresh.
 
 (** We generalize the [fresh] operation on sets to generate lists of fresh
 elements w.r.t. a set [X]. *)
diff --git a/stdpp/gmap.v b/stdpp/gmap.v
index fe1cbc57a8d8538b787da1552fa85e31ecedcab6..fcb2352b75b4934a076c2a61c588cd402defc928 100644
--- a/stdpp/gmap.v
+++ b/stdpp/gmap.v
@@ -367,4 +367,4 @@ Section gset.
   Qed.
 End gset.
 
-Typeclasses Opaque gset.
+Global Typeclasses Opaque gset.
diff --git a/stdpp/gmultiset.v b/stdpp/gmultiset.v
index d71a62cdd5269eb44a6c55f91dbd40ca4695005d..40b13c6340762e4612a1fa0a602b0668d6d52eba 100644
--- a/stdpp/gmultiset.v
+++ b/stdpp/gmultiset.v
@@ -62,10 +62,10 @@ Section definitions.
     let (X) := X in dom X.
 End definitions.
 
-Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq.
-Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty.
-Typeclasses Opaque gmultiset_singleton gmultiset_union gmultiset_difference.
-Typeclasses Opaque gmultiset_scalar_mul gmultiset_dom.
+Global Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq.
+Global Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty.
+Global Typeclasses Opaque gmultiset_singleton gmultiset_union gmultiset_difference.
+Global Typeclasses Opaque gmultiset_scalar_mul gmultiset_dom.
 
 Section basic_lemmas.
   Context `{Countable A}.
diff --git a/stdpp/hashset.v b/stdpp/hashset.v
index 72d865301af8f094832ef5b41a817c57dd3aff95..1a8d6275eab335eef0949e2cfd56c6591d158eac 100644
--- a/stdpp/hashset.v
+++ b/stdpp/hashset.v
@@ -116,7 +116,7 @@ Proof.
 Qed.
 End hashset.
 
-Typeclasses Opaque hashset_elem_of.
+Global Typeclasses Opaque hashset_elem_of.
 
 Section remove_duplicates.
 Context `{EqDecision A} (hash : A → Z).
diff --git a/stdpp/lexico.v b/stdpp/lexico.v
index 59a387b45738b4673a9fa9790694105f5cb7a076..8f551c113299268aadaa82c9886c0b91be4c250e 100644
--- a/stdpp/lexico.v
+++ b/stdpp/lexico.v
@@ -19,7 +19,7 @@ Global Instance bool_lexico : Lexico bool := λ b1 b2,
 Global Instance nat_lexico : Lexico nat := (<).
 Global Instance N_lexico : Lexico N := (<)%N.
 Global Instance Z_lexico : Lexico Z := (<)%Z.
-Typeclasses Opaque bool_lexico nat_lexico N_lexico Z_lexico.
+Global Typeclasses Opaque bool_lexico nat_lexico N_lexico Z_lexico.
 Global Instance list_lexico `{Lexico A} : Lexico (list A) :=
   fix go l1 l2 :=
   let _ : Lexico (list A) := @go in
diff --git a/stdpp/namespaces.v b/stdpp/namespaces.v
index be47aa69945eec961de5ebca607caf5e7c86bc5f..b19428e7103c318e4023c383817079d272aed6df 100644
--- a/stdpp/namespaces.v
+++ b/stdpp/namespaces.v
@@ -4,7 +4,7 @@ From stdpp Require Import options.
 Definition namespace := list positive.
 Global Instance namespace_eq_dec : EqDecision namespace := _.
 Global Instance namespace_countable : Countable namespace := _.
-Typeclasses Opaque namespace.
+Global Typeclasses Opaque namespace.
 
 Definition nroot : namespace := nil.
 
diff --git a/stdpp/numbers.v b/stdpp/numbers.v
index 746cfe27804f601db01702f05f7fa271d31a0e6d..ee00877e9ee2323fef6ce58fdcbffd1ea949ae94 100644
--- a/stdpp/numbers.v
+++ b/stdpp/numbers.v
@@ -36,7 +36,7 @@ Global Arguments Nat.max : simpl nomatch.
 
 (** We do not make [Nat.lt] since it is an alias for [lt], which contains the
 actual definition that we want to make opaque. *)
-Typeclasses Opaque lt.
+Global Typeclasses Opaque lt.
 
 Reserved Notation "x ≤ y ≤ z" (at level 70, y at next level).
 Reserved Notation "x ≤ y < z" (at level 70, y at next level).
@@ -172,8 +172,8 @@ End Nat.
 (** * Notations and properties of [positive] *)
 Local Open Scope positive_scope.
 
-Typeclasses Opaque Pos.le.
-Typeclasses Opaque Pos.lt.
+Global Typeclasses Opaque Pos.le.
+Global Typeclasses Opaque Pos.lt.
 
 Infix "≤" := Pos.le : positive_scope.
 Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z) : positive_scope.
@@ -365,8 +365,8 @@ Local Close Scope positive_scope.
 (** * Notations and properties of [N] *)
 Local Open Scope N_scope.
 
-Typeclasses Opaque N.le.
-Typeclasses Opaque N.lt.
+Global Typeclasses Opaque N.le.
+Global Typeclasses Opaque N.lt.
 
 Infix "≤" := N.le : N_scope.
 Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z)%N : N_scope.
@@ -446,8 +446,8 @@ Local Close Scope N_scope.
 (** * Notations and properties of [Z] *)
 Local Open Scope Z_scope.
 
-Typeclasses Opaque Z.le.
-Typeclasses Opaque Z.lt.
+Global Typeclasses Opaque Z.le.
+Global Typeclasses Opaque Z.lt.
 
 Infix "≤" := Z.le : Z_scope.
 Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z) : Z_scope.
@@ -724,8 +724,8 @@ End N2Z.
 (* Add others here. *)
 
 (** * Notations and properties of [Qc] *)
-Typeclasses Opaque Qcle.
-Typeclasses Opaque Qclt.
+Global Typeclasses Opaque Qcle.
+Global Typeclasses Opaque Qclt.
 
 Local Open Scope Qc_scope.
 Delimit Scope Qc_scope with Qc.
@@ -946,7 +946,7 @@ Module Qp.
   Global Arguments inv : simpl never.
 
   Definition div (p q : Qp) : Qp := mul p (inv q).
-  Typeclasses Opaque div.
+  Global Typeclasses Opaque div.
   Global Arguments div : simpl never.
 
   Definition le (p q : Qp) : Prop :=
diff --git a/stdpp/option.v b/stdpp/option.v
index 65a2a9b56a436df7d1e0fd57fd349fcaa02f7805..a5dbfda201fb5c1df9d7b514c95b56efde421183 100644
--- a/stdpp/option.v
+++ b/stdpp/option.v
@@ -148,7 +148,7 @@ Section setoids.
   Proof. destruct 3; simpl; auto. Qed.
 End setoids.
 
-Typeclasses Opaque option_equiv.
+Global Typeclasses Opaque option_equiv.
 
 (** Equality on [option] is decidable. *)
 Global Instance option_eq_None_dec {A} (mx : option A) : Decision (mx = None) :=
diff --git a/stdpp/sets.v b/stdpp/sets.v
index 2dd1a20210cb374d225efef529106fdb43491640..2465d89af44e404e0a091c8d556fe063f02160aa 100644
--- a/stdpp/sets.v
+++ b/stdpp/sets.v
@@ -17,7 +17,7 @@ Global Instance set_subseteq_instance `{ElemOf A C} : SubsetEq C | 20 := λ X Y,
   ∀ x, x ∈ X → x ∈ Y.
 Global Instance set_disjoint_instance `{ElemOf A C} : Disjoint C | 20 := λ X Y,
   ∀ x, x ∈ X → x ∈ Y → False.
-Typeclasses Opaque set_equiv_instance set_subseteq_instance set_disjoint_instance.
+Global Typeclasses Opaque set_equiv_instance set_subseteq_instance set_disjoint_instance.
 
 (** * Setoids *)
 Section setoids_simple.
@@ -1333,7 +1333,7 @@ End set_seq.
 Definition minimal `{ElemOf A C} (R : relation A) (x : A) (X : C) : Prop :=
   ∀ y, y ∈ X → R y x → R x y.
 Global Instance: Params (@minimal) 5 := {}.
-Typeclasses Opaque minimal.
+Global Typeclasses Opaque minimal.
 
 Section minimal.
   Context `{SemiSet A C} {R : relation A}.
diff --git a/stdpp/telescopes.v b/stdpp/telescopes.v
index 33f44ad92b627728e4a0f0abe657ce3e2054c1f5..ce374c3ec6dd8e540ede99c270e131c85f25c335 100644
--- a/stdpp/telescopes.v
+++ b/stdpp/telescopes.v
@@ -229,7 +229,7 @@ Proof.
 Qed.
 
 (* Teach typeclass resolution how to make progress on these binders *)
-Typeclasses Opaque tforall texist.
+Global Typeclasses Opaque tforall texist.
 Global Hint Extern 1 (tforall _) =>
   progress cbn [tforall tele_fold tele_bind tele_app] : typeclass_instances.
 Global Hint Extern 1 (texist _) =>
diff --git a/stdpp_unstable/bitvector.v b/stdpp_unstable/bitvector.v
index 5908a2cbc658ef6c434ec9e505e45d3b559e4002..38495bfbd811eac40c6ddfc789bff1a1b6e4d820 100644
--- a/stdpp_unstable/bitvector.v
+++ b/stdpp_unstable/bitvector.v
@@ -251,7 +251,7 @@ Proof. unfold BvWf. apply _. Qed.
 Global Instance bv_wf_dec n z : Decision (BvWf n z).
 Proof. unfold BvWf. apply _. Defined.
 
-Typeclasses Opaque BvWf.
+Global Typeclasses Opaque BvWf.
 
 Ltac solve_BvWf :=
   lazymatch goal with