diff --git a/examples/StateTMonad.v b/examples/StateTMonad.v
index fb8081a2..4b3a233d 100644
--- a/examples/StateTMonad.v
+++ b/examples/StateTMonad.v
@@ -8,7 +8,7 @@ Fail Definition foo : stateT unit option unit :=
   ret tt.
 
 (** Use [Existing Instance] to bring the Local [Monad_stateT] instance into context *)
-Existing Instance Monad_stateT.
+#[export] Existing Instance Monad_stateT.
 
 (** Now the definition succeeds *)
 Definition foo : stateT unit option unit :=
diff --git a/theories/Core/Any.v b/theories/Core/Any.v
index 299120b4..9cc0fed4 100644
--- a/theories/Core/Any.v
+++ b/theories/Core/Any.v
@@ -10,4 +10,5 @@ Polymorphic Definition RESOLVE (T : Type) : Type := T.
 
 Existing Class RESOLVE.
 
+#[global]
 Hint Extern 0 (RESOLVE _) => unfold RESOLVE : typeclass_instances.
diff --git a/theories/Data/Eq.v b/theories/Data/Eq.v
index 2dae4fe3..98c7b57a 100644
--- a/theories/Data/Eq.v
+++ b/theories/Data/Eq.v
@@ -28,6 +28,7 @@ Lemma match_eq_sym_eq
 Proof.
   destruct pf. reflexivity.
 Defined.
+#[global]
 Hint Rewrite match_eq_sym_eq : eq_rw.
 
 Lemma match_eq_sym_eq'
@@ -40,6 +41,7 @@ Lemma match_eq_sym_eq'
 Proof.
   destruct pf. reflexivity.
 Defined.
+#[global]
 Hint Rewrite match_eq_sym_eq' : eq_rw.
 
 
@@ -73,6 +75,7 @@ Lemma eq_Const_eq
 Proof.
   destruct pf. reflexivity.
 Defined.
+#[global]
 Hint Rewrite eq_Const_eq : eq_rw.
 
 Lemma eq_Arr_eq
@@ -88,11 +91,13 @@ Lemma eq_Arr_eq
 Proof.
   destruct pf. reflexivity.
 Defined.
+#[global]
 Hint Rewrite eq_Arr_eq : eq_rw.
 
 Lemma eq_sym_eq_sym : forall (T : Type) (a b : T) (pf : a = b),
                         eq_sym (eq_sym pf) = pf.
 Proof. destruct pf. reflexivity. Defined.
+#[global]
 Hint Rewrite eq_sym_eq_sym : eq_rw.
 
 Ltac autorewrite_eq_rw :=
diff --git a/theories/Data/ListFirstnSkipn.v b/theories/Data/ListFirstnSkipn.v
index ad5e284c..bae0e748 100644
--- a/theories/Data/ListFirstnSkipn.v
+++ b/theories/Data/ListFirstnSkipn.v
@@ -45,6 +45,7 @@ Proof.
   simpl. replace (n - 0) with n; [ | lia ]. reflexivity.
 Qed.
 
+#[global]
 Hint Rewrite firstn_app_L firstn_app_R firstn_all firstn_0 firstn_cons using lia : list_rw.
 
 Lemma skipn_app_R : forall T n (a b : list T),
@@ -90,4 +91,5 @@ Proof.
   simpl. replace (n - 0) with n; [ | lia ]. reflexivity.
 Qed.
 
+#[global]
 Hint Rewrite skipn_app_L skipn_app_R skipn_0 skipn_all skipn_cons using lia : list_rw.
diff --git a/theories/Data/Option.v b/theories/Data/Option.v
index 153c9b17..bdcedc79 100644
--- a/theories/Data/Option.v
+++ b/theories/Data/Option.v
@@ -180,4 +180,5 @@ Proof.
   destruct pf. destruct val; reflexivity.
 Defined.
 
+#[global]
 Hint Rewrite eq_option_eq : eq_rw.
diff --git a/theories/Data/PList.v b/theories/Data/PList.v
index b80dedfe..d8b9ff1f 100644
--- a/theories/Data/PList.v
+++ b/theories/Data/PList.v
@@ -216,6 +216,7 @@ End pmap.
 
 Polymorphic Definition Functor_plist@{i} : Functor@{i i} plist@{i} :=
 {| fmap := @fmap_plist@{i i} |}.
+#[global]
 Existing Instance Functor_plist.
 
 
diff --git a/theories/Data/POption.v b/theories/Data/POption.v
index 928f6463..ce2de987 100644
--- a/theories/Data/POption.v
+++ b/theories/Data/POption.v
@@ -80,9 +80,11 @@ End poption_map.
 
 Definition Functor_poption@{i} : Functor@{i i} poption@{i} :=
 {| fmap := @fmap_poption@{i i} |}.
+#[global]
 Existing Instance Functor_poption.
 
 Definition Applicative_poption@{i} : Applicative@{i i} poption@{i} :=
 {| pure := @pSome@{i}
  ; ap   := @ap_poption |}.
+#[global]
 Existing Instance Applicative_poption.
diff --git a/theories/Data/SigT.v b/theories/Data/SigT.v
index f452367f..c4cdda72 100644
--- a/theories/Data/SigT.v
+++ b/theories/Data/SigT.v
@@ -39,4 +39,5 @@ Lemma eq_sigT_rw
             end.
 Proof. destruct pf. destruct s; reflexivity. Qed.
 
+#[global]
 Hint Rewrite eq_sigT_rw : eq_rw.
diff --git a/theories/Generic/Ind.v b/theories/Generic/Ind.v
index 9c3763e4..2c2c6200 100644
--- a/theories/Generic/Ind.v
+++ b/theories/Generic/Ind.v
@@ -132,7 +132,9 @@ Ltac all_resolve :=
              | |- _ => solve [ eauto with typeclass_instances ]
            end.
 
+#[global]
 Hint Extern 0 (ProductResolve _ _) => all_resolve : typeclass_instances.
+#[global]
 Hint Extern 0 (VariantResolve _ _) => all_resolve : typeclass_instances.
 
 Definition comma_before (b : bool) (s : showM) : showM :=
diff --git a/theories/Programming/Eqv.v b/theories/Programming/Eqv.v
index 35547624..8bcd804a 100644
--- a/theories/Programming/Eqv.v
+++ b/theories/Programming/Eqv.v
@@ -9,6 +9,7 @@ Class EqvWF T :=
 { eqvWFEqv :> Eqv T
 ; eqvWFEquivalence :> Equivalence eqv
 }.
+#[global]
 Instance EqvWF_Build {T} {E:Eqv T} {EV:Equivalence eqv} : EqvWF T :=
   { eqvWFEqv := E ; eqvWFEquivalence := EV }.
 
diff --git a/theories/Programming/Injection.v b/theories/Programming/Injection.v
index 781e6953..14747c0d 100644
--- a/theories/Programming/Injection.v
+++ b/theories/Programming/Injection.v
@@ -9,10 +9,13 @@ Polymorphic Class Injection (x : Type) (t : Type) := inject : x -> t.
 Class Projection x t := { project : t -> x ; pmodify : (x -> x) -> (t -> t) }.
 *)
 
+#[global]
 Polymorphic Instance Injection_refl {T : Type} : Injection T T :=
 { inject := @id T }.
 
+#[global]
 Instance Injection_ascii_string : Injection ascii string :=
   { inject a := String a EmptyString }.
+#[global]
 Instance Injection_ascii_string_cons : Injection ascii (string -> string) :=
   { inject := String }.
diff --git a/theories/Programming/Le.v b/theories/Programming/Le.v
index 22231269..017fe04d 100644
--- a/theories/Programming/Le.v
+++ b/theories/Programming/Le.v
@@ -8,9 +8,11 @@ Definition neg_lte {T} {L:Lte T} (x:T) (y:T) : Prop := not (lte x y).
 Definition lt {T} {L:Lte T} x y := lte x y /\ ~lte y x.
 Definition neg_lt {T} {L:Lte T} x y := not (lt x y).
 
+#[global]
 Instance lt_RelDec {T} {L:Lte T} {RD:RelDec lte} : RelDec lt :=
   { rel_dec x y := (rel_dec x y && negb (rel_dec y x))%bool }.
 
+#[global]
 Instance lt_RelDecCorrect {T} {L:Lte T} {RD:RelDec lte} {RDC:RelDec_Correct RD}
   : RelDec_Correct lt_RelDec.
 Proof. constructor.
@@ -29,6 +31,7 @@ Class LteWF T :=
 ; lteWFPreOrder :> PreOrder lte
 }.
 
+#[global]
 Instance LteWF_Build {T} {L:Lte T} {PO:PreOrder lte} : LteWF T :=
   { lteWFLte := L ; lteWFPreOrder := PO }.
 
diff --git a/theories/Tactics/BoolTac.v b/theories/Tactics/BoolTac.v
index 06f46439..71d8de0e 100644
--- a/theories/Tactics/BoolTac.v
+++ b/theories/Tactics/BoolTac.v
@@ -3,6 +3,7 @@ Require Import Coq.Bool.Bool.
 Set Implicit Arguments.
 Set Strict Implicit.
 
+#[global]
 Hint Rewrite negb_orb negb_andb negb_involutive if_negb : bool_rw.
 
 Lemma negb_true : forall a, negb a = true -> a = false.
@@ -56,4 +57,4 @@ Proof.
   intros.
   do_bool.
 Abort.
-*)
\ No newline at end of file
+*)
diff --git a/theories/Tactics/Consider.v b/theories/Tactics/Consider.v
index 72b40fd0..8023752a 100644
--- a/theories/Tactics/Consider.v
+++ b/theories/Tactics/Consider.v
@@ -101,6 +101,7 @@ Section from_rel_dec.
   Qed.
 End from_rel_dec.
 
+#[global]
 Hint Extern 10 (@Reflect (?f ?a ?b) _ _) =>
   eapply (@Reflect_RelDecCorrect _ _ (@Build_RelDec _ _ f) _) : typeclass_instances.