Merge pull request #1620 from Alizter/fix-warnings

fix warnings

theories/Basics/Overture.v

@@ -595,6 +595,7 @@ Class IsTrunc (n : trunc_index) (A : Type) : Type :=
 
 (** We use the principle that we should always be doing typeclass resolution on truncation of non-equality types.  We try to change the hypotheses and goals so that they never mention something like [IsTrunc n (_ = _)] and instead say [IsTrunc (S n) _].  If you're evil enough that some of your paths [a = b] are n-truncated, but others are not, then you'll have to either reason manually or add some (local) hints with higher priority than the hint below, or generalize your equality type so that it's not a path anymore. *)
 
+#[global]
 Typeclasses Opaque IsTrunc. (* don't auto-unfold [IsTrunc] in typeclass search *)
 
 Arguments IsTrunc : simpl never. (* don't auto-unfold [IsTrunc] with [simpl] *)
@@ -733,6 +734,7 @@ Definition symmetric_neq {A} {x y : A} : x <> y -> y <> x
 Definition complement {A} (R : Relation A) : Relation A :=
   fun x y => ~ (R x y).
 
+#[global]
 Typeclasses Opaque complement.
 
 Class Irreflexive {A} (R : Relation A) :=
@@ -762,6 +764,7 @@ Register tt as core.True.I.
 (** A space is pointed if that space has a point. *)
 Class IsPointed (A : Type) := point : A.
 
+#[global]
 Typeclasses Transparent IsPointed.
 
 Arguments point A {_}.

theories/Basics/UniverseLevel.v

@@ -19,6 +19,7 @@ Definition lower2 {A B} (f : forall x : Lift A, Lift (B (lower x))) : forall x :
   := f.
 
 (** We make [lift] and [lower] opaque so that typeclass resolution doesn't pick up [isequiv_lift] as an instance of [IsEquiv idmap] and wreck havok. *)
+#[global]
 Typeclasses Opaque lift lower lift2 lower2.
 
 Global Instance isequiv_lift T : IsEquiv (@lift T)
@@ -83,6 +84,7 @@ Definition lower'2@{i i' j j'} {A : Type@{i}} {B : A -> Type@{i'}}
   := f.
 
 (** We make [lift] and [lower] opaque so that typeclass resolution doesn't pick up [isequiv_lift] as an instance of [IsEquiv idmap] and wreck havok. *)
+#[global]
 Typeclasses Opaque lift' lower' lift'2 lower'2.
 
 Definition isequiv_lift'@{i j} (T : Type@{i}) : IsEquiv (@lift'@{i j} T)

theories/Categories/Category/Morphisms.v

@@ -246,6 +246,7 @@ Class IsMonomorphism {C} {x y} (m : morphism C x y) :=
 (** We make [IsEpimorphism] and [IsMonomorphism] transparent to
     typeclass search so that we can infer things like [IsHProp]
     automatically. *)
+#[global]
 Typeclasses Transparent IsEpimorphism IsMonomorphism.
 
 Record Epimorphism {C} x y :=

theories/Categories/NatCategory.v

@@ -54,7 +54,8 @@ Module Export Core.
     Notation "9" := (nat_category 9) : category_scope.
   End NatCategoryCoreNotations.
 
-  Typeclasses Transparent nat_category.
+  #[export]
+Typeclasses Transparent nat_category.
   #[export]
   Hint Unfold nat_category : core.
   Arguments nat_category / .

theories/Classes/interfaces/canonical_names.v

@@ -54,7 +54,7 @@ Hint Extern 10 (Apart (sig _)) => apply @sig_apart : typeclass_instances.
 Class Cast A B := cast: A -> B.
 Arguments cast _ _ {Cast} _.
 Notation "' x" := (cast _ _ x) : mc_scope.
-Typeclasses Transparent Cast.
+#[global] Typeclasses Transparent Cast.
 
 (* Other canonically named relations/operations/constants: *)
 Class SgOp A := sg_op: A -> A -> A.
@@ -67,17 +67,17 @@ Class Negate A := negate: A -> A.
 Class DecRecip A := dec_recip: A -> A.
 Definition ApartZero R `{Zero R} `{Apart R} := sig (≶ zero).
 Class Recip A `{Apart A} `{Zero A} := recip: ApartZero A -> A.
-Typeclasses Transparent SgOp MonUnit Plus Mult Zero One Negate.
+#[global] Typeclasses Transparent SgOp MonUnit Plus Mult Zero One Negate.
 
 Class Meet A := meet: A -> A -> A.
 Class Join A := join: A -> A -> A.
 Class Top A := top: A.
 Class Bottom A := bottom: A.
-Typeclasses Transparent Meet Join Top Bottom.
+#[global] Typeclasses Transparent Meet Join Top Bottom.
 
 Class Le A := le: Relation A.
 Class Lt A := lt: Relation A.
-Typeclasses Transparent Le Lt.
+#[global] Typeclasses Transparent Le Lt.
 
 Definition NonNeg R `{Zero R} `{Le R} := sig (le zero).
 Definition Pos R `{Zero R} `{Lt R} := sig (lt zero).
@@ -241,7 +241,7 @@ Class RightInverse {A} {B} {C} (op : A -> B -> C) (inv : A -> B) (unit : C)
 Class Commutative {B A} (f : A -> A -> B) : Type
   := commutativity: forall x y, f x y = f y x.
 
-Typeclasses Transparent Commutative.
+#[global] Typeclasses Transparent Commutative.
 
 Class HeteroAssociative {A B C AB BC ABC}
   (fA_BC: A -> BC -> ABC) (fBC: B -> C -> BC)

theories/WildCat/Core.v

@@ -74,6 +74,7 @@ Arguments fmap {A B isgraph_A isgraph_B} F {is0functor_F a b} f : rename.
 Class Is2Graph (A : Type) `{IsGraph A}
   := isgraph_hom : forall (a b : A), IsGraph (a $-> b).
 Global Existing Instance isgraph_hom | 20.
+#[global]
 Typeclasses Transparent Is2Graph.
 
 (** ** Wild 1-categorical structures *)
@@ -397,6 +398,7 @@ Defined.
 Class Is3Graph (A : Type) `{Is2Graph A}
   := isgraph_hom_hom : forall (a b : A), Is2Graph (a $-> b).
 Global Existing Instance isgraph_hom_hom | 30.
+#[global]
 Typeclasses Transparent Is3Graph.
 
 (** *** Preservation of initial and terminal objects *)

theories/WildCat/Opposite.v

@@ -12,6 +12,7 @@ Definition op (A : Type) : Type := A.
 Notation "A ^op" := (op A).
 
 (** This stops typeclass search from trying to unfold op. *)
+#[global]
 Typeclasses Opaque op.
 
 Section Op.