diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 0a9e4471764ebe63d7958b34c03d6c1e6b5d7f13..7ad13e5a583d9253a5de516b7556fb9ccab5471c 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -66,7 +66,7 @@ Section definitions.
          ∗ ⌜heap_freeable_rel σ hF⌝)%I.
 End definitions.
 
-Typeclasses Opaque heap_mapsto heap_freeable heap_mapsto_vec.
+Global Typeclasses Opaque heap_mapsto heap_freeable heap_mapsto_vec.
 Global Instance: Params (@heap_mapsto) 4 := {}.
 Global Instance: Params (@heap_freeable) 5 := {}.
 
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 8c897d6795c8bcf6a6dd24151edd392d12a9446e..63d8295c17ec4b625bbc154573fadcfd63ca8e8f 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -669,4 +669,4 @@ Section arc.
   Qed.
 End arc.
 
-Typeclasses Opaque is_arc arc_tok weak_tok.
+Global Typeclasses Opaque is_arc arc_tok weak_tok.
diff --git a/theories/lang/lib/lock.v b/theories/lang/lib/lock.v
index e7987116a2c24ea807a2ddfaf7c54e88577ced46..f1bdd6ecf232db65192ee89bed926996b715996a 100644
--- a/theories/lang/lib/lock.v
+++ b/theories/lang/lib/lock.v
@@ -109,4 +109,4 @@ Section proof.
   Qed.
 End proof.
 
-Typeclasses Opaque lock_proto.
+Global Typeclasses Opaque lock_proto.
diff --git a/theories/lang/lib/spawn.v b/theories/lang/lib/spawn.v
index 2b120455906f2de2139a45388dcbc9e9bb284e73..b176e3f3c5e6c7f71dede8b7893e688bbbc9e020 100644
--- a/theories/lang/lib/spawn.v
+++ b/theories/lang/lib/spawn.v
@@ -125,4 +125,4 @@ 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 020323fa33392d825cd84230d8b79f050f050474..8f67ef3f8077abe037460a1dc15bdc87accb0eaf 100644
--- a/theories/lifetime/at_borrow.v
+++ b/theories/lifetime/at_borrow.v
@@ -103,4 +103,4 @@ Lemma at_bor_acc_lftN `{!invGS Σ, !lftGS Σ userE} (P : iProp Σ) E κ :
              [†κ] ∗ |={E∖↑lftN,E}=> True.
 Proof. intros. by rewrite (at_bor_acc _ lftN) // difference_twice_L. Qed.
 
-Typeclasses Opaque at_bor.
+Global Typeclasses Opaque at_bor.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index bfa1faf19e848f4a863d2c65d4469f262251ffe0..761b30537bfd2289fc7d3f27d629465842658664 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -168,4 +168,4 @@ Proof.
     iDestruct (lft_tok_dead with "Hκ' H†'") as "[]".
 Qed.
 
-Typeclasses Opaque frac_bor.
+Global Typeclasses Opaque frac_bor.
diff --git a/theories/lifetime/meta.v b/theories/lifetime/meta.v
index 80ebbcc790f5f79cd1b6bddc58e10ddd5e67f992..b9e4f8af89233797307c152eda21b77b22ee9a33 100644
--- a/theories/lifetime/meta.v
+++ b/theories/lifetime/meta.v
@@ -64,4 +64,4 @@ Section lft_meta.
   Qed.
 End lft_meta.
 
-Typeclasses Opaque lft_meta.
+Global Typeclasses Opaque lft_meta.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 418e1a9159fbb5b931540acf618b352996cf9ef7..a278956cfb57f526bf58010ec225ef2c184441c6 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -219,7 +219,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 144c079c12528f3a47f5aab7baa23f1590d149dc..4a1f37aed5fa106a0e08990577c2faa67cc80be9 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.