From 9660dc7f88048c581c0256e3f782b899ae08d697 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 16 May 2022 10:54:09 +0200
Subject: [PATCH] add missing Global hints

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

diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index 0983259d..863a9625 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 c5c6445c..3c7e5e49 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 7f9b32ab..0f57c0f2 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 54b4823d..a833b4c4 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 45cdfad1..05e4d0c1 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 ab6c8800..36117c72 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 fdc0827a..0b5fd532 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 5c68ed5d..d784b0db 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 3b192a69..d208f940 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