From bacff978f07005149cd50ccba5144452298e660f Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Sat, 7 May 2022 20:45:31 +0100
Subject: [PATCH 1/4] Fix warning about legacy `:>` syntax for classes

---
 theories/Categories/Functor/Attributes.v      |   7 +-
 .../Classes/interfaces/abstract_algebra.v     | 187 ++++++++++++------
 theories/Classes/interfaces/canonical_names.v |  29 ++-
 theories/Classes/interfaces/integers.v        |   7 +-
 theories/Classes/interfaces/naturals.v        |   7 +-
 theories/Classes/interfaces/orders.v          |  97 +++++----
 theories/Classes/interfaces/rationals.v       |   7 +-
 theories/Classes/theory/premetric.v           |  19 +-
 theories/Diagrams/DDiagram.v                  |   3 +-
 theories/Homotopy/CayleyDickson.v             |  51 +++--
 theories/Homotopy/HSpace.v                    |   7 +-
 theories/Sets/Ordinals.v                      |  20 +-
 12 files changed, 286 insertions(+), 155 deletions(-)

diff --git a/theories/Categories/Functor/Attributes.v b/theories/Categories/Functor/Attributes.v
index f972fc30bd1..e7e2d710298 100644
--- a/theories/Categories/Functor/Attributes.v
+++ b/theories/Categories/Functor/Attributes.v
@@ -143,5 +143,8 @@ Class IsEssentiallySurjective A B (F : Functor A B)
     We say [F] is a _weak equivalence_ if it is fully faithful and
     essentially surjective. *)
 Class IsWeakEquivalence `{Funext} A B (F : Functor A B)
-  := { is_fully_faithful__is_weak_equivalence :> IsFullyFaithful F;
-       is_essentially_surjective__is_weak_equivalence :> IsEssentiallySurjective F }.
+  := { is_fully_faithful__is_weak_equivalence : IsFullyFaithful F;
+       is_essentially_surjective__is_weak_equivalence : IsEssentiallySurjective F }.
+#[global] Existing Instances
+  is_fully_faithful__is_weak_equivalence
+  is_essentially_surjective__is_weak_equivalence.
diff --git a/theories/Classes/interfaces/abstract_algebra.v b/theories/Classes/interfaces/abstract_algebra.v
index 85a18daf91b..61793f0a400 100644
--- a/theories/Classes/interfaces/abstract_algebra.v
+++ b/theories/Classes/interfaces/abstract_algebra.v
@@ -9,9 +9,10 @@ For various structures we omit declaration of substructures. For example, if we
 say:
 
 Class Setoid_Morphism :=
-  { setoidmor_a :> Setoid A
-  ; setoidmor_b :> Setoid B
-  ; sm_proper :> Proper ((=) ==> (=)) f }.
+  { setoidmor_a : Setoid A
+  ; setoidmor_b : Setoid B
+  ; sm_proper : Proper ((=) ==> (=)) f }.
+#[global] Existing Instances setoidmor_a setoidmor_b sm_proper.
 
 then each time a Setoid instance is required, Coq will try to prove that a
 Setoid_Morphism exists. This obviously results in an enormous blow-up of the
@@ -25,11 +26,16 @@ Setoid_Morphism as a substructure, setoid rewriting will become horribly slow.
 (* An unbundled variant of the former CoRN CSetoid. We do not 
   include a proof that A is a Setoid because it can be derived. *)
 Class IsApart A {Aap : Apart A} : Type :=
-  { apart_set :> IsHSet A
-  ; apart_mere :> is_mere_relation _ apart
-  ; apart_symmetric :> Symmetric (≶)
-  ; apart_cotrans :> CoTransitive (≶)
+  { apart_set : IsHSet A
+  ; apart_mere : is_mere_relation _ apart
+  ; apart_symmetric : Symmetric (≶)
+  ; apart_cotrans : CoTransitive (≶)
   ; tight_apart : forall x y, ~(x ≶ y) <-> x = y }.
+#[global] Existing Instances
+  apart_set
+  apart_mere
+  apart_symmetric
+  apart_cotrans.
 
 Global Instance apart_irrefl `{IsApart A} : Irreflexive (≶).
 Proof.
@@ -71,55 +77,75 @@ Section upper_classes.
   Local Open Scope mc_mult_scope.
 
   Class IsSemiGroup {Aop: SgOp A} :=
-    { sg_set :> IsHSet A
-    ; sg_ass :> Associative (.*.) }.
+    { sg_set : IsHSet A
+    ; sg_ass : Associative (.*.) }.
+    #[global] Existing Instances sg_set sg_ass.
 
   Class IsCommutativeSemiGroup {Aop : SgOp A} :=
-    { comsg_sg :> @IsSemiGroup (.*.)
-    ; comsg_comm :> Commutative (.*.) }.
+    { comsg_sg : @IsSemiGroup (.*.)
+    ; comsg_comm : Commutative (.*.) }.
+  #[global] Existing Instances comsg_sg comsg_comm.
 
   Class IsSemiLattice {Aop : SgOp A} :=
-    { semilattice_sg :> @IsCommutativeSemiGroup (.*.)
-    ; semilattice_idempotent :> BinaryIdempotent (.*.)}.
+    { semilattice_sg : @IsCommutativeSemiGroup (.*.)
+    ; semilattice_idempotent : BinaryIdempotent (.*.)}.
+  #[global] Existing Instances semilattice_sg semilattice_idempotent.
 
   Class IsMonoid {Aop : SgOp A} {Aunit : MonUnit A} :=
-    { monoid_semigroup :> IsSemiGroup
-    ; monoid_left_id :> LeftIdentity (.*.) mon_unit
-    ; monoid_right_id :> RightIdentity (.*.) mon_unit }.
+    { monoid_semigroup : IsSemiGroup
+    ; monoid_left_id : LeftIdentity (.*.) mon_unit
+    ; monoid_right_id : RightIdentity (.*.) mon_unit }.
+  #[global] Existing Instances
+    monoid_semigroup
+    monoid_left_id
+    monoid_right_id.
 
   Class IsCommutativeMonoid {Aop : SgOp A} {Aunit : MonUnit A} :=
-    { commonoid_mon :> @IsMonoid (.*.) Aunit
-    ; commonoid_commutative :> Commutative (.*.) }.
+    { commonoid_mon : @IsMonoid (.*.) Aunit
+    ; commonoid_commutative : Commutative (.*.) }.
+  #[global] Existing Instances
+    commonoid_mon
+    commonoid_commutative.
 
   Class IsGroup {Aop : SgOp A} {Aunit : MonUnit A} {Anegate : Negate A} :=
-    { group_monoid :> @IsMonoid (.*.) Aunit
-    ; negate_l :> LeftInverse (.*.) (-) mon_unit
-    ; negate_r :> RightInverse (.*.) (-) mon_unit }.
+    { group_monoid : @IsMonoid (.*.) Aunit
+    ; negate_l : LeftInverse (.*.) (-) mon_unit
+    ; negate_r : RightInverse (.*.) (-) mon_unit }.
+  #[global] Existing Instances 
+    group_monoid
+    negate_l
+    negate_r.
 
   Class IsBoundedSemiLattice {Aop : SgOp A} {Aunit : MonUnit A} :=
-    { bounded_semilattice_mon :> @IsCommutativeMonoid (.*.) Aunit
-    ; bounded_semilattice_idempotent :> BinaryIdempotent (.*.)}.
+    { bounded_semilattice_mon : @IsCommutativeMonoid (.*.) Aunit
+    ; bounded_semilattice_idempotent : BinaryIdempotent (.*.)}.
+  #[global] Existing Instances
+    bounded_semilattice_mon
+    bounded_semilattice_idempotent.
 
   Class IsAbGroup {Aop : SgOp A} {Aunit : MonUnit A} {Anegate : Negate A} :=
-    { abgroup_group :> @IsGroup (.*.) Aunit Anegate
-    ; abgroup_commutative :> Commutative (.*.) }.
+    { abgroup_group : @IsGroup (.*.) Aunit Anegate
+    ; abgroup_commutative : Commutative (.*.) }.
+  #[global] Existing Instances abgroup_group abgroup_commutative.
 
   Close Scope mc_mult_scope.
 
   Context {Aplus : Plus A} {Amult : Mult A} {Azero : Zero A} {Aone : One A}.
 
   Class IsSemiRing :=
-    { semiplus_monoid :> @IsCommutativeMonoid plus_is_sg_op zero_is_mon_unit
-    ; semimult_monoid :> @IsCommutativeMonoid mult_is_sg_op one_is_mon_unit
-    ; semiring_distr :> LeftDistribute (.*.) (+)
-    ; semiring_left_absorb :> LeftAbsorb (.*.) 0 }.
+    { semiplus_monoid : @IsCommutativeMonoid plus_is_sg_op zero_is_mon_unit
+    ; semimult_monoid : @IsCommutativeMonoid mult_is_sg_op one_is_mon_unit
+    ; semiring_distr : LeftDistribute (.*.) (+)
+    ; semiring_left_absorb : LeftAbsorb (.*.) 0 }.
+  #[global] Existing Instances semiplus_monoid semimult_monoid semiring_distr semiring_left_absorb.
 
   Context {Anegate : Negate A}.
 
   Class IsRing :=
-    { ring_group :> @IsAbGroup plus_is_sg_op zero_is_mon_unit _
-    ; ring_monoid :> @IsCommutativeMonoid mult_is_sg_op one_is_mon_unit
-    ; ring_dist :> LeftDistribute (.*.) (+) }.
+    { ring_group : @IsAbGroup plus_is_sg_op zero_is_mon_unit _
+    ; ring_monoid : @IsCommutativeMonoid mult_is_sg_op one_is_mon_unit
+    ; ring_dist : LeftDistribute (.*.) (+) }.
+  #[global] Existing Instances ring_group ring_monoid ring_dist.
 
   (* For now, we follow CoRN/ring_theory's example in having Ring and SemiRing
     require commutative multiplication. *)
@@ -127,26 +153,33 @@ Section upper_classes.
   Class IsIntegralDomain :=
     { intdom_ring : IsRing
     ; intdom_nontrivial : PropHolds (not (1 = 0))
-    ; intdom_nozeroes :> NoZeroDivisors A }.
+    ; intdom_nozeroes : NoZeroDivisors A }.
+  #[global] Existing Instances intdom_nozeroes.
 
   (* We do not include strong extensionality for (-) and (/)
     because it can de derived *)
   Class IsField {Aap: Apart A} {Arecip: Recip A} :=
-    { field_ring :> IsRing
-    ; field_apart :> IsApart A
-    ; field_plus_ext :> StrongBinaryExtensionality (+)
-    ; field_mult_ext :> StrongBinaryExtensionality (.*.)
+    { field_ring : IsRing
+    ; field_apart : IsApart A
+    ; field_plus_ext : StrongBinaryExtensionality (+)
+    ; field_mult_ext : StrongBinaryExtensionality (.*.)
     ; field_nontrivial : PropHolds (1 ≶ 0)
     ; recip_inverse : forall x, x.1 // x = 1 }.
+  #[global] Existing Instances
+    field_ring
+    field_apart
+    field_plus_ext
+    field_mult_ext.
 
   (* We let /0 = 0 so properties as Injective (/),
     f (/x) = / (f x), / /x = x, /x * /y = /(x * y) 
     hold without any additional assumptions *)
   Class IsDecField {Adec_recip : DecRecip A} :=
-    { decfield_ring :> IsRing
+    { decfield_ring : IsRing
     ; decfield_nontrivial : PropHolds (1 <> 0)
     ; dec_recip_0 : /0 = 0
     ; dec_recip_inverse : forall x, x <> 0 -> x / x = 1 }.
+  #[export] Existing Instances decfield_ring.
 
   Class FieldCharacteristic@{j} {Aap : Apart@{i j} A} (k : nat) : Type@{j}
     := field_characteristic : forall n : nat, Nat.lt@{i} 0 n ->
@@ -184,31 +217,48 @@ Section lattice.
   Context A {Ajoin: Join A} {Ameet: Meet A} {Abottom : Bottom A} {Atop : Top A}.
 
   Class IsJoinSemiLattice := 
-    join_semilattice :> @IsSemiLattice A join_is_sg_op.
+    join_semilattice : @IsSemiLattice A join_is_sg_op.
+  #[global] Existing Instance join_semilattice.
   Class IsBoundedJoinSemiLattice := 
-    bounded_join_semilattice :> @IsBoundedSemiLattice A
+    bounded_join_semilattice : @IsBoundedSemiLattice A
       join_is_sg_op bottom_is_mon_unit.
-  Class IsMeetSemiLattice := 
-    meet_semilattice :> @IsSemiLattice A meet_is_sg_op.
+  #[global] Existing Instance bounded_join_semilattice.
+  Class IsMeetSemiLattice :=
+    meet_semilattice : @IsSemiLattice A meet_is_sg_op.
+  #[global] Existing Instance meet_semilattice.
   Class IsBoundedMeetSemiLattice :=
-    bounded_meet_semilattice :> @IsBoundedSemiLattice A
+    bounded_meet_semilattice : @IsBoundedSemiLattice A
       meet_is_sg_op top_is_mon_unit.
+  #[global] Existing Instance bounded_meet_semilattice.
+
 
   Class IsLattice := 
-    { lattice_join :> IsJoinSemiLattice
-    ; lattice_meet :> IsMeetSemiLattice
-    ; join_meet_absorption :> Absorption (⊔) (⊓) 
-    ; meet_join_absorption :> Absorption (⊓) (⊔)}.
+    { lattice_join : IsJoinSemiLattice
+    ; lattice_meet : IsMeetSemiLattice
+    ; join_meet_absorption : Absorption (⊔) (⊓) 
+    ; meet_join_absorption : Absorption (⊓) (⊔) }.
+  #[global] Existing Instances
+    lattice_join
+    lattice_meet
+    join_meet_absorption 
+    meet_join_absorption.
 
   Class IsBoundedLattice :=
-    { boundedlattice_join :> IsBoundedJoinSemiLattice
-    ; boundedlattice_meet :> IsBoundedMeetSemiLattice
-    ; boundedjoin_meet_absorption :> Absorption (⊔) (⊓)
-    ; boundedmeet_join_absorption :> Absorption (⊓) (⊔)}.
+    { boundedlattice_join : IsBoundedJoinSemiLattice
+    ; boundedlattice_meet : IsBoundedMeetSemiLattice
+    ; boundedjoin_meet_absorption : Absorption (⊔) (⊓)
+    ; boundedmeet_join_absorption : Absorption (⊓) (⊔)}.
+  #[global] Existing Instances
+    boundedlattice_join
+    boundedlattice_meet
+    boundedjoin_meet_absorption
+    boundedmeet_join_absorption.
+  
 
   Class IsDistributiveLattice := 
-    { distr_lattice_lattice :> IsLattice
-    ; join_meet_distr_l :> LeftDistribute (⊔) (⊓) }.
+    { distr_lattice_lattice : IsLattice
+    ; join_meet_distr_l : LeftDistribute (⊔) (⊓) }.
+  #[global] Existing Instances distr_lattice_lattice join_meet_distr_l.
 End lattice.
 
 Section morphism_classes.
@@ -226,8 +276,9 @@ Section morphism_classes.
     preserves_mon_unit : f mon_unit = mon_unit.
 
   Class IsMonoidPreserving (f : A -> B) :=
-    { monmor_sgmor :> IsSemiGroupPreserving f
-    ; monmor_unitmor :> IsUnitPreserving f }.
+    { monmor_sgmor : IsSemiGroupPreserving f
+    ; monmor_unitmor : IsUnitPreserving f }.
+  #[global] Existing Instances monmor_sgmor monmor_unitmor.
   End sgmorphism_classes.
 
   Section ringmorphism_classes.
@@ -236,15 +287,17 @@ Section morphism_classes.
     {Aone : One A} {Bone : One B}.
 
   Class IsSemiRingPreserving (f : A -> B) :=
-    { semiringmor_plus_mor :> @IsMonoidPreserving A B
+    { semiringmor_plus_mor : @IsMonoidPreserving A B
         plus_is_sg_op plus_is_sg_op zero_is_mon_unit zero_is_mon_unit f
-    ; semiringmor_mult_mor :> @IsMonoidPreserving A B
+    ; semiringmor_mult_mor : @IsMonoidPreserving A B
         mult_is_sg_op mult_is_sg_op one_is_mon_unit one_is_mon_unit f }.
+  #[global] Existing Instances semiringmor_plus_mor semiringmor_mult_mor.
 
   Context {Aap : Apart A} {Bap : Apart B}.
   Class IsSemiRingStrongPreserving (f : A -> B) :=
-    { strong_semiringmor_sr_mor :> IsSemiRingPreserving f
-    ; strong_semiringmor_strong_mor :> StrongExtensionality f }.
+    { strong_semiringmor_sr_mor : IsSemiRingPreserving f
+    ; strong_semiringmor_strong_mor : StrongExtensionality f }.
+  #[global] Existing Instances strong_semiringmor_sr_mor strong_semiringmor_strong_mor.
   End ringmorphism_classes.
 
   Section latticemorphism_classes.
@@ -252,19 +305,25 @@ Section morphism_classes.
     {Ameet : Meet A} {Bmeet : Meet B}.
 
   Class IsJoinPreserving (f : A -> B) :=
-    join_slmor_sgmor :> @IsSemiGroupPreserving A B join_is_sg_op join_is_sg_op f.
+    join_slmor_sgmor : @IsSemiGroupPreserving A B join_is_sg_op join_is_sg_op f.
+  #[global] Existing Instances join_slmor_sgmor.
 
   Class IsMeetPreserving (f : A -> B) :=
-    meet_slmor_sgmor :> @IsSemiGroupPreserving A B meet_is_sg_op meet_is_sg_op f.
+    meet_slmor_sgmor : @IsSemiGroupPreserving A B meet_is_sg_op meet_is_sg_op f.
+  #[global] Existing Instances meet_slmor_sgmor.
 
   Context {Abottom : Bottom A} {Bbottom : Bottom B}.
   Class IsBoundedJoinPreserving (f : A -> B) := bounded_join_slmor_monmor
-      :> @IsMonoidPreserving A B join_is_sg_op join_is_sg_op
+      : @IsMonoidPreserving A B join_is_sg_op join_is_sg_op
          bottom_is_mon_unit bottom_is_mon_unit f.
+  #[global] Existing Instances bounded_join_slmor_monmor.
 
   Class IsLatticePreserving (f : A -> B) :=
-    { latticemor_join_mor :> IsJoinPreserving f
-    ; latticemor_meet_mor :> IsMeetPreserving f }.
+    { latticemor_join_mor : IsJoinPreserving f
+    ; latticemor_meet_mor : IsMeetPreserving f }.
+  #[global] Existing Instances
+    latticemor_join_mor
+    latticemor_meet_mor.
   End latticemorphism_classes.
 End morphism_classes.
 
diff --git a/theories/Classes/interfaces/canonical_names.v b/theories/Classes/interfaces/canonical_names.v
index 2505693d5b8..acb8976c41a 100644
--- a/theories/Classes/interfaces/canonical_names.v
+++ b/theories/Classes/interfaces/canonical_names.v
@@ -44,8 +44,9 @@ Notation "(≶ x )" := (fun y => apart y x) (only parsing) : mc_scope.
 (* Even for setoids with decidable equality x <> y does not imply x ≶ y.
 Therefore we introduce the following class. *)
 Class TrivialApart A {Aap : Apart A} :=
-  { trivial_apart_prop :> is_mere_relation A apart
+  { trivial_apart_prop : is_mere_relation A apart
   ; trivial_apart : forall x y, x ≶ y <-> x <> y }.
+#[global] Existing Instance trivial_apart_prop.
 
 Definition sig_apart `{Apart A} (P: A -> Type) : Apart (sig P) := fun x y => x.1 ≶ y.1.
 #[export]
@@ -207,7 +208,8 @@ Class Idempotent `(f: A -> A -> A) (x : A) : Type := idempotency: f x x = x.
 Arguments idempotency {A} _ _ {Idempotent}.
 
 Class UnaryIdempotent {A} (f: A -> A) : Type :=
-  unary_idempotent :> Idempotent Compose f.
+  unary_idempotent : Idempotent Compose f.
+#[global] Existing Instances unary_idempotent.
 
 Lemma unary_idempotency `{UnaryIdempotent A f} x : f (f x) = f x.
 Proof.
@@ -218,7 +220,8 @@ apply idempotency. apply _.
 Qed.
 
 Class BinaryIdempotent `(op: A -> A -> A) : Type
-  := binary_idempotent :> forall x, Idempotent op x.
+  := binary_idempotent : forall x, Idempotent op x.
+#[global] Existing Instances binary_idempotent.
 
 Class LeftIdentity {A B} (op : A -> B -> B) (x : A): Type
   := left_identity: forall y, op x y = y.
@@ -248,7 +251,8 @@ Class HeteroAssociative {A B C AB BC ABC}
   (fAB_C: AB -> C -> ABC) (fAB : A -> B -> AB): Type
   := associativity : forall x y z, fA_BC x (fBC y z) = fAB_C (fAB x y) z.
 Class Associative {A} (f : A -> A -> A)
-  := simple_associativity :> HeteroAssociative f f f f.
+  := simple_associativity : HeteroAssociative f f f f.
+#[global] Existing Instances simple_associativity.
 
 Class Involutive {A} (f : A -> A) := involutive: forall x, f (f x) = x.
 
@@ -270,9 +274,10 @@ Class AntiSymmetric `(R : Relation A) : Type
 Arguments antisymmetry {A} _ {AntiSymmetric} _ _ _ _.
 
 Class EquivRel `(R : Relation A) : Type := Build_EquivRel
-  { EquivRel_Reflexive :> Reflexive R ;
-    EquivRel_Symmetric :> Symmetric R ;
-    EquivRel_Transitive :> Transitive R }.
+  { EquivRel_Reflexive : Reflexive R ;
+    EquivRel_Symmetric : Symmetric R ;
+    EquivRel_Transitive : Transitive R }.
+#[global] Existing Instances EquivRel_Reflexive EquivRel_Symmetric EquivRel_Transitive.
 
 Definition SigEquivRel {A:Type} (R : Relation A) : Type :=
   {_ : Reflexive R | { _ : Symmetric R | Transitive R}}.
@@ -320,9 +325,12 @@ Class RightHeteroDistribute {A B C}
   (f : A -> B -> C) (g_l : A -> A -> A) (g : C -> C -> C) : Type
   := distribute_r: forall a b c, f (g_l a b) c = g (f a c) (f b c).
 Class LeftDistribute {A} (f g: A -> A -> A)
-  := simple_distribute_l :> LeftHeteroDistribute f g g.
+  := simple_distribute_l : LeftHeteroDistribute f g g.
+#[global] Existing Instances simple_distribute_l.
 Class RightDistribute {A} (f g: A -> A -> A)
-  := simple_distribute_r :> RightHeteroDistribute f g g.
+  := simple_distribute_r : RightHeteroDistribute f g g.
+#[global] Existing Instances simple_distribute_r.
+
 
 Class HeteroSymmetric {A} {T : A -> A -> Type}
   (R : forall {x y}, T x y -> T y x -> Type) : Type
@@ -406,8 +414,9 @@ Class Bind (M : Type -> Type) := bind : forall {A B}, M A -> (A -> M B) -> M B.
 
 Class Enumerable@{i} (A : Type@{i}) :=
   { enumerator : nat -> A
-  ; enumerator_issurj :>
+  ; enumerator_issurj :
     IsConnMap@{i} (trunc_S minus_two) enumerator }.
+#[global] Existing Instance enumerator_issurj.
 Arguments enumerator A {_} _.
 Arguments enumerator_issurj A {_} _.
 
diff --git a/theories/Classes/interfaces/integers.v b/theories/Classes/interfaces/integers.v
index 08819d0198c..1cbc3407a3f 100644
--- a/theories/Classes/interfaces/integers.v
+++ b/theories/Classes/interfaces/integers.v
@@ -10,11 +10,12 @@ Arguments integers_to_ring A {_} R {_ _ _ _ _ _} _.
 
 Class Integers A {Aap:Apart A} {Aplus Amult Azero Aone Anegate Ale Alt}
   `{U : IntegersToRing A} :=
-  { integers_ring :> @IsRing A Aplus Amult Azero Aone Anegate
-  ; integers_order :> FullPseudoSemiRingOrder Ale Alt
-  ; integers_to_ring_mor:> forall {B} `{IsRing B}, IsSemiRingPreserving (integers_to_ring A B)
+  { integers_ring : @IsRing A Aplus Amult Azero Aone Anegate
+  ; integers_order : FullPseudoSemiRingOrder Ale Alt
+  ; integers_to_ring_mor : forall {B} `{IsRing B}, IsSemiRingPreserving (integers_to_ring A B)
   ; integers_initial: forall {B} `{IsRing B} {h : A -> B} `{!IsSemiRingPreserving h} x,
       integers_to_ring A B x = h x}.
+#[global] Existing Instances integers_ring integers_order integers_to_ring_mor.
 
 Section specializable.
   Context (Z N : Type) `{Integers Z} `{Naturals N}.
diff --git a/theories/Classes/interfaces/naturals.v b/theories/Classes/interfaces/naturals.v
index 5462ded0f09..f842fce1148 100644
--- a/theories/Classes/interfaces/naturals.v
+++ b/theories/Classes/interfaces/naturals.v
@@ -9,12 +9,13 @@ Arguments naturals_to_semiring A {_} B {_ _ _ _ _} _.
 
 Class Naturals A {Aap:Apart A} {Aplus Amult Azero Aone Ale Alt}
   `{U: NaturalsToSemiRing A} :=
-  { naturals_ring :> @IsSemiRing A Aplus Amult Azero Aone
-  ; naturals_order :> FullPseudoSemiRingOrder Ale Alt
-  ; naturals_to_semiring_mor:> forall {B} `{IsSemiRing B},
+  { naturals_ring : @IsSemiRing A Aplus Amult Azero Aone
+  ; naturals_order : FullPseudoSemiRingOrder Ale Alt
+  ; naturals_to_semiring_mor : forall {B} `{IsSemiRing B},
     IsSemiRingPreserving (naturals_to_semiring A B)
   ; naturals_initial: forall {B} `{IsSemiRing B} {h : A -> B} `{!IsSemiRingPreserving h} x,
     naturals_to_semiring A B x = h x }.
+#[global] Existing Instances naturals_ring naturals_order naturals_to_semiring_mor.
 
 (* Specializable operations: *)
 Class NatDistance N `{Plus N}
diff --git a/theories/Classes/interfaces/orders.v b/theories/Classes/interfaces/orders.v
index 1e36d3d14da..16607dcca43 100644
--- a/theories/Classes/interfaces/orders.v
+++ b/theories/Classes/interfaces/orders.v
@@ -20,14 +20,22 @@ usual properties like Trichotomy (<) and TotalRelation (≤).
 *)
 
 Class PartialOrder `(Ale : Le A) :=
-  { po_hset :> IsHSet A
-  ; po_hprop :> is_mere_relation A Ale
-  ; po_preorder:> PreOrder (≤)
-  ; po_antisym:> AntiSymmetric (≤) }.
+  { po_hset : IsHSet A
+  ; po_hprop : is_mere_relation A Ale
+  ; po_preorder : PreOrder (≤)
+  ; po_antisym : AntiSymmetric (≤) }.
+#[global] Existing Instances
+  po_hset
+  po_hprop
+  po_preorder
+  po_antisym. 
 
 Class TotalOrder `(Ale : Le A) :=
-  { total_order_po :> PartialOrder (≤)
-  ; total_order_total :> TotalRelation (≤) }.
+  { total_order_po : PartialOrder (≤)
+  ; total_order_total : TotalRelation (≤) }.
+#[global] Existing Instances
+  total_order_po
+  total_order_total.
 
 (*
 We define a variant of the order theoretic definition of meet and join
@@ -39,50 +47,57 @@ This is needed to prove equavalence with the algebraic definition. We
 do this in orders.lattices.
 *)
 Class MeetSemiLatticeOrder `(Ale : Le A) `{Meet A} :=
-  { meet_sl_order :> PartialOrder (≤)
+  { meet_sl_order : PartialOrder (≤)
   ; meet_lb_l : forall x y, x ⊓ y ≤ x
   ; meet_lb_r : forall x y, x ⊓ y ≤ y
   ; meet_glb : forall x y z, z ≤ x -> z ≤ y -> z ≤ x ⊓ y }.
+#[global] Existing Instances meet_sl_order.
 
 Class JoinSemiLatticeOrder `(Ale : Le A) `{Join A} :=
-  { join_sl_order :> PartialOrder (≤)
+  { join_sl_order : PartialOrder (≤)
   ; join_ub_l : forall x y, x ≤ x ⊔ y
   ; join_ub_r : forall x y, y ≤ x ⊔ y
   ; join_lub : forall x y z, x ≤ z -> y ≤ z -> x ⊔ y ≤ z }.
+#[global] Existing Instances join_sl_order.
 
 Class LatticeOrder `(Ale : Le A) `{Meet A} `{Join A} :=
-  { lattice_order_meet :> MeetSemiLatticeOrder (≤)
-  ; lattice_order_join :> JoinSemiLatticeOrder (≤) }.
+  { lattice_order_meet : MeetSemiLatticeOrder (≤)
+  ; lattice_order_join : JoinSemiLatticeOrder (≤) }.
+#[global] Existing Instances lattice_order_meet lattice_order_join.
 
 Class StrictOrder `(Alt : Lt A) :=
-  { strict_order_mere :> is_mere_relation A lt
-  ; strictorder_irrefl :> Irreflexive (<)
-  ; strictorder_trans :> Transitive (<) }.
+  { strict_order_mere : is_mere_relation A lt
+  ; strictorder_irrefl : Irreflexive (<)
+  ; strictorder_trans : Transitive (<) }.
+#[global] Existing Instances strict_order_mere strictorder_irrefl strictorder_trans.
 
 (* The constructive notion of a total strict total order.
    We will prove that (<) is in fact a StrictOrder. *)
 Class PseudoOrder `{Aap : Apart A} (Alt : Lt A) :=
-  { pseudo_order_apart : IsApart A
-  ; pseudo_order_mere_lt :> is_mere_relation A lt
+{ pseudo_order_apart : IsApart A
+  ; pseudo_order_mere_lt : is_mere_relation A lt
   ; pseudo_order_antisym : forall x y, ~(x < y /\ y < x)
-  ; pseudo_order_cotrans :> CoTransitive (<)
+  ; pseudo_order_cotrans : CoTransitive (<)
   ; apart_iff_total_lt : forall x y, x ≶ y <-> x < y |_| y < x }.
+#[global] Existing Instances pseudo_order_mere_lt pseudo_order_cotrans.
 
 (* A partial order (≤) with a corresponding (<). We will prove that (<) is in fact
   a StrictOrder *)
 Class FullPartialOrder `{Aap : Apart A} (Ale : Le A) (Alt : Lt A) :=
   { strict_po_apart : IsApart A
   ; strict_po_mere_lt : is_mere_relation A lt
-  ; strict_po_po :> PartialOrder (≤)
-  ; strict_po_trans :> Transitive (<)
+  ; strict_po_po : PartialOrder (≤)
+  ; strict_po_trans : Transitive (<)
   ; lt_iff_le_apart : forall x y, x < y <-> x ≤ y /\ x ≶ y }.
+#[global] Existing Instances strict_po_po strict_po_trans.
 
 (* A pseudo order (<) with a corresponding (≤). We will prove that (≤) is in fact
   a PartialOrder. *)
 Class FullPseudoOrder `{Aap : Apart A} (Ale : Le A) (Alt : Lt A) :=
-  { fullpseudo_le_hprop :> is_mere_relation A Ale
-  ; full_pseudo_order_pseudo :> PseudoOrder Alt
+  { fullpseudo_le_hprop : is_mere_relation A Ale
+  ; full_pseudo_order_pseudo : PseudoOrder Alt
   ; le_iff_not_lt_flip : forall x y, x ≤ y <-> ~(y < x) }.
+#[global] Existing Instances fullpseudo_le_hprop full_pseudo_order_pseudo.
 
 Section order_maps.
   Context {A B : Type} {Ale: Le A} {Ble: Le B}(f : A -> B).
@@ -92,8 +107,9 @@ Section order_maps.
   Class OrderReflecting := order_reflecting : forall x y, (f x ≤ f y -> x ≤ y).
 
   Class OrderEmbedding :=
-    { order_embedding_preserving :> OrderPreserving
-    ; order_embedding_reflecting :> OrderReflecting }.
+    { order_embedding_preserving : OrderPreserving
+    ; order_embedding_reflecting : OrderReflecting }.
+  #[global] Existing Instances order_embedding_preserving order_embedding_reflecting.
 End order_maps.
 
 Section srorder_maps.
@@ -106,8 +122,9 @@ Section srorder_maps.
     : forall x y, (f x < f y -> x < y).
 
   Class StrictOrderEmbedding :=
-    { strict_order_embedding_preserving :> StrictlyOrderPreserving
-    ; strict_order_embedding_reflecting :> StrictlyOrderReflecting }.
+    { strict_order_embedding_preserving : StrictlyOrderPreserving
+    ; strict_order_embedding_reflecting : StrictlyOrderReflecting }.
+  #[global] Existing Instances strict_order_embedding_preserving strict_order_embedding_reflecting.
 End srorder_maps.
 
 #[export]
@@ -124,34 +141,38 @@ Davorin Lešnik's PhD thesis.
 *)
 Class SemiRingOrder `{Plus A} `{Mult A}
     `{Zero A} `{One A} (Ale : Le A) :=
-  { srorder_po :> PartialOrder Ale
+  { srorder_po : PartialOrder Ale
   ; srorder_partial_minus : forall x y, x ≤ y -> exists z, y = x + z
-  ; srorder_plus :> forall z, OrderEmbedding (z +)
+  ; srorder_plus : forall z, OrderEmbedding (z +)
   ; nonneg_mult_compat : forall x y, PropHolds (0 ≤ x) -> PropHolds (0 ≤ y) ->
                                 PropHolds (0 ≤ x * y) }.
+#[global] Existing Instances srorder_po srorder_plus.
 
 Class StrictSemiRingOrder `{Plus A} `{Mult A}
     `{Zero A} `{One A} (Alt : Lt A) :=
-  { strict_srorder_so :> StrictOrder Alt
+  { strict_srorder_so : StrictOrder Alt
   ; strict_srorder_partial_minus : forall x y, x < y -> exists z, y = x + z
-  ; strict_srorder_plus :> forall z, StrictOrderEmbedding (z +)
+  ; strict_srorder_plus : forall z, StrictOrderEmbedding (z +)
   ; pos_mult_compat : forall x y, PropHolds (0 < x) -> PropHolds (0 < y) ->
                              PropHolds (0 < x * y) }.
+#[global] Existing Instances strict_srorder_so strict_srorder_plus.
 
 Class PseudoSemiRingOrder `{Apart A} `{Plus A}
     `{Mult A} `{Zero A} `{One A} (Alt : Lt A) :=
-  { pseudo_srorder_strict :> PseudoOrder Alt
+  { pseudo_srorder_strict : PseudoOrder Alt
   ; pseudo_srorder_partial_minus : forall x y, ~(y < x) -> exists z, y = x + z
-  ; pseudo_srorder_plus :> forall z, StrictOrderEmbedding (z +)
-  ; pseudo_srorder_mult_ext :> StrongBinaryExtensionality (.*.)
+  ; pseudo_srorder_plus : forall z, StrictOrderEmbedding (z +)
+  ; pseudo_srorder_mult_ext : StrongBinaryExtensionality (.*.)
   ; pseudo_srorder_pos_mult_compat : forall x y, PropHolds (0 < x) -> PropHolds (0 < y) ->
                                             PropHolds (0 < x * y) }.
+#[global] Existing Instances pseudo_srorder_strict pseudo_srorder_plus pseudo_srorder_mult_ext.
 
 Class FullPseudoSemiRingOrder `{Apart A} `{Plus A}
     `{Mult A} `{Zero A} `{One A} (Ale : Le A) (Alt : Lt A) :=
-  { full_pseudo_srorder_le_hprop :> is_mere_relation A Ale
-  ; full_pseudo_srorder_pso :> PseudoSemiRingOrder Alt
+  { full_pseudo_srorder_le_hprop : is_mere_relation A Ale
+  ; full_pseudo_srorder_pso : PseudoSemiRingOrder Alt
   ; full_pseudo_srorder_le_iff_not_lt_flip : forall x y, x ≤ y <-> ~(y < x) }.
+#[global] Existing Instances full_pseudo_srorder_le_hprop full_pseudo_srorder_pso.
 
 (* Due to bug #2528 *)
 #[export]
@@ -191,7 +212,11 @@ HoTT book chapter 11. *)
 Class OrderedField (A : Type) {Alt : Lt A} {Ale : Le A} {Aap : Apart A} {Azero : Zero A}
       {Aone : One A} {Aplus : Plus A} {Anegate : Negate A} {Amult : Mult A}
       {Arecip : Recip A} {Ajoin : Join A} {Ameet : Meet A} :=
-  { ordered_field_field :> @IsField A Aplus Amult Azero Aone Anegate Aap Arecip
-  ; ordered_field_lattice :> LatticeOrder Ale
-  ; ordered_field_fssro :> @FullPseudoSemiRingOrder A _ _ _ Azero _ _ _
+  { ordered_field_field : @IsField A Aplus Amult Azero Aone Anegate Aap Arecip
+  ; ordered_field_lattice : LatticeOrder Ale
+  ; ordered_field_fssro : @FullPseudoSemiRingOrder A _ _ _ Azero _ _ _
   }.
+#[global] Existing Instances
+  ordered_field_field
+  ordered_field_lattice
+  ordered_field_fssro.
diff --git a/theories/Classes/interfaces/rationals.v b/theories/Classes/interfaces/rationals.v
index dc9a8d2a555..9e8fcb85863 100644
--- a/theories/Classes/interfaces/rationals.v
+++ b/theories/Classes/interfaces/rationals.v
@@ -21,10 +21,11 @@ Arguments rationals_to_field A {_} B {_ _ _ _ _ _ _ _ _} _.
 
 Class Rationals A {Aap : Apart A} {Aplus Amult Azero Aone Aneg Arecip Ale Alt}
   `{U : !RationalsToField A} :=
-  { rationals_field :> @IsDecField A Aplus Amult Azero Aone Aneg Arecip
-  ; rationals_order :> FullPseudoSemiRingOrder Ale Alt
-  ; rationals_to_field_mor :> forall {B} `{IsField B} `{!FieldCharacteristic B 0},
+  { rationals_field : @IsDecField A Aplus Amult Azero Aone Aneg Arecip
+  ; rationals_order : FullPseudoSemiRingOrder Ale Alt
+  ; rationals_to_field_mor : forall {B} `{IsField B} `{!FieldCharacteristic B 0},
     IsSemiRingPreserving (rationals_to_field A B)
   ; rationals_initial : forall {B} `{IsField B} `{!FieldCharacteristic B 0}
     {h : A -> B} `{!IsSemiRingPreserving h} x,
     rationals_to_field A B x = h x }.
+#[global] Existing Instances rationals_field rationals_order rationals_to_field_mor.
diff --git a/theories/Classes/theory/premetric.v b/theories/Classes/theory/premetric.v
index 29f395e07f2..fa0a568a108 100644
--- a/theories/Classes/theory/premetric.v
+++ b/theories/Classes/theory/premetric.v
@@ -45,12 +45,19 @@ Class Rounded@{i j} (A:Type@{i}) `{Closeness A}
       e = d + d' /\ close d u v)))).
 
 Class PreMetric@{i j} (A:Type@{i}) {Aclose : Closeness A} :=
-  { premetric_prop :> forall e, is_mere_relation A (close e)
-  ; premetric_refl :> forall e, Reflexive (close (A:=A) e)
-  ; premetric_symm :> forall e, Symmetric (close (A:=A) e)
-  ; premetric_separated :> Separated A
-  ; premetric_triangular :> Triangular A
-  ; premetric_rounded :> Rounded@{i j} A }.
+  { premetric_prop : forall e, is_mere_relation A (close e)
+  ; premetric_refl : forall e, Reflexive (close (A:=A) e)
+  ; premetric_symm : forall e, Symmetric (close (A:=A) e)
+  ; premetric_separated : Separated A
+  ; premetric_triangular : Triangular A
+  ; premetric_rounded : Rounded@{i j} A }.
+#[global] Existing Instances
+  premetric_prop
+  premetric_refl
+  premetric_symm
+  premetric_separated
+  premetric_triangular
+  premetric_rounded.
 
 Global Instance premetric_hset@{i j} `{Funext}
   {A:Type@{i} } `{PreMetric@{i j} A} : IsHSet A.
diff --git a/theories/Diagrams/DDiagram.v b/theories/Diagrams/DDiagram.v
index 5d0334a2c74..0143ba4bd8f 100644
--- a/theories/Diagrams/DDiagram.v
+++ b/theories/Diagrams/DDiagram.v
@@ -35,5 +35,6 @@ Definition DDiagram {G : Graph} (D : Diagram G)
 
   Class Equifibered {G : Graph} {D : Diagram G} (E : DDiagram D) := {
     isequifibered i j (g : G i j) (x : D i)
-      :> IsEquiv (@arr _ E (i; x) (j; D _f g x) (g; idpath));
+      : IsEquiv (@arr _ E (i; x) (j; D _f g x) (g; idpath));
   }.
+  #[global] Existing Instance isequifibered.
diff --git a/theories/Homotopy/CayleyDickson.v b/theories/Homotopy/CayleyDickson.v
index 07e97772574..d5752a7cbe0 100644
--- a/theories/Homotopy/CayleyDickson.v
+++ b/theories/Homotopy/CayleyDickson.v
@@ -11,17 +11,28 @@ Local Open Scope mc_mult_scope.
 (** A Cayley-Dickson Spheroid is a pointed type X which is an H-space, with two operations called negation and conjugation, satisfying the seven following laws.
   --x=x   x**=x   1*=1    (-x)*=-x*   x(-y)=-(xy)   (xy)* = y* x*    x* x=1    *)
 Class CayleyDicksonSpheroid (X : pType) := {
-  cds_hspace :> IsHSpace X;
-  cds_negate :> Negate X;
-  cds_conjug :> Conjugate X;
-  cds_negate_inv :> Involutive cds_negate;
-  cds_conjug_inv :> Involutive cds_conjug;
-  cds_conjug_unit_pres :> IsUnitPreserving cds_conjug;
-  cds_conjug_left_inv :> LeftInverse (.*.) cds_conjug mon_unit;
-  cds_conjug_distr :> DistrOpp (.*.) cds_conjug;
-  cds_swapop :> SwapOp (-) cds_conjug;
-  cds_factorneg_r :> FactorNegRight (-) (.*.);
+  cds_hspace : IsHSpace X;
+  cds_negate : Negate X;
+  cds_conjug : Conjugate X;
+  cds_negate_inv : Involutive cds_negate;
+  cds_conjug_inv : Involutive cds_conjug;
+  cds_conjug_unit_pres : IsUnitPreserving cds_conjug;
+  cds_conjug_left_inv : LeftInverse (.*.) cds_conjug mon_unit;
+  cds_conjug_distr : DistrOpp (.*.) cds_conjug;
+  cds_swapop : SwapOp (-) cds_conjug;
+  cds_factorneg_r : FactorNegRight (-) (.*.);
 }.
+#[global] Existing Instances
+  cds_hspace
+  cds_negate
+  cds_conjug
+  cds_negate_inv
+  cds_conjug_inv
+  cds_conjug_unit_pres
+  cds_conjug_left_inv
+  cds_conjug_distr
+  cds_swapop
+  cds_factorneg_r.
 
 Section CayleyDicksonSpherioid_Properties.
 
@@ -73,14 +84,20 @@ Proof.
 Defined.
 
 Class CayleyDicksonImaginaroid (A : Type) := {
-  cdi_negate :> Negate A;
-  cdi_negate_involutive :> Involutive cdi_negate;
-  cdi_susp_hspace :> IsHSpace (Build_pType (Susp A) _);
-  cdi_susp_factorneg_r :> FactorNegRight (negate_susp A cdi_negate) hspace_op;
-  cdi_susp_conjug_left_inv
-    :> LeftInverse hspace_op (conjugate_susp A cdi_negate) mon_unit;
-  cdi_susp_conjug_distr :> DistrOpp hspace_op (conjugate_susp A cdi_negate);
+  cdi_negate : Negate A;
+  cdi_negate_involutive : Involutive cdi_negate;
+  cdi_susp_hspace : IsHSpace (Build_pType (Susp A) _);
+  cdi_susp_factorneg_r : FactorNegRight (negate_susp A cdi_negate) hspace_op;
+  cdi_susp_conjug_left_inv : LeftInverse hspace_op (conjugate_susp A cdi_negate) mon_unit;
+  cdi_susp_conjug_distr : DistrOpp hspace_op (conjugate_susp A cdi_negate);
 }.
+#[global] Existing Instances
+  cdi_negate
+  cdi_negate_involutive
+  cdi_susp_hspace
+  cdi_susp_factorneg_r
+  cdi_susp_conjug_left_inv
+  cdi_susp_conjug_distr.
 
 Global Instance involutive_negate_susp {A} `(CayleyDicksonImaginaroid A)
   : Involutive (negate_susp A cdi_negate).
diff --git a/theories/Homotopy/HSpace.v b/theories/Homotopy/HSpace.v
index a6390126c81..1f7ea6b59b7 100644
--- a/theories/Homotopy/HSpace.v
+++ b/theories/Homotopy/HSpace.v
@@ -7,10 +7,11 @@ Local Open Scope trunc_scope.
 Local Open Scope mc_mult_scope.
 
 Class IsHSpace (X : pType) := {
-  hspace_op :> SgOp X;
-  hspace_left_identity :> LeftIdentity hspace_op (point _);
-  hspace_right_identity :> RightIdentity hspace_op (point _);
+  hspace_op : SgOp X;
+  hspace_left_identity : LeftIdentity hspace_op (point _);
+  hspace_right_identity : RightIdentity hspace_op (point _);
 }.
+#[global] Existing Instances hspace_left_identity hspace_right_identity hspace_op.
 
 Global Instance hspace_mon_unit {X : pType} `{IsHSpace X} : MonUnit X := point _.
 
diff --git a/theories/Sets/Ordinals.v b/theories/Sets/Ordinals.v
index 357939b715d..21e17178f70 100644
--- a/theories/Sets/Ordinals.v
+++ b/theories/Sets/Ordinals.v
@@ -51,13 +51,19 @@ Proof. unfold Extensional. exact _. Qed.
 
 (** * Ordinals *)
 
-Class IsOrdinal@{carrier relation} (A : Type@{carrier}) (R : Relation@{carrier relation} A) :=
-  { ordinal_is_hset :> IsHSet A
-    ; ordinal_relation_is_mere :> is_mere_relation A R
-    ; ordinal_extensionality :> Extensional R
-    ; ordinal_well_foundedness :> WellFounded R
-    ; ordinal_transitivity :> Transitive R
-  }.
+Class IsOrdinal@{carrier relation} (A : Type@{carrier}) (R : Relation@{carrier relation} A) := {
+  ordinal_is_hset : IsHSet A ;
+  ordinal_relation_is_mere : is_mere_relation A R ;
+  ordinal_extensionality : Extensional R ;
+  ordinal_well_foundedness : WellFounded R ;
+  ordinal_transitivity : Transitive R ;
+}.
+#[global] Existing Instances
+  ordinal_is_hset
+  ordinal_relation_is_mere
+  ordinal_extensionality
+  ordinal_well_foundedness
+  ordinal_transitivity.
 
 Global Instance ishprop_IsOrdinal `{Funext} A R
   : IsHProp (IsOrdinal A R).

From 8ac35b523d5df69ba01b228c39af5153484f3856 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Sat, 7 May 2022 20:48:09 +0100
Subject: [PATCH 2/4] Fix warning about assert_succeeds

This has become a built-in tactic in Coq 8.16.
---
 theories/Basics/Tactics.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Basics/Tactics.v b/theories/Basics/Tactics.v
index 2e599d0aaf8..f689d20f8ef 100644
--- a/theories/Basics/Tactics.v
+++ b/theories/Basics/Tactics.v
@@ -472,7 +472,7 @@ Tactic Notation "funext" simple_intropattern(a) simple_intropattern(b) simple_in
 (* Test whether a tactic fails or succeeds, without actually doing anything.  Taken from Coq stdlib. *)
 Ltac assert_fails tac :=
   tryif (once tac) then gfail 0 tac "succeeds" else idtac.
-Ltac assert_succeeds tac :=
+Tactic Notation "assert_succeeds" tactic3(tac) :=
   tryif (assert_fails tac) then gfail 0 tac "fails" else idtac.
 Tactic Notation "assert_succeeds" tactic3(tac) :=
   assert_succeeds tac.

From 50d24665a019841e57fb4653d7a80452b8eb5bd9 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Sat, 7 May 2022 20:51:50 +0100
Subject: [PATCH 3/4] Change #[global] instances to #[export]

---
 theories/Categories/Functor/Attributes.v      |  2 +-
 .../Classes/interfaces/abstract_algebra.v     | 56 +++++++++----------
 theories/Classes/interfaces/canonical_names.v | 16 +++---
 theories/Classes/interfaces/integers.v        |  2 +-
 theories/Classes/interfaces/naturals.v        |  2 +-
 theories/Classes/interfaces/orders.v          | 32 +++++------
 theories/Classes/interfaces/rationals.v       |  2 +-
 theories/Classes/theory/premetric.v           |  2 +-
 theories/Diagrams/DDiagram.v                  |  2 +-
 theories/Homotopy/CayleyDickson.v             |  4 +-
 theories/Homotopy/HSpace.v                    |  2 +-
 theories/Sets/Ordinals.v                      |  2 +-
 12 files changed, 62 insertions(+), 62 deletions(-)

diff --git a/theories/Categories/Functor/Attributes.v b/theories/Categories/Functor/Attributes.v
index e7e2d710298..821f02ec440 100644
--- a/theories/Categories/Functor/Attributes.v
+++ b/theories/Categories/Functor/Attributes.v
@@ -145,6 +145,6 @@ Class IsEssentiallySurjective A B (F : Functor A B)
 Class IsWeakEquivalence `{Funext} A B (F : Functor A B)
   := { is_fully_faithful__is_weak_equivalence : IsFullyFaithful F;
        is_essentially_surjective__is_weak_equivalence : IsEssentiallySurjective F }.
-#[global] Existing Instances
+#[export] Existing Instances
   is_fully_faithful__is_weak_equivalence
   is_essentially_surjective__is_weak_equivalence.
diff --git a/theories/Classes/interfaces/abstract_algebra.v b/theories/Classes/interfaces/abstract_algebra.v
index 61793f0a400..d3a4baee48d 100644
--- a/theories/Classes/interfaces/abstract_algebra.v
+++ b/theories/Classes/interfaces/abstract_algebra.v
@@ -12,7 +12,7 @@ Class Setoid_Morphism :=
   { setoidmor_a : Setoid A
   ; setoidmor_b : Setoid B
   ; sm_proper : Proper ((=) ==> (=)) f }.
-#[global] Existing Instances setoidmor_a setoidmor_b sm_proper.
+#[export] Existing Instances setoidmor_a setoidmor_b sm_proper.
 
 then each time a Setoid instance is required, Coq will try to prove that a
 Setoid_Morphism exists. This obviously results in an enormous blow-up of the
@@ -31,7 +31,7 @@ Class IsApart A {Aap : Apart A} : Type :=
   ; apart_symmetric : Symmetric (≶)
   ; apart_cotrans : CoTransitive (≶)
   ; tight_apart : forall x y, ~(x ≶ y) <-> x = y }.
-#[global] Existing Instances
+#[export] Existing Instances
   apart_set
   apart_mere
   apart_symmetric
@@ -79,23 +79,23 @@ Section upper_classes.
   Class IsSemiGroup {Aop: SgOp A} :=
     { sg_set : IsHSet A
     ; sg_ass : Associative (.*.) }.
-    #[global] Existing Instances sg_set sg_ass.
+    #[export] Existing Instances sg_set sg_ass.
 
   Class IsCommutativeSemiGroup {Aop : SgOp A} :=
     { comsg_sg : @IsSemiGroup (.*.)
     ; comsg_comm : Commutative (.*.) }.
-  #[global] Existing Instances comsg_sg comsg_comm.
+  #[export] Existing Instances comsg_sg comsg_comm.
 
   Class IsSemiLattice {Aop : SgOp A} :=
     { semilattice_sg : @IsCommutativeSemiGroup (.*.)
     ; semilattice_idempotent : BinaryIdempotent (.*.)}.
-  #[global] Existing Instances semilattice_sg semilattice_idempotent.
+  #[export] Existing Instances semilattice_sg semilattice_idempotent.
 
   Class IsMonoid {Aop : SgOp A} {Aunit : MonUnit A} :=
     { monoid_semigroup : IsSemiGroup
     ; monoid_left_id : LeftIdentity (.*.) mon_unit
     ; monoid_right_id : RightIdentity (.*.) mon_unit }.
-  #[global] Existing Instances
+  #[export] Existing Instances
     monoid_semigroup
     monoid_left_id
     monoid_right_id.
@@ -103,7 +103,7 @@ Section upper_classes.
   Class IsCommutativeMonoid {Aop : SgOp A} {Aunit : MonUnit A} :=
     { commonoid_mon : @IsMonoid (.*.) Aunit
     ; commonoid_commutative : Commutative (.*.) }.
-  #[global] Existing Instances
+  #[export] Existing Instances
     commonoid_mon
     commonoid_commutative.
 
@@ -111,7 +111,7 @@ Section upper_classes.
     { group_monoid : @IsMonoid (.*.) Aunit
     ; negate_l : LeftInverse (.*.) (-) mon_unit
     ; negate_r : RightInverse (.*.) (-) mon_unit }.
-  #[global] Existing Instances 
+  #[export] Existing Instances 
     group_monoid
     negate_l
     negate_r.
@@ -119,14 +119,14 @@ Section upper_classes.
   Class IsBoundedSemiLattice {Aop : SgOp A} {Aunit : MonUnit A} :=
     { bounded_semilattice_mon : @IsCommutativeMonoid (.*.) Aunit
     ; bounded_semilattice_idempotent : BinaryIdempotent (.*.)}.
-  #[global] Existing Instances
+  #[export] Existing Instances
     bounded_semilattice_mon
     bounded_semilattice_idempotent.
 
   Class IsAbGroup {Aop : SgOp A} {Aunit : MonUnit A} {Anegate : Negate A} :=
     { abgroup_group : @IsGroup (.*.) Aunit Anegate
     ; abgroup_commutative : Commutative (.*.) }.
-  #[global] Existing Instances abgroup_group abgroup_commutative.
+  #[export] Existing Instances abgroup_group abgroup_commutative.
 
   Close Scope mc_mult_scope.
 
@@ -137,7 +137,7 @@ Section upper_classes.
     ; semimult_monoid : @IsCommutativeMonoid mult_is_sg_op one_is_mon_unit
     ; semiring_distr : LeftDistribute (.*.) (+)
     ; semiring_left_absorb : LeftAbsorb (.*.) 0 }.
-  #[global] Existing Instances semiplus_monoid semimult_monoid semiring_distr semiring_left_absorb.
+  #[export] Existing Instances semiplus_monoid semimult_monoid semiring_distr semiring_left_absorb.
 
   Context {Anegate : Negate A}.
 
@@ -145,7 +145,7 @@ Section upper_classes.
     { ring_group : @IsAbGroup plus_is_sg_op zero_is_mon_unit _
     ; ring_monoid : @IsCommutativeMonoid mult_is_sg_op one_is_mon_unit
     ; ring_dist : LeftDistribute (.*.) (+) }.
-  #[global] Existing Instances ring_group ring_monoid ring_dist.
+  #[export] Existing Instances ring_group ring_monoid ring_dist.
 
   (* For now, we follow CoRN/ring_theory's example in having Ring and SemiRing
     require commutative multiplication. *)
@@ -154,7 +154,7 @@ Section upper_classes.
     { intdom_ring : IsRing
     ; intdom_nontrivial : PropHolds (not (1 = 0))
     ; intdom_nozeroes : NoZeroDivisors A }.
-  #[global] Existing Instances intdom_nozeroes.
+  #[export] Existing Instances intdom_nozeroes.
 
   (* We do not include strong extensionality for (-) and (/)
     because it can de derived *)
@@ -165,7 +165,7 @@ Section upper_classes.
     ; field_mult_ext : StrongBinaryExtensionality (.*.)
     ; field_nontrivial : PropHolds (1 ≶ 0)
     ; recip_inverse : forall x, x.1 // x = 1 }.
-  #[global] Existing Instances
+  #[export] Existing Instances
     field_ring
     field_apart
     field_plus_ext
@@ -218,18 +218,18 @@ Section lattice.
 
   Class IsJoinSemiLattice := 
     join_semilattice : @IsSemiLattice A join_is_sg_op.
-  #[global] Existing Instance join_semilattice.
+  #[export] Existing Instance join_semilattice.
   Class IsBoundedJoinSemiLattice := 
     bounded_join_semilattice : @IsBoundedSemiLattice A
       join_is_sg_op bottom_is_mon_unit.
-  #[global] Existing Instance bounded_join_semilattice.
+  #[export] Existing Instance bounded_join_semilattice.
   Class IsMeetSemiLattice :=
     meet_semilattice : @IsSemiLattice A meet_is_sg_op.
-  #[global] Existing Instance meet_semilattice.
+  #[export] Existing Instance meet_semilattice.
   Class IsBoundedMeetSemiLattice :=
     bounded_meet_semilattice : @IsBoundedSemiLattice A
       meet_is_sg_op top_is_mon_unit.
-  #[global] Existing Instance bounded_meet_semilattice.
+  #[export] Existing Instance bounded_meet_semilattice.
 
 
   Class IsLattice := 
@@ -237,7 +237,7 @@ Section lattice.
     ; lattice_meet : IsMeetSemiLattice
     ; join_meet_absorption : Absorption (⊔) (⊓) 
     ; meet_join_absorption : Absorption (⊓) (⊔) }.
-  #[global] Existing Instances
+  #[export] Existing Instances
     lattice_join
     lattice_meet
     join_meet_absorption 
@@ -248,7 +248,7 @@ Section lattice.
     ; boundedlattice_meet : IsBoundedMeetSemiLattice
     ; boundedjoin_meet_absorption : Absorption (⊔) (⊓)
     ; boundedmeet_join_absorption : Absorption (⊓) (⊔)}.
-  #[global] Existing Instances
+  #[export] Existing Instances
     boundedlattice_join
     boundedlattice_meet
     boundedjoin_meet_absorption
@@ -258,7 +258,7 @@ Section lattice.
   Class IsDistributiveLattice := 
     { distr_lattice_lattice : IsLattice
     ; join_meet_distr_l : LeftDistribute (⊔) (⊓) }.
-  #[global] Existing Instances distr_lattice_lattice join_meet_distr_l.
+  #[export] Existing Instances distr_lattice_lattice join_meet_distr_l.
 End lattice.
 
 Section morphism_classes.
@@ -278,7 +278,7 @@ Section morphism_classes.
   Class IsMonoidPreserving (f : A -> B) :=
     { monmor_sgmor : IsSemiGroupPreserving f
     ; monmor_unitmor : IsUnitPreserving f }.
-  #[global] Existing Instances monmor_sgmor monmor_unitmor.
+  #[export] Existing Instances monmor_sgmor monmor_unitmor.
   End sgmorphism_classes.
 
   Section ringmorphism_classes.
@@ -291,13 +291,13 @@ Section morphism_classes.
         plus_is_sg_op plus_is_sg_op zero_is_mon_unit zero_is_mon_unit f
     ; semiringmor_mult_mor : @IsMonoidPreserving A B
         mult_is_sg_op mult_is_sg_op one_is_mon_unit one_is_mon_unit f }.
-  #[global] Existing Instances semiringmor_plus_mor semiringmor_mult_mor.
+  #[export] Existing Instances semiringmor_plus_mor semiringmor_mult_mor.
 
   Context {Aap : Apart A} {Bap : Apart B}.
   Class IsSemiRingStrongPreserving (f : A -> B) :=
     { strong_semiringmor_sr_mor : IsSemiRingPreserving f
     ; strong_semiringmor_strong_mor : StrongExtensionality f }.
-  #[global] Existing Instances strong_semiringmor_sr_mor strong_semiringmor_strong_mor.
+  #[export] Existing Instances strong_semiringmor_sr_mor strong_semiringmor_strong_mor.
   End ringmorphism_classes.
 
   Section latticemorphism_classes.
@@ -306,22 +306,22 @@ Section morphism_classes.
 
   Class IsJoinPreserving (f : A -> B) :=
     join_slmor_sgmor : @IsSemiGroupPreserving A B join_is_sg_op join_is_sg_op f.
-  #[global] Existing Instances join_slmor_sgmor.
+  #[export] Existing Instances join_slmor_sgmor.
 
   Class IsMeetPreserving (f : A -> B) :=
     meet_slmor_sgmor : @IsSemiGroupPreserving A B meet_is_sg_op meet_is_sg_op f.
-  #[global] Existing Instances meet_slmor_sgmor.
+  #[export] Existing Instances meet_slmor_sgmor.
 
   Context {Abottom : Bottom A} {Bbottom : Bottom B}.
   Class IsBoundedJoinPreserving (f : A -> B) := bounded_join_slmor_monmor
       : @IsMonoidPreserving A B join_is_sg_op join_is_sg_op
          bottom_is_mon_unit bottom_is_mon_unit f.
-  #[global] Existing Instances bounded_join_slmor_monmor.
+  #[export] Existing Instances bounded_join_slmor_monmor.
 
   Class IsLatticePreserving (f : A -> B) :=
     { latticemor_join_mor : IsJoinPreserving f
     ; latticemor_meet_mor : IsMeetPreserving f }.
-  #[global] Existing Instances
+  #[export] Existing Instances
     latticemor_join_mor
     latticemor_meet_mor.
   End latticemorphism_classes.
diff --git a/theories/Classes/interfaces/canonical_names.v b/theories/Classes/interfaces/canonical_names.v
index acb8976c41a..9a7cffece8d 100644
--- a/theories/Classes/interfaces/canonical_names.v
+++ b/theories/Classes/interfaces/canonical_names.v
@@ -46,7 +46,7 @@ Therefore we introduce the following class. *)
 Class TrivialApart A {Aap : Apart A} :=
   { trivial_apart_prop : is_mere_relation A apart
   ; trivial_apart : forall x y, x ≶ y <-> x <> y }.
-#[global] Existing Instance trivial_apart_prop.
+#[export] Existing Instance trivial_apart_prop.
 
 Definition sig_apart `{Apart A} (P: A -> Type) : Apart (sig P) := fun x y => x.1 ≶ y.1.
 #[export]
@@ -209,7 +209,7 @@ Arguments idempotency {A} _ _ {Idempotent}.
 
 Class UnaryIdempotent {A} (f: A -> A) : Type :=
   unary_idempotent : Idempotent Compose f.
-#[global] Existing Instances unary_idempotent.
+#[export] Existing Instances unary_idempotent.
 
 Lemma unary_idempotency `{UnaryIdempotent A f} x : f (f x) = f x.
 Proof.
@@ -221,7 +221,7 @@ Qed.
 
 Class BinaryIdempotent `(op: A -> A -> A) : Type
   := binary_idempotent : forall x, Idempotent op x.
-#[global] Existing Instances binary_idempotent.
+#[export] Existing Instances binary_idempotent.
 
 Class LeftIdentity {A B} (op : A -> B -> B) (x : A): Type
   := left_identity: forall y, op x y = y.
@@ -252,7 +252,7 @@ Class HeteroAssociative {A B C AB BC ABC}
   := associativity : forall x y z, fA_BC x (fBC y z) = fAB_C (fAB x y) z.
 Class Associative {A} (f : A -> A -> A)
   := simple_associativity : HeteroAssociative f f f f.
-#[global] Existing Instances simple_associativity.
+#[export] Existing Instances simple_associativity.
 
 Class Involutive {A} (f : A -> A) := involutive: forall x, f (f x) = x.
 
@@ -277,7 +277,7 @@ Class EquivRel `(R : Relation A) : Type := Build_EquivRel
   { EquivRel_Reflexive : Reflexive R ;
     EquivRel_Symmetric : Symmetric R ;
     EquivRel_Transitive : Transitive R }.
-#[global] Existing Instances EquivRel_Reflexive EquivRel_Symmetric EquivRel_Transitive.
+#[export] Existing Instances EquivRel_Reflexive EquivRel_Symmetric EquivRel_Transitive.
 
 Definition SigEquivRel {A:Type} (R : Relation A) : Type :=
   {_ : Reflexive R | { _ : Symmetric R | Transitive R}}.
@@ -326,10 +326,10 @@ Class RightHeteroDistribute {A B C}
   := distribute_r: forall a b c, f (g_l a b) c = g (f a c) (f b c).
 Class LeftDistribute {A} (f g: A -> A -> A)
   := simple_distribute_l : LeftHeteroDistribute f g g.
-#[global] Existing Instances simple_distribute_l.
+#[export] Existing Instances simple_distribute_l.
 Class RightDistribute {A} (f g: A -> A -> A)
   := simple_distribute_r : RightHeteroDistribute f g g.
-#[global] Existing Instances simple_distribute_r.
+#[export] Existing Instances simple_distribute_r.
 
 
 Class HeteroSymmetric {A} {T : A -> A -> Type}
@@ -416,7 +416,7 @@ Class Enumerable@{i} (A : Type@{i}) :=
   { enumerator : nat -> A
   ; enumerator_issurj :
     IsConnMap@{i} (trunc_S minus_two) enumerator }.
-#[global] Existing Instance enumerator_issurj.
+#[export] Existing Instance enumerator_issurj.
 Arguments enumerator A {_} _.
 Arguments enumerator_issurj A {_} _.
 
diff --git a/theories/Classes/interfaces/integers.v b/theories/Classes/interfaces/integers.v
index 1cbc3407a3f..bd808e0a784 100644
--- a/theories/Classes/interfaces/integers.v
+++ b/theories/Classes/interfaces/integers.v
@@ -15,7 +15,7 @@ Class Integers A {Aap:Apart A} {Aplus Amult Azero Aone Anegate Ale Alt}
   ; integers_to_ring_mor : forall {B} `{IsRing B}, IsSemiRingPreserving (integers_to_ring A B)
   ; integers_initial: forall {B} `{IsRing B} {h : A -> B} `{!IsSemiRingPreserving h} x,
       integers_to_ring A B x = h x}.
-#[global] Existing Instances integers_ring integers_order integers_to_ring_mor.
+#[export] Existing Instances integers_ring integers_order integers_to_ring_mor.
 
 Section specializable.
   Context (Z N : Type) `{Integers Z} `{Naturals N}.
diff --git a/theories/Classes/interfaces/naturals.v b/theories/Classes/interfaces/naturals.v
index f842fce1148..f6212d7ca16 100644
--- a/theories/Classes/interfaces/naturals.v
+++ b/theories/Classes/interfaces/naturals.v
@@ -15,7 +15,7 @@ Class Naturals A {Aap:Apart A} {Aplus Amult Azero Aone Ale Alt}
     IsSemiRingPreserving (naturals_to_semiring A B)
   ; naturals_initial: forall {B} `{IsSemiRing B} {h : A -> B} `{!IsSemiRingPreserving h} x,
     naturals_to_semiring A B x = h x }.
-#[global] Existing Instances naturals_ring naturals_order naturals_to_semiring_mor.
+#[export] Existing Instances naturals_ring naturals_order naturals_to_semiring_mor.
 
 (* Specializable operations: *)
 Class NatDistance N `{Plus N}
diff --git a/theories/Classes/interfaces/orders.v b/theories/Classes/interfaces/orders.v
index 16607dcca43..4e1b63c0995 100644
--- a/theories/Classes/interfaces/orders.v
+++ b/theories/Classes/interfaces/orders.v
@@ -24,7 +24,7 @@ Class PartialOrder `(Ale : Le A) :=
   ; po_hprop : is_mere_relation A Ale
   ; po_preorder : PreOrder (≤)
   ; po_antisym : AntiSymmetric (≤) }.
-#[global] Existing Instances
+#[export] Existing Instances
   po_hset
   po_hprop
   po_preorder
@@ -33,7 +33,7 @@ Class PartialOrder `(Ale : Le A) :=
 Class TotalOrder `(Ale : Le A) :=
   { total_order_po : PartialOrder (≤)
   ; total_order_total : TotalRelation (≤) }.
-#[global] Existing Instances
+#[export] Existing Instances
   total_order_po
   total_order_total.
 
@@ -51,25 +51,25 @@ Class MeetSemiLatticeOrder `(Ale : Le A) `{Meet A} :=
   ; meet_lb_l : forall x y, x ⊓ y ≤ x
   ; meet_lb_r : forall x y, x ⊓ y ≤ y
   ; meet_glb : forall x y z, z ≤ x -> z ≤ y -> z ≤ x ⊓ y }.
-#[global] Existing Instances meet_sl_order.
+#[export] Existing Instances meet_sl_order.
 
 Class JoinSemiLatticeOrder `(Ale : Le A) `{Join A} :=
   { join_sl_order : PartialOrder (≤)
   ; join_ub_l : forall x y, x ≤ x ⊔ y
   ; join_ub_r : forall x y, y ≤ x ⊔ y
   ; join_lub : forall x y z, x ≤ z -> y ≤ z -> x ⊔ y ≤ z }.
-#[global] Existing Instances join_sl_order.
+#[export] Existing Instances join_sl_order.
 
 Class LatticeOrder `(Ale : Le A) `{Meet A} `{Join A} :=
   { lattice_order_meet : MeetSemiLatticeOrder (≤)
   ; lattice_order_join : JoinSemiLatticeOrder (≤) }.
-#[global] Existing Instances lattice_order_meet lattice_order_join.
+#[export] Existing Instances lattice_order_meet lattice_order_join.
 
 Class StrictOrder `(Alt : Lt A) :=
   { strict_order_mere : is_mere_relation A lt
   ; strictorder_irrefl : Irreflexive (<)
   ; strictorder_trans : Transitive (<) }.
-#[global] Existing Instances strict_order_mere strictorder_irrefl strictorder_trans.
+#[export] Existing Instances strict_order_mere strictorder_irrefl strictorder_trans.
 
 (* The constructive notion of a total strict total order.
    We will prove that (<) is in fact a StrictOrder. *)
@@ -79,7 +79,7 @@ Class PseudoOrder `{Aap : Apart A} (Alt : Lt A) :=
   ; pseudo_order_antisym : forall x y, ~(x < y /\ y < x)
   ; pseudo_order_cotrans : CoTransitive (<)
   ; apart_iff_total_lt : forall x y, x ≶ y <-> x < y |_| y < x }.
-#[global] Existing Instances pseudo_order_mere_lt pseudo_order_cotrans.
+#[export] Existing Instances pseudo_order_mere_lt pseudo_order_cotrans.
 
 (* A partial order (≤) with a corresponding (<). We will prove that (<) is in fact
   a StrictOrder *)
@@ -89,7 +89,7 @@ Class FullPartialOrder `{Aap : Apart A} (Ale : Le A) (Alt : Lt A) :=
   ; strict_po_po : PartialOrder (≤)
   ; strict_po_trans : Transitive (<)
   ; lt_iff_le_apart : forall x y, x < y <-> x ≤ y /\ x ≶ y }.
-#[global] Existing Instances strict_po_po strict_po_trans.
+#[export] Existing Instances strict_po_po strict_po_trans.
 
 (* A pseudo order (<) with a corresponding (≤). We will prove that (≤) is in fact
   a PartialOrder. *)
@@ -97,7 +97,7 @@ Class FullPseudoOrder `{Aap : Apart A} (Ale : Le A) (Alt : Lt A) :=
   { fullpseudo_le_hprop : is_mere_relation A Ale
   ; full_pseudo_order_pseudo : PseudoOrder Alt
   ; le_iff_not_lt_flip : forall x y, x ≤ y <-> ~(y < x) }.
-#[global] Existing Instances fullpseudo_le_hprop full_pseudo_order_pseudo.
+#[export] Existing Instances fullpseudo_le_hprop full_pseudo_order_pseudo.
 
 Section order_maps.
   Context {A B : Type} {Ale: Le A} {Ble: Le B}(f : A -> B).
@@ -109,7 +109,7 @@ Section order_maps.
   Class OrderEmbedding :=
     { order_embedding_preserving : OrderPreserving
     ; order_embedding_reflecting : OrderReflecting }.
-  #[global] Existing Instances order_embedding_preserving order_embedding_reflecting.
+  #[export] Existing Instances order_embedding_preserving order_embedding_reflecting.
 End order_maps.
 
 Section srorder_maps.
@@ -124,7 +124,7 @@ Section srorder_maps.
   Class StrictOrderEmbedding :=
     { strict_order_embedding_preserving : StrictlyOrderPreserving
     ; strict_order_embedding_reflecting : StrictlyOrderReflecting }.
-  #[global] Existing Instances strict_order_embedding_preserving strict_order_embedding_reflecting.
+  #[export] Existing Instances strict_order_embedding_preserving strict_order_embedding_reflecting.
 End srorder_maps.
 
 #[export]
@@ -146,7 +146,7 @@ Class SemiRingOrder `{Plus A} `{Mult A}
   ; srorder_plus : forall z, OrderEmbedding (z +)
   ; nonneg_mult_compat : forall x y, PropHolds (0 ≤ x) -> PropHolds (0 ≤ y) ->
                                 PropHolds (0 ≤ x * y) }.
-#[global] Existing Instances srorder_po srorder_plus.
+#[export] Existing Instances srorder_po srorder_plus.
 
 Class StrictSemiRingOrder `{Plus A} `{Mult A}
     `{Zero A} `{One A} (Alt : Lt A) :=
@@ -155,7 +155,7 @@ Class StrictSemiRingOrder `{Plus A} `{Mult A}
   ; strict_srorder_plus : forall z, StrictOrderEmbedding (z +)
   ; pos_mult_compat : forall x y, PropHolds (0 < x) -> PropHolds (0 < y) ->
                              PropHolds (0 < x * y) }.
-#[global] Existing Instances strict_srorder_so strict_srorder_plus.
+#[export] Existing Instances strict_srorder_so strict_srorder_plus.
 
 Class PseudoSemiRingOrder `{Apart A} `{Plus A}
     `{Mult A} `{Zero A} `{One A} (Alt : Lt A) :=
@@ -165,14 +165,14 @@ Class PseudoSemiRingOrder `{Apart A} `{Plus A}
   ; pseudo_srorder_mult_ext : StrongBinaryExtensionality (.*.)
   ; pseudo_srorder_pos_mult_compat : forall x y, PropHolds (0 < x) -> PropHolds (0 < y) ->
                                             PropHolds (0 < x * y) }.
-#[global] Existing Instances pseudo_srorder_strict pseudo_srorder_plus pseudo_srorder_mult_ext.
+#[export] Existing Instances pseudo_srorder_strict pseudo_srorder_plus pseudo_srorder_mult_ext.
 
 Class FullPseudoSemiRingOrder `{Apart A} `{Plus A}
     `{Mult A} `{Zero A} `{One A} (Ale : Le A) (Alt : Lt A) :=
   { full_pseudo_srorder_le_hprop : is_mere_relation A Ale
   ; full_pseudo_srorder_pso : PseudoSemiRingOrder Alt
   ; full_pseudo_srorder_le_iff_not_lt_flip : forall x y, x ≤ y <-> ~(y < x) }.
-#[global] Existing Instances full_pseudo_srorder_le_hprop full_pseudo_srorder_pso.
+#[export] Existing Instances full_pseudo_srorder_le_hprop full_pseudo_srorder_pso.
 
 (* Due to bug #2528 *)
 #[export]
@@ -216,7 +216,7 @@ Class OrderedField (A : Type) {Alt : Lt A} {Ale : Le A} {Aap : Apart A} {Azero :
   ; ordered_field_lattice : LatticeOrder Ale
   ; ordered_field_fssro : @FullPseudoSemiRingOrder A _ _ _ Azero _ _ _
   }.
-#[global] Existing Instances
+#[export] Existing Instances
   ordered_field_field
   ordered_field_lattice
   ordered_field_fssro.
diff --git a/theories/Classes/interfaces/rationals.v b/theories/Classes/interfaces/rationals.v
index 9e8fcb85863..f45569c87aa 100644
--- a/theories/Classes/interfaces/rationals.v
+++ b/theories/Classes/interfaces/rationals.v
@@ -28,4 +28,4 @@ Class Rationals A {Aap : Apart A} {Aplus Amult Azero Aone Aneg Arecip Ale Alt}
   ; rationals_initial : forall {B} `{IsField B} `{!FieldCharacteristic B 0}
     {h : A -> B} `{!IsSemiRingPreserving h} x,
     rationals_to_field A B x = h x }.
-#[global] Existing Instances rationals_field rationals_order rationals_to_field_mor.
+#[export] Existing Instances rationals_field rationals_order rationals_to_field_mor.
diff --git a/theories/Classes/theory/premetric.v b/theories/Classes/theory/premetric.v
index fa0a568a108..44d689327d6 100644
--- a/theories/Classes/theory/premetric.v
+++ b/theories/Classes/theory/premetric.v
@@ -51,7 +51,7 @@ Class PreMetric@{i j} (A:Type@{i}) {Aclose : Closeness A} :=
   ; premetric_separated : Separated A
   ; premetric_triangular : Triangular A
   ; premetric_rounded : Rounded@{i j} A }.
-#[global] Existing Instances
+#[export] Existing Instances
   premetric_prop
   premetric_refl
   premetric_symm
diff --git a/theories/Diagrams/DDiagram.v b/theories/Diagrams/DDiagram.v
index 0143ba4bd8f..cae822eaba7 100644
--- a/theories/Diagrams/DDiagram.v
+++ b/theories/Diagrams/DDiagram.v
@@ -37,4 +37,4 @@ Definition DDiagram {G : Graph} (D : Diagram G)
     isequifibered i j (g : G i j) (x : D i)
       : IsEquiv (@arr _ E (i; x) (j; D _f g x) (g; idpath));
   }.
-  #[global] Existing Instance isequifibered.
+  #[export] Existing Instance isequifibered.
diff --git a/theories/Homotopy/CayleyDickson.v b/theories/Homotopy/CayleyDickson.v
index d5752a7cbe0..7f68705e8fd 100644
--- a/theories/Homotopy/CayleyDickson.v
+++ b/theories/Homotopy/CayleyDickson.v
@@ -22,7 +22,7 @@ Class CayleyDicksonSpheroid (X : pType) := {
   cds_swapop : SwapOp (-) cds_conjug;
   cds_factorneg_r : FactorNegRight (-) (.*.);
 }.
-#[global] Existing Instances
+#[export] Existing Instances
   cds_hspace
   cds_negate
   cds_conjug
@@ -91,7 +91,7 @@ Class CayleyDicksonImaginaroid (A : Type) := {
   cdi_susp_conjug_left_inv : LeftInverse hspace_op (conjugate_susp A cdi_negate) mon_unit;
   cdi_susp_conjug_distr : DistrOpp hspace_op (conjugate_susp A cdi_negate);
 }.
-#[global] Existing Instances
+#[export] Existing Instances
   cdi_negate
   cdi_negate_involutive
   cdi_susp_hspace
diff --git a/theories/Homotopy/HSpace.v b/theories/Homotopy/HSpace.v
index 1f7ea6b59b7..9a292629247 100644
--- a/theories/Homotopy/HSpace.v
+++ b/theories/Homotopy/HSpace.v
@@ -11,7 +11,7 @@ Class IsHSpace (X : pType) := {
   hspace_left_identity : LeftIdentity hspace_op (point _);
   hspace_right_identity : RightIdentity hspace_op (point _);
 }.
-#[global] Existing Instances hspace_left_identity hspace_right_identity hspace_op.
+#[export] Existing Instances hspace_left_identity hspace_right_identity hspace_op.
 
 Global Instance hspace_mon_unit {X : pType} `{IsHSpace X} : MonUnit X := point _.
 
diff --git a/theories/Sets/Ordinals.v b/theories/Sets/Ordinals.v
index 21e17178f70..01c663725c6 100644
--- a/theories/Sets/Ordinals.v
+++ b/theories/Sets/Ordinals.v
@@ -58,7 +58,7 @@ Class IsOrdinal@{carrier relation} (A : Type@{carrier}) (R : Relation@{carrier r
   ordinal_well_foundedness : WellFounded R ;
   ordinal_transitivity : Transitive R ;
 }.
-#[global] Existing Instances
+#[export] Existing Instances
   ordinal_is_hset
   ordinal_relation_is_mere
   ordinal_extensionality

From f6003ecb25a99f8af10746ff0a638dda9704277b Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Sat, 7 May 2022 20:54:15 +0100
Subject: [PATCH 4/4] Clean up newlines after #[global] attribute

---
 theories/Basics/Overture.v               | 9 +++------
 theories/Basics/UniverseLevel.v          | 6 ++----
 theories/Categories/Category/Morphisms.v | 3 +--
 theories/WildCat/Core.v                  | 6 ++----
 theories/WildCat/Opposite.v              | 3 +--
 5 files changed, 9 insertions(+), 18 deletions(-)

diff --git a/theories/Basics/Overture.v b/theories/Basics/Overture.v
index d02b6b03314..acb088c6db2 100644
--- a/theories/Basics/Overture.v
+++ b/theories/Basics/Overture.v
@@ -595,8 +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 *)
+#[global] Typeclasses Opaque IsTrunc. (* don't auto-unfold [IsTrunc] in typeclass search *)
 
 Arguments IsTrunc : simpl never. (* don't auto-unfold [IsTrunc] with [simpl] *)
 
@@ -734,8 +733,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.
+#[global] Typeclasses Opaque complement.
 
 Class Irreflexive {A} (R : Relation A) :=
   irreflexivity : Reflexive (complement R).
@@ -764,8 +762,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.
+#[global] Typeclasses Transparent IsPointed.
 
 Arguments point A {_}.
 
diff --git a/theories/Basics/UniverseLevel.v b/theories/Basics/UniverseLevel.v
index 7ba4e8e0618..dc3e1f5b4e4 100644
--- a/theories/Basics/UniverseLevel.v
+++ b/theories/Basics/UniverseLevel.v
@@ -19,8 +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] Typeclasses Opaque lift lower lift2 lower2.
 
 Global Instance isequiv_lift T : IsEquiv (@lift T)
   := @Build_IsEquiv
@@ -84,8 +83,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.
+#[global] Typeclasses Opaque lift' lower' lift'2 lower'2.
 
 Definition isequiv_lift'@{i j} (T : Type@{i}) : IsEquiv (@lift'@{i j} T)
   := @Build_IsEquiv
diff --git a/theories/Categories/Category/Morphisms.v b/theories/Categories/Category/Morphisms.v
index c3129d700e3..819513f32e5 100644
--- a/theories/Categories/Category/Morphisms.v
+++ b/theories/Categories/Category/Morphisms.v
@@ -248,8 +248,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.
+#[global] Typeclasses Transparent IsEpimorphism IsMonomorphism.
 
 Record Epimorphism {C} x y :=
   {
diff --git a/theories/WildCat/Core.v b/theories/WildCat/Core.v
index 997f32f293c..3dac7509ab5 100644
--- a/theories/WildCat/Core.v
+++ b/theories/WildCat/Core.v
@@ -74,8 +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.
+#[global] Typeclasses Transparent Is2Graph.
 
 (** ** Wild 1-categorical structures *)
 Class Is1Cat (A : Type) `{!IsGraph A, !Is2Graph A, !Is01Cat A} :=
@@ -398,8 +397,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.
+#[global] Typeclasses Transparent Is3Graph.
 
 (** *** Preservation of initial and terminal objects *)
 
diff --git a/theories/WildCat/Opposite.v b/theories/WildCat/Opposite.v
index 14b6de17a9a..8c8ae9fb99a 100644
--- a/theories/WildCat/Opposite.v
+++ b/theories/WildCat/Opposite.v
@@ -12,8 +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.
+#[global] Typeclasses Opaque op.
 
 Section Op.