From 8574b623a74b52b005035a24fdf998fafa2ac8bc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 1 May 2023 21:40:10 +0200
Subject: [PATCH] Add `Global` to `Typeclasses Opaque`/`Typeclasses
 Transparent`.

---
 _CoqProject                |  2 --
 stdpp/base.v               |  8 ++++----
 stdpp/boolset.v            |  2 +-
 stdpp/coGset.v             |  4 ++--
 stdpp/fin_maps.v           |  6 +++---
 stdpp/fin_sets.v           | 14 +++++++-------
 stdpp/gmap.v               |  2 +-
 stdpp/gmultiset.v          |  8 ++++----
 stdpp/hashset.v            |  2 +-
 stdpp/lexico.v             |  2 +-
 stdpp/namespaces.v         |  2 +-
 stdpp/numbers.v            | 20 ++++++++++----------
 stdpp/option.v             |  2 +-
 stdpp/sets.v               |  4 ++--
 stdpp/telescopes.v         |  2 +-
 stdpp_unstable/bitvector.v |  2 +-
 16 files changed, 40 insertions(+), 42 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index d01ced3e..2b206438 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 45e5a5f8..52068077 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 7cddb6af..5e1b5e1d 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 57590d44..2b3e4c94 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 9e7f68a4..12eb7e76 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 740d79a2..527b6291 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 fe1cbc57..fcb2352b 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 d71a62cd..40b13c63 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 72d86530..1a8d6275 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 59a387b4..8f551c11 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 be47aa69..b19428e7 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 746cfe27..ee00877e 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 65a2a9b5..a5dbfda2 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 2dd1a202..2465d89a 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 33f44ad9..ce374c3e 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 5908a2cb..38495bfb 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
-- 
GitLab