diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index 0983259dbdc7cfc8d7aaebda96e7f11b01c6fa0d..863a962560516d3c824a94732f1c9016dbf0abba 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -269,7 +269,7 @@ Section ArcInv.
 
 End ArcInv.
 
-Typeclasses Opaque StrongTok WeakTok StrMoves StrDowns WkUps.
+Global Typeclasses Opaque StrongTok WeakTok StrMoves StrDowns WkUps.
 
 Section arc.
   (* P1 is the thing that is shared by strong reference owners (in practice,
@@ -2756,5 +2756,5 @@ Section arc.
   Qed.
 End arc.
 
-Typeclasses Opaque StrMoveCertS StrDownCertS WkUpCertS.
-Typeclasses Opaque is_arc strong_arc weak_arc.
+Global Typeclasses Opaque StrMoveCertS StrDownCertS WkUpCertS.
+Global Typeclasses Opaque is_arc strong_arc weak_arc.
diff --git a/theories/lang/lock.v b/theories/lang/lock.v
index c5c6445c14f513ad3e1e2fa171bf54019ee53ed2..3c7e5e4939b9cf7f3f2f96d9547aeb3086d043a2 100644
--- a/theories/lang/lock.v
+++ b/theories/lang/lock.v
@@ -172,4 +172,4 @@ Section proof.
   Qed.
 End proof.
 
-Typeclasses Opaque lock_proto.
+Global Typeclasses Opaque lock_proto.
diff --git a/theories/lang/spawn.v b/theories/lang/spawn.v
index 7f9b32ab711ec5849affefb45ca058b95594a193..0f57c0f21d1b170dda061400671d3b8843cef5d7 100644
--- a/theories/lang/spawn.v
+++ b/theories/lang/spawn.v
@@ -226,4 +226,4 @@ Proof.
 Qed.
 End proof.
 
-Typeclasses Opaque finish_handle join_handle.
+Global Typeclasses Opaque finish_handle join_handle.
diff --git a/theories/lifetime/at_borrow.v b/theories/lifetime/at_borrow.v
index 54b4823d0ef6666dd9e293984db8987be412eeea..a833b4c49331c439e2a1ab3e7ea5d839eac7777b 100644
--- a/theories/lifetime/at_borrow.v
+++ b/theories/lifetime/at_borrow.v
@@ -72,4 +72,4 @@ Section atomic_bors.
   Qed.
 End atomic_bors.
 
-Typeclasses Opaque at_bor.
+Global Typeclasses Opaque at_bor.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 45cdfad1f2a84d52c7fef0019fc72da629f58f1f..05e4d0c1a20612f4b51f6477890c3b3a748e69a8 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -196,4 +196,4 @@ Section frac_bor.
   Qed.
 End frac_bor.
 
-Typeclasses Opaque frac_bor.
+Global Typeclasses Opaque frac_bor.
diff --git a/theories/lifetime/meta.v b/theories/lifetime/meta.v
index ab6c88001de84c92a596a128cc37d7143bc9122c..36117c724d3eb2ff47ffb0acf2e1c088159aff09 100644
--- a/theories/lifetime/meta.v
+++ b/theories/lifetime/meta.v
@@ -65,4 +65,4 @@ Section lft_meta.
   Qed.
 End lft_meta.
 
-Typeclasses Opaque lft_meta.
+Global Typeclasses Opaque lft_meta.
diff --git a/theories/lifetime/model/boxes.v b/theories/lifetime/model/boxes.v
index fdc0827a50f9f5c59c2782598990a3e1aa58f3d0..0b5fd532888c051d92ff7ea415ea379073b186e0 100644
--- a/theories/lifetime/model/boxes.v
+++ b/theories/lifetime/model/boxes.v
@@ -289,4 +289,4 @@ Proof.
 Qed.
 End box.
 
-Typeclasses Opaque slice box.
+Global Typeclasses Opaque slice box.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 5c68ed5d88dcfbb6362ae37cdf01e4fef17a42f0..d784b0db397897fac9a862fa3dd194b95a20f233 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -232,7 +232,7 @@ Infix "⊑" := lft_incl (at level 70) : bi_scope.
 (* TODO: Making all these things opaque is rather annoying, we should
    find a way to avoid it, or *at least*, to avoid having to manually unfold
    this because iDestruct et al don't look through these names any more. *)
-Typeclasses Opaque lft_tok lft_dead bor_cnt lft_bor_alive lft_bor_dead
+Global Typeclasses Opaque lft_tok lft_dead bor_cnt lft_bor_alive lft_bor_dead
   lft_inh lft_inv_alive lft_vs_inv lft_vs lft_inv_dead lft_inv lft_incl
   idx_bor_own idx_bor raw_bor bor.
 
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index 3b192a69e7da4d4c9e6b8810374b6b5a28994bda..d208f940ee24ea8c517faeaca36deb093d88d344 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -63,4 +63,4 @@ Section na_bor.
   Qed.
 End na_bor.
 
-Typeclasses Opaque na_bor.
+Global Typeclasses Opaque na_bor.