From b949eceab3ec0e5d974ebe8b5988042072cde312 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 11 May 2022 16:13:52 +0200
Subject: [PATCH] fix deprecation warnings

---
 theories/lang/heap.v                  | 2 +-
 theories/lang/lib/arc.v               | 2 +-
 theories/lang/lib/lock.v              | 2 +-
 theories/lang/lib/spawn.v             | 2 +-
 theories/lifetime/at_borrow.v         | 2 +-
 theories/lifetime/frac_borrow.v       | 2 +-
 theories/lifetime/meta.v              | 2 +-
 theories/lifetime/model/definitions.v | 2 +-
 theories/lifetime/na_borrow.v         | 2 +-
 9 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 0a9e4471..7ad13e5a 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 8c897d67..63d8295c 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 e7987116..f1bdd6ec 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 2b120455..b176e3f3 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 020323fa..8f67ef3f 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 bfa1faf1..761b3053 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 80ebbcc7..b9e4f8af 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 418e1a91..a278956c 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 144c079c..4a1f37ae 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.
-- 
GitLab