Explicitly annotate all hint declarations of the standard library.

By default Coq stdlib warnings raise an error, so this is really required.

125 files changed, 752 insertions, 0 deletions

diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index 74d1e391c4..71c8f10755 100644
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.v
@@ -24,6 +24,7 @@ Section Between.
     | bet_emp : between k k
     | bet_S : forall l, between k l -> P l -> between k (S l).
 
+  #[local]
   Hint Constructors between: arith.
 
   Lemma bet_eq : forall k l, l = k -> between k l.
@@ -31,18 +32,21 @@ Section Between.
     intros * ->; auto with arith.
   Qed.
 
+  #[local]
   Hint Resolve bet_eq: arith.
 
   Lemma between_le : forall k l, between k l -> k <= l.
   Proof.
     induction 1; auto with arith.
   Qed.
+  #[local]
   Hint Immediate between_le: arith.
 
   Lemma between_Sk_l : forall k l, between k l -> S k <= l -> between (S k) l.
   Proof.
     induction 1 as [|* [|]]; auto with arith.
   Qed.
+  #[local]
   Hint Resolve between_Sk_l: arith.
 
   Lemma between_restr :
@@ -57,6 +61,7 @@ Section Between.
     | exists_S : forall l, exists_between k l -> exists_between k (S l)
     | exists_le : forall l, k <= l -> Q l -> exists_between k (S l).
 
+  #[local]
   Hint Constructors exists_between: arith.
 
   Lemma exists_le_S : forall k l, exists_between k l -> S k <= l.
@@ -66,12 +71,14 @@ Section Between.
 
   Lemma exists_lt : forall k l, exists_between k l -> k < l.
   Proof exists_le_S.
+  #[local]
   Hint Immediate exists_le_S exists_lt: arith.
 
   Lemma exists_S_le : forall k l, exists_between k (S l) -> k <= l.
   Proof.
     intros; apply le_S_n; auto with arith.
   Qed.
+  #[local]
   Hint Immediate exists_S_le: arith.
 
   Definition in_int p q r := p <= r /\ r < q.
@@ -80,6 +87,7 @@ Section Between.
   Proof.
     split; assumption.
   Qed.
+  #[local]
   Hint Resolve in_int_intro: arith.
 
   Lemma in_int_lt : forall p q r, in_int p q r -> p < q.
@@ -99,12 +107,14 @@ Section Between.
   Proof.
     intros * []; auto with arith.
   Qed.
+  #[local]
   Hint Resolve in_int_S: arith.
 
   Lemma in_int_Sp_q : forall p q r, in_int (S p) q r -> in_int p q r.
   Proof.
     intros * []; auto with arith.
   Qed.
+  #[local]
   Hint Immediate in_int_Sp_q: arith.
 
   Lemma between_in_int :
@@ -188,6 +198,8 @@ Section Between.
 
 End Between.
 
+#[global]
 Hint Resolve nth_O bet_S bet_emp bet_eq between_Sk_l exists_S exists_le
   in_int_S in_int_intro: arith.
+#[global]
 Hint Immediate in_int_Sp_q exists_le_S exists_S_le: arith.
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 2d34412908..c52edf9994 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -42,6 +42,7 @@ Qed.
 Lemma lt_div2 n : 0 < n -> div2 n < n.
 Proof. apply Nat.lt_div2. Qed.
 
+#[global]
 Hint Resolve lt_div2: arith.
 
 (** Properties related to the parity *)
@@ -73,6 +74,7 @@ Proof.
  symmetry in Ev'. elim (n_Sn _ Ev').
 Qed.
 
+#[global]
 Hint Resolve even_div2 div2_even odd_div2 div2_odd: arith.
 
 Lemma even_odd_div2 n :
@@ -88,6 +90,7 @@ Qed.
 
 Notation double := Nat.double (only parsing).
 
+#[global]
 Hint Unfold double Nat.double: arith.
 
 Lemma double_S n : double (S n) = S (S (double n)).
@@ -100,6 +103,7 @@ Proof.
   apply Nat.add_shuffle1.
 Qed.
 
+#[global]
 Hint Resolve double_S: arith.
 
 Lemma even_odd_double n :
@@ -133,6 +137,7 @@ Proof proj1 (proj2 (even_odd_double n)).
 Lemma double_odd n : n = S (double (div2 n)) -> odd n.
 Proof proj2 (proj2 (even_odd_double n)).
 
+#[global]
 Hint Resolve even_double double_even odd_double double_odd: arith.
 
 (** Application:
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index 593d8c5934..66678b24f8 100644
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -27,6 +27,7 @@ Theorem eq_nat_refl n : eq_nat n n.
 Proof.
   induction n; simpl; auto.
 Qed.
+#[global]
 Hint Resolve eq_nat_refl: arith.
 
 (** [eq] restricted to [nat] and [eq_nat] are equivalent *)
@@ -48,6 +49,7 @@ Proof.
  apply eq_nat_is_eq.
 Qed.
 
+#[global]
 Hint Immediate eq_eq_nat eq_nat_eq: arith.
 
 Theorem eq_nat_elim :
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index 3422596818..87d6a6ee64 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -31,7 +31,9 @@ Inductive even : nat -> Prop :=
 with odd : nat -> Prop :=
     odd_S : forall n, even n -> odd (S n).
 
+#[global]
 Hint Constructors even: arith.
+#[global]
 Hint Constructors odd: arith.
 
 (** * Equivalence with predicates [Nat.Even] and [Nat.odd] *)
@@ -178,6 +180,7 @@ Proof. parity_binop. Qed.
 Lemma odd_mult_inv_r n m : odd (n * m) -> odd m.
 Proof. parity_binop. Qed.
 
+#[global]
 Hint Resolve
  even_even_plus odd_even_plus odd_plus_l odd_plus_r
  even_mult_l even_mult_r even_mult_l even_mult_r odd_mult : arith.
diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v
index 05d585b9a2..492aeba66b 100644
--- a/theories/Arith/Gt.v
+++ b/theories/Arith/Gt.v
@@ -135,13 +135,21 @@ Qed.
 
 (** * Hints *)
 
+#[global]
 Hint Resolve gt_Sn_O gt_Sn_n gt_n_S : arith.
+#[global]
 Hint Immediate gt_S_n gt_pred : arith.
+#[global]
 Hint Resolve gt_irrefl gt_asym : arith.
+#[global]
 Hint Resolve le_not_gt gt_not_le : arith.
+#[global]
 Hint Immediate le_S_gt gt_S_le : arith.
+#[global]
 Hint Resolve gt_le_S le_gt_S : arith.
+#[global]
 Hint Resolve gt_trans_S le_gt_trans gt_le_trans: arith.
+#[global]
 Hint Resolve plus_gt_compat_l: arith.
 
 (* begin hide *)
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index 4e71465452..3d176fb644 100644
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -32,7 +32,9 @@ Notation le_refl := Nat.le_refl (only parsing).
 Notation le_trans := Nat.le_trans (only parsing).
 Notation le_antisym := Nat.le_antisymm (only parsing).
 
+#[global]
 Hint Resolve le_trans: arith.
+#[global]
 Hint Immediate le_antisym: arith.
 
 (** * Properties of [le] w.r.t 0 *)
@@ -61,8 +63,11 @@ Notation le_Sn_n := Nat.nle_succ_diag_l (only parsing). (* ~ S n <= n *)
 Theorem le_Sn_le : forall n m, S n <= m -> n <= m.
 Proof Nat.lt_le_incl.
 
+#[global]
 Hint Resolve le_0_n le_Sn_0: arith.
+#[global]
 Hint Resolve le_n_S le_n_Sn le_Sn_n : arith.
+#[global]
 Hint Immediate le_n_0_eq le_Sn_le le_S_n : arith.
 
 (** * Properties of [le] w.r.t predecessor *)
@@ -70,6 +75,7 @@ Hint Immediate le_n_0_eq le_Sn_le le_S_n : arith.
 Notation le_pred_n := Nat.le_pred_l (only parsing). (* pred n <= n *)
 Notation le_pred := Nat.pred_le_mono (only parsing). (* n<=m -> pred n <= pred m *)
 
+#[global]
 Hint Resolve le_pred_n: arith.
 
 (** * A different elimination principle for the order on natural numbers *)
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index 60cc361e35..467420afb3 100644
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -27,6 +27,7 @@ Local Open Scope nat_scope.
 
 Notation lt_irrefl := Nat.lt_irrefl (only parsing). (* ~ x < x *)
 
+#[global]
 Hint Resolve lt_irrefl: arith.
 
 (** * Relationship between [le] and [lt] *)
@@ -50,8 +51,11 @@ Qed.
 
 Register le_lt_n_Sm as num.nat.le_lt_n_Sm.
 
+#[global]
 Hint Immediate lt_le_S: arith.
+#[global]
 Hint Immediate lt_n_Sm_le: arith.
+#[global]
 Hint Immediate le_lt_n_Sm: arith.
 
 Theorem le_not_lt n m : n <= m -> ~ m < n.
@@ -64,6 +68,7 @@ Proof.
  apply Nat.lt_nge.
 Qed.
 
+#[global]
 Hint Immediate le_not_lt lt_not_le: arith.
 
 (** * Asymmetry *)
@@ -85,7 +90,9 @@ Proof.
  intros. now apply Nat.neq_sym, Nat.neq_0_lt_0.
 Qed.
 
+#[global]
 Hint Resolve lt_0_Sn lt_n_0 : arith.
+#[global]
 Hint Immediate neq_0_lt lt_0_neq: arith.
 
 (** * Order and successor *)
@@ -105,7 +112,9 @@ Qed.
 
 Register lt_S_n as num.nat.lt_S_n.
 
+#[global]
 Hint Resolve lt_n_Sn lt_S lt_n_S : arith.
+#[global]
 Hint Immediate lt_S_n : arith.
 
 (** * Predecessor *)
@@ -130,7 +139,9 @@ Proof.
  intros. now apply Nat.lt_pred_l, Nat.neq_0_lt_0.
 Qed.
 
+#[global]
 Hint Immediate lt_pred: arith.
+#[global]
 Hint Resolve lt_pred_n_n: arith.
 
 (** * Transitivity properties *)
@@ -141,6 +152,7 @@ Notation le_lt_trans := Nat.le_lt_trans (only parsing).
 
 Register le_lt_trans as num.nat.le_lt_trans.
 
+#[global]
 Hint Resolve lt_trans lt_le_trans le_lt_trans: arith.
 
 (** * Large = strict or equal *)
@@ -154,6 +166,7 @@ Qed.
 
 Notation lt_le_weak := Nat.lt_le_incl (only parsing).
 
+#[global]
 Hint Immediate lt_le_weak: arith.
 
 (** * Dichotomy *)
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index 28fe51f9af..863b02ef2e 100644
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -43,8 +43,10 @@ Notation max_case2 := max_case (only parsing).
 Notation max_SS := Nat.succ_max_distr (only parsing).
 (* end hide *)
 
+#[global]
 Hint Resolve
  Nat.max_l Nat.max_r Nat.le_max_l Nat.le_max_r : arith.
 
+#[global]
 Hint Resolve
  Nat.min_l Nat.min_r Nat.le_min_l Nat.le_min_r : arith.
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index b8c7ac147a..6cbba63e1a 100644
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -111,13 +111,23 @@ Qed.
 
 (** * Hints *)
 
+#[global]
 Hint Resolve minus_n_O: arith.
+#[global]
 Hint Resolve minus_Sn_m: arith.
+#[global]
 Hint Resolve minus_diag_reverse: arith.
+#[global]
 Hint Resolve minus_plus_simpl_l_reverse: arith.
+#[global]
 Hint Immediate plus_minus: arith.
+#[global]
 Hint Resolve minus_plus: arith.
+#[global]
 Hint Resolve le_plus_minus: arith.
+#[global]
 Hint Resolve le_plus_minus_r: arith.
+#[global]
 Hint Resolve lt_minus: arith.
+#[global]
 Hint Immediate lt_O_minus_lt: arith.
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index d7f703e6e4..584b282f4d 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -33,12 +33,14 @@ Notation mult_0_r := Nat.mul_0_r (only parsing). (* n * 0 = 0 *)
 Notation mult_1_l := Nat.mul_1_l (only parsing). (* 1 * n = n *)
 Notation mult_1_r := Nat.mul_1_r (only parsing). (* n * 1 = n *)
 
+#[global]
 Hint Resolve mult_1_l mult_1_r: arith.
 
 (** ** Commutativity *)
 
 Notation mult_comm := Nat.mul_comm (only parsing). (* n * m = m * n *)
 
+#[global]
 Hint Resolve mult_comm: arith.
 
 (** ** Distributivity *)
@@ -55,8 +57,11 @@ Notation mult_minus_distr_r :=
 Notation mult_minus_distr_l :=
   Nat.mul_sub_distr_l (only parsing). (* n*(m-p) = n*m - n*p *)
 
+#[global]
 Hint Resolve mult_plus_distr_r: arith.
+#[global]
 Hint Resolve mult_minus_distr_r: arith.
+#[global]
 Hint Resolve mult_minus_distr_l: arith.
 
 (** ** Associativity *)
@@ -68,7 +73,9 @@ Proof.
  symmetry. apply Nat.mul_assoc.
 Qed.
 
+#[global]
 Hint Resolve mult_assoc_reverse: arith.
+#[global]
 Hint Resolve mult_assoc: arith.
 
 (** ** Inversion lemmas *)
@@ -94,12 +101,14 @@ Lemma mult_O_le n m : m = 0 \/ n <= m * n.
 Proof.
  destruct m; [left|right]; simpl; trivial using Nat.le_add_r.
 Qed.
+#[global]
 Hint Resolve mult_O_le: arith.
 
 Lemma mult_le_compat_l n m p : n <= m -> p * n <= p * m.
 Proof.
  apply Nat.mul_le_mono_nonneg_l, Nat.le_0_l. (* TODO : get rid of 0<=n hyp *)
 Qed.
+#[global]
 Hint Resolve mult_le_compat_l: arith.
 
 Lemma mult_le_compat_r n m p : n <= m -> n * p <= m * p.
@@ -117,6 +126,7 @@ Proof.
   apply Nat.mul_lt_mono_pos_l, Nat.lt_0_succ.
 Qed.
 
+#[global]
 Hint Resolve mult_S_lt_compat_l: arith.
 
 Lemma mult_lt_compat_l n m p : n < m -> 0 < p -> p * n < p * m.
diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v
index 37704704a0..8d3b1b318a 100644
--- a/theories/Arith/PeanoNat.v
+++ b/theories/Arith/PeanoNat.v
@@ -765,7 +765,9 @@ Infix "?=" := Nat.compare (at level 70) : nat_scope.
 Infix "/" := Nat.div : nat_scope.
 Infix "mod" := Nat.modulo (at level 40, no associativity) : nat_scope.
 
+#[global]
 Hint Unfold Nat.le : core.
+#[global]
 Hint Unfold Nat.lt : core.
 
 Register Nat.le_trans as num.nat.le_trans.
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index 9a7a397023..2fc44ba592 100644
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -23,6 +23,7 @@ Defined.
 
 Notation eq_nat_dec := Nat.eq_dec (only parsing).
 
+#[global]
 Hint Resolve O_or_S eq_nat_dec: arith.
 
 Theorem dec_eq_nat n m : decidable (n = m).
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 5da7738adc..49e242276e 100644
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -179,11 +179,17 @@ Proof (succ_plus_discr n 3).
 
 (** * Compatibility Hints *)
 
+#[global]
 Hint Immediate plus_comm : arith.
+#[global]
 Hint Resolve plus_assoc plus_assoc_reverse : arith.
+#[global]
 Hint Resolve plus_le_compat_l plus_le_compat_r : arith.
+#[global]
 Hint Resolve le_plus_l le_plus_r le_plus_trans : arith.
+#[global]
 Hint Immediate lt_plus_trans : arith.
+#[global]
 Hint Resolve plus_lt_compat_l plus_lt_compat_r : arith.
 
 (** For compatibility, we "Require" the same files as before *)
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index ebd909c1dc..a87eeba9b1 100644
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -197,7 +197,9 @@ Proof.
   intros n H q; pattern q; apply lt_wf_ind; auto with arith.
 Qed.
 
+#[global]
 Hint Resolve lt_wf: arith.
+#[global]
 Hint Resolve well_founded_lt_compat: arith.
 
 Section LT_WF_REL.
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 0f62db42cf..8039c96efe 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -44,13 +44,16 @@ Lemma diff_true_false : true <> false.
 Proof.
   discriminate.
 Qed.
+#[global]
 Hint Resolve diff_true_false : bool.
 
 Lemma diff_false_true : false <> true.
 Proof.
   discriminate.
 Qed.
+#[global]
 Hint Resolve diff_false_true : bool.
+#[global]
 Hint Extern 1 (false <> true) => exact diff_false_true : core.
 
 Lemma eq_true_false_abs : forall b:bool, b = true -> b = false -> False.
@@ -87,6 +90,7 @@ Qed.
     | true => b2 = true
     | false => True
   end.
+#[global]
 Hint Unfold le: bool.
 
 Lemma le_implb : forall b1 b2, le b1 b2 <-> implb b1 b2 = true.
@@ -104,6 +108,7 @@ Notation leb_implb := le_implb (only parsing).
     | true => False
     | false => b2 = true
   end.
+#[global]
 Hint Unfold lt: bool.
 
 #[ local ] Definition compare (b1 b2 : bool) :=
@@ -271,6 +276,7 @@ Lemma orb_true_intro :
 Proof.
  intros; apply orb_true_iff; trivial.
 Qed.
+#[global]
 Hint Resolve orb_true_intro: bool.
 
 Lemma orb_false_intro :
@@ -278,6 +284,7 @@ Lemma orb_false_intro :
 Proof.
  intros. subst. reflexivity.
 Qed.
+#[global]
 Hint Resolve orb_false_intro: bool.
 
 Lemma orb_false_elim :
@@ -297,6 +304,7 @@ Lemma orb_true_r : forall b:bool, b || true = true.
 Proof.
   destr_bool.
 Qed.
+#[global]
 Hint Resolve orb_true_r: bool.
 
 Lemma orb_true_l : forall b:bool, true || b = true.
@@ -313,12 +321,14 @@ Lemma orb_false_r : forall b:bool, b || false = b.
 Proof.
   destr_bool.
 Qed.
+#[global]
 Hint Resolve orb_false_r: bool.
 
 Lemma orb_false_l : forall b:bool, false || b = b.
 Proof.
   destr_bool.
 Qed.
+#[global]
 Hint Resolve orb_false_l: bool.
 
 Notation orb_b_false := orb_false_r (only parsing).
@@ -330,6 +340,7 @@ Lemma orb_negb_r : forall b:bool, b || negb b = true.
 Proof.
   destr_bool.
 Qed.
+#[global]
 Hint Resolve orb_negb_r: bool.
 
 Lemma orb_negb_l : forall b:bool, negb b || b = true.
@@ -352,6 +363,7 @@ Lemma orb_assoc : forall b1 b2 b3:bool, b1 || (b2 || b3) = b1 || b2 || b3.
 Proof.
   destr_bool.
 Qed.
+#[global]
 Hint Resolve orb_comm orb_assoc: bool.
 
 (***************************)
@@ -426,6 +438,7 @@ Lemma andb_false_elim :
 Proof.
   intro b1; destruct b1; simpl; auto.
 Defined.
+#[global]
 Hint Resolve andb_false_elim: bool.
 
 (** Complementation *)
@@ -434,6 +447,7 @@ Lemma andb_negb_r : forall b:bool, b && negb b = false.
 Proof.
   destr_bool.
 Qed.
+#[global]
 Hint Resolve andb_negb_r: bool.
 
 Lemma andb_negb_l : forall b:bool, negb b && b = false.
@@ -457,6 +471,7 @@ Proof.
   destr_bool.
 Qed.
 
+#[global]
 Hint Resolve andb_comm andb_assoc: bool.
 
 (*****************************************)
@@ -722,6 +737,7 @@ Qed.
 
 Notation bool_6 := eq_true_not_negb (only parsing). (* Compatibility *)
 
+#[global]
 Hint Resolve eq_true_not_negb : bool.
 
 (* An interesting lemma for auto but too strong to keep compatibility *)
@@ -737,6 +753,7 @@ Lemma absurd_eq_true : forall b, False -> b = true.
 Proof.
   contradiction.
 Qed.
+#[global]
 Hint Resolve absurd_eq_true : core.
 
 (* A specific instance of eq_trans that preserves compatibility with
@@ -746,6 +763,7 @@ Lemma trans_eq_bool : forall x y z:bool, x = y -> y = z -> x = z.
 Proof.
   apply eq_trans.
 Qed.
+#[global]
 Hint Resolve trans_eq_bool : core.
 
 (***************************************)
@@ -754,6 +772,7 @@ Hint Resolve trans_eq_bool : core.
 
 (** [Is_true] and equality *)
 
+#[global]
 Hint Unfold Is_true: bool.
 
 Lemma Is_true_eq_true : forall x:bool, Is_true x -> x = true.
@@ -773,6 +792,7 @@ Qed.
 
 Notation Is_true_eq_true2 := Is_true_eq_right (only parsing).
 
+#[global]
 Hint Immediate Is_true_eq_right Is_true_eq_left: bool.
 
 Lemma eqb_refl : forall x:bool, Is_true (eqb x x).
@@ -806,6 +826,7 @@ Lemma andb_prop_intro :
 Proof.
   destr_bool; tauto.
 Qed.
+#[global]
 Hint Resolve andb_prop_intro: bool.
 
 Notation andb_true_intro2 :=
@@ -817,6 +838,7 @@ Lemma andb_prop_elim :
 Proof.
   destr_bool; auto.
 Qed.
+#[global]
 Hint Resolve andb_prop_elim: bool.
 
 Notation andb_prop2 := andb_prop_elim (only parsing).
@@ -901,6 +923,7 @@ Qed.
 Inductive reflect (P : Prop) : bool -> Set :=
   | ReflectT : P -> reflect P true
   | ReflectF : ~ P -> reflect P false.
+#[global]
 Hint Constructors reflect : bool.
 
 (** Interest: a case on a reflect lemma or hyp performs clever
diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v
index 1a41eb6bb5..7e9087c377 100644
--- a/theories/Bool/IfProp.v
+++ b/theories/Bool/IfProp.v
@@ -14,6 +14,7 @@ Inductive IfProp (A B:Prop) : bool -> Prop :=
   | Iftrue : A -> IfProp A B true
   | Iffalse : B -> IfProp A B false.
 
+#[global]
 Hint Resolve Iftrue Iffalse: bool.
 
 Lemma Iftrue_inv : forall (A B:Prop) (b:bool), IfProp A B b -> b = true -> A.
diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v
index 52605a4667..49feda15ea 100644
--- a/theories/Bool/Sumbool.v
+++ b/theories/Bool/Sumbool.v
@@ -19,6 +19,7 @@ Definition sumbool_of_bool : forall b:bool, {b = true} + {b = false}.
   intros b; destruct b; auto.
 Defined.
 
+#[global]
 Hint Resolve sumbool_of_bool: bool.
 
 Definition bool_eq_rec :
@@ -57,7 +58,9 @@ Section connectives.
 
 End connectives.
 
+#[global]
 Hint Resolve sumbool_and sumbool_or: core.
+#[global]
 Hint Immediate sumbool_not : core.
 
 (** Any decidability function in type [sumbool] can be turned into a function
diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v
index 3665a8c78d..aff5008410 100644
--- a/theories/Bool/Zerob.v
+++ b/theories/Bool/Zerob.v
@@ -23,6 +23,7 @@ Lemma zerob_true_intro : forall n:nat, n = 0 -> zerob n = true.
 Proof.
   destruct n; [ trivial with bool | inversion 1 ].
 Qed.
+#[global]
 Hint Resolve zerob_true_intro: bool.
 
 Lemma zerob_true_elim : forall n:nat, zerob n = true -> n = 0.
@@ -34,6 +35,7 @@ Lemma zerob_false_intro : forall n:nat, n <> 0 -> zerob n = false.
 Proof.
   destruct n; [ destruct 1; auto with bool | trivial with bool ].
 Qed.
+#[global]
 Hint Resolve zerob_false_intro: bool.
 
 Lemma zerob_false_elim : forall n:nat, zerob n = false -> n <> 0.
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index 9a3a1d3709..892568c3d8 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -80,9 +80,11 @@ End Proper.
 (** We favor the use of Leibniz equality or a declared reflexive crelation 
   when resolving [ProperProxy], otherwise, if the crelation is given (not an evar),
   we fall back to [Proper]. *)
+#[global]
 Hint Extern 1 (ProperProxy _ _) => 
   class_apply @eq_proper_proxy || class_apply @reflexive_proper_proxy : typeclass_instances.
 
+#[global]
 Hint Extern 2 (ProperProxy ?R _) => 
   not_evar R; class_apply @proper_proper_proxy : typeclass_instances.
 
@@ -215,8 +217,11 @@ Typeclasses Opaque respectful pointwise_relation forall_relation.
 Arguments forall_relation {A P}%type sig%signature _ _.
 Arguments pointwise_relation A%type {B}%type R%signature _ _.
   
+#[global]
 Hint Unfold Reflexive : core.
+#[global]
 Hint Unfold Symmetric : core.
+#[global]
 Hint Unfold Transitive : core.
 
 (** Resolution with subrelation: favor decomposing products over applying reflexivity
@@ -225,6 +230,7 @@ Ltac subrelation_tac T U :=
   (is_ground T ; is_ground U ; class_apply @subrelation_refl) ||
     class_apply @subrelation_respectful || class_apply @subrelation_refl.
 
+#[global]
 Hint Extern 3 (@subrelation _ ?T ?U) => subrelation_tac T U : typeclass_instances.
 
 CoInductive apply_subrelation : Prop := do_subrelation.
@@ -234,6 +240,7 @@ Ltac proper_subrelation :=
     [ H : apply_subrelation |- _ ] => clear H ; class_apply @subrelation_proper
   end.
 
+#[global]
 Hint Extern 5 (@Proper _ ?H _) => proper_subrelation : typeclass_instances.
 
 (** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *)
@@ -254,6 +261,7 @@ Proof. firstorder. Qed.
 
 (** We use an extern hint to help unification. *)
 
+#[global]
 Hint Extern 4 (subrelation (@forall_relation ?A ?B ?R) (@forall_relation _ _ ?S)) =>
   apply (@forall_subrelation A B R S) ; intro : typeclass_instances.
 
@@ -526,17 +534,23 @@ Ltac proper_reflexive :=
   end.
 
 
+#[global]
 Hint Extern 1 (subrelation (flip _) _) => class_apply @flip1 : typeclass_instances.
+#[global]
 Hint Extern 1 (subrelation _ (flip _)) => class_apply @flip2 : typeclass_instances.
 
 (* Hint Extern 1 (Proper _ (complement _)) => apply @complement_proper  *)
 (*   : typeclass_instances. *)
+#[global]
 Hint Extern 1 (Proper _ (flip _)) => apply @flip_proper 
   : typeclass_instances.
+#[global]
 Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_flip_proper 
   : typeclass_instances.
+#[global]
 Hint Extern 4 (@Proper _ _ _) => partial_application_tactic 
   : typeclass_instances.
+#[global]
 Hint Extern 7 (@Proper _ _ _) => proper_reflexive 
   : typeclass_instances.
 
@@ -586,7 +600,9 @@ Ltac proper_normalization :=
       set(H:=did_normalization) ; class_apply @proper_normalizes_proper
   end.
 
+#[global]
 Hint Extern 1 (Normalizes _ _ _) => normalizes : typeclass_instances.
+#[global]
 Hint Extern 6 (@Proper _ _ _) => proper_normalization 
   : typeclass_instances.
 
@@ -690,6 +706,7 @@ split.
   + right. transitivity y; auto.
 Qed.
 
+#[global]
 Hint Extern 4 (PreOrder (relation_disjunction _ _)) => 
   class_apply StrictOrder_PreOrder : typeclass_instances.
 
@@ -702,8 +719,10 @@ elim (StrictOrder_Irreflexive x).
 transitivity y; auto.
 Qed.
 
+#[global]
 Hint Extern 4 (StrictOrder (relation_conjunction _ _)) => 
   class_apply PartialOrder_StrictOrder : typeclass_instances.
 
+#[global]
 Hint Extern 4 (PartialOrder _ (relation_disjunction _ _)) => 
   class_apply StrictOrder_PartialOrder : typeclass_instances.
diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v
index 72a196ca7a..236d35b68e 100644
--- a/theories/Classes/CRelationClasses.v
+++ b/theories/Classes/CRelationClasses.v
@@ -203,22 +203,35 @@ Defined.
 
 (** Hints to drive the typeclass resolution avoiding loops
  due to the use of full unification. *)
+#[global]
 Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclass_instances.
+#[global]
 Hint Extern 3 (Symmetric (complement _)) => class_apply complement_Symmetric : typeclass_instances.
+#[global]
 Hint Extern 3 (Irreflexive (complement _)) => class_apply complement_Irreflexive : typeclass_instances.
 
+#[global]
 Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances.
+#[global]
 Hint Extern 3 (Irreflexive (flip _)) => class_apply flip_Irreflexive : typeclass_instances.
+#[global]
 Hint Extern 3 (Symmetric (flip _)) => class_apply flip_Symmetric : typeclass_instances.
+#[global]
 Hint Extern 3 (Asymmetric (flip _)) => class_apply flip_Asymmetric : typeclass_instances.
+#[global]
 Hint Extern 3 (Antisymmetric (flip _)) => class_apply flip_Antisymmetric : typeclass_instances.
+#[global]
 Hint Extern 3 (Transitive (flip _)) => class_apply flip_Transitive : typeclass_instances.
+#[global]
 Hint Extern 3 (StrictOrder (flip _)) => class_apply flip_StrictOrder : typeclass_instances.
+#[global]
 Hint Extern 3 (PreOrder (flip _)) => class_apply flip_PreOrder : typeclass_instances.
 
+#[global]
 Hint Extern 4 (subrelation (flip _) _) => 
   class_apply @subrelation_symmetric : typeclass_instances.
 
+#[global]
 Hint Resolve irreflexivity : ord.
 
 Unset Implicit Arguments.
@@ -231,6 +244,7 @@ Ltac solve_crelation :=
   | [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H
   end.
 
+#[global]
 Hint Extern 4 => solve_crelation : crelations.
 
 (** We can already dualize all these properties. *)
@@ -351,6 +365,7 @@ Section Binary.
   Qed.
 End Binary.
 
+#[global]
 Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : typeclass_instances.
 
 (** The partial order defined by subrelation and crelation equivalence. *)
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index 394f5dc4de..9ca465bbfd 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -36,4 +36,5 @@ Ltac unconvertible :=
     | |- _ => exact tt
   end.
 
+#[global]
 Hint Extern 0 (@Unconvertible _ _ _) => unconvertible : typeclass_instances.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index c70e3fe478..ffbea7dddf 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -81,9 +81,11 @@ End Proper.
 (** We favor the use of Leibniz equality or a declared reflexive relation 
   when resolving [ProperProxy], otherwise, if the relation is given (not an evar),
   we fall back to [Proper]. *)
+#[global]
 Hint Extern 1 (ProperProxy _ _) => 
   class_apply @eq_proper_proxy || class_apply @reflexive_proper_proxy : typeclass_instances.
 
+#[global]
 Hint Extern 2 (ProperProxy ?R _) => 
   not_evar R; class_apply @proper_proper_proxy : typeclass_instances.
 
@@ -213,8 +215,11 @@ Typeclasses Opaque respectful pointwise_relation forall_relation.
 Arguments forall_relation {A P}%type sig%signature _ _.
 Arguments pointwise_relation A%type {B}%type R%signature _ _.
   
+#[global]
 Hint Unfold Reflexive : core.
+#[global]
 Hint Unfold Symmetric : core.
+#[global]
 Hint Unfold Transitive : core.
 
 (** Resolution with subrelation: favor decomposing products over applying reflexivity
@@ -223,6 +228,7 @@ Ltac subrelation_tac T U :=
   (is_ground T ; is_ground U ; class_apply @subrelation_refl) ||
     class_apply @subrelation_respectful || class_apply @subrelation_refl.
 
+#[global]
 Hint Extern 3 (@subrelation _ ?T ?U) => subrelation_tac T U : typeclass_instances.
 
 CoInductive apply_subrelation : Prop := do_subrelation.
@@ -232,6 +238,7 @@ Ltac proper_subrelation :=
     [ H : apply_subrelation |- _ ] => clear H ; class_apply @subrelation_proper
   end.
 
+#[global]
 Hint Extern 5 (@Proper _ ?H _) => proper_subrelation : typeclass_instances.
 
 (** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *)
@@ -244,6 +251,7 @@ Proof. firstorder. Qed.
 
 (** We use an extern hint to help unification. *)
 
+#[global]
 Hint Extern 4 (subrelation (@forall_relation ?A ?B ?R) (@forall_relation _ _ ?S)) =>
   apply (@forall_subrelation A B R S) ; intro : typeclass_instances.
 
@@ -538,17 +546,24 @@ Ltac proper_reflexive :=
   end.
 
 
+#[global]
 Hint Extern 1 (subrelation (flip _) _) => class_apply @flip1 : typeclass_instances.
+#[global]
 Hint Extern 1 (subrelation _ (flip _)) => class_apply @flip2 : typeclass_instances.
 
+#[global]
 Hint Extern 1 (Proper _ (complement _)) => apply @complement_proper 
   : typeclass_instances.
+#[global]
 Hint Extern 1 (Proper _ (flip _)) => apply @flip_proper 
   : typeclass_instances.
+#[global]
 Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_flip_proper 
   : typeclass_instances.
+#[global]
 Hint Extern 4 (@Proper _ _ _) => partial_application_tactic 
   : typeclass_instances.
+#[global]
 Hint Extern 7 (@Proper _ _ _) => proper_reflexive 
   : typeclass_instances.
 
@@ -603,7 +618,9 @@ Ltac proper_normalization :=
       set(H:=did_normalization) ; class_apply @proper_normalizes_proper
   end.
 
+#[global]
 Hint Extern 1 (Normalizes _ _ _) => normalizes : typeclass_instances.
+#[global]
 Hint Extern 6 (@Proper _ _ _) => proper_normalization 
   : typeclass_instances.
 
@@ -693,6 +710,7 @@ split.
   + right. transitivity y; auto.
 Qed.
 
+#[global]
 Hint Extern 4 (PreOrder (relation_disjunction _ _)) => 
   class_apply StrictOrder_PreOrder : typeclass_instances.
 
@@ -705,8 +723,10 @@ elim (StrictOrder_Irreflexive x).
 transitivity y; auto.
 Qed.
 
+#[global]
 Hint Extern 4 (StrictOrder (relation_conjunction _ _)) => 
   class_apply PartialOrder_StrictOrder : typeclass_instances.
 
+#[global]
 Hint Extern 4 (PartialOrder _ (relation_disjunction _ _)) => 
   class_apply StrictOrder_PartialOrder : typeclass_instances.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 5381e91997..d8246c22e1 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -196,19 +196,31 @@ Defined.
 
 (** Hints to drive the typeclass resolution avoiding loops
  due to the use of full unification. *)
+#[global]
 Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclass_instances.
+#[global]
 Hint Extern 3 (Symmetric (complement _)) => class_apply complement_Symmetric : typeclass_instances.
+#[global]
 Hint Extern 3 (Irreflexive (complement _)) => class_apply complement_Irreflexive : typeclass_instances.
 
+#[global]
 Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances.
+#[global]
 Hint Extern 3 (Irreflexive (flip _)) => class_apply flip_Irreflexive : typeclass_instances.
+#[global]
 Hint Extern 3 (Symmetric (flip _)) => class_apply flip_Symmetric : typeclass_instances.
+#[global]
 Hint Extern 3 (Asymmetric (flip _)) => class_apply flip_Asymmetric : typeclass_instances.
+#[global]
 Hint Extern 3 (Antisymmetric (flip _)) => class_apply flip_Antisymmetric : typeclass_instances.
+#[global]
 Hint Extern 3 (Transitive (flip _)) => class_apply flip_Transitive : typeclass_instances.
+#[global]
 Hint Extern 3 (StrictOrder (flip _)) => class_apply flip_StrictOrder : typeclass_instances.
+#[global]
 Hint Extern 3 (PreOrder (flip _)) => class_apply flip_PreOrder : typeclass_instances.
 
+#[global]
 Hint Extern 4 (subrelation (flip _) _) => 
   class_apply @subrelation_symmetric : typeclass_instances.
 
@@ -218,6 +230,7 @@ Arguments asymmetry {A} {R} {_} [x] [y] _ _.
 Arguments transitivity {A} {R} {_} [x] [y] [z] _ _.
 Arguments Antisymmetric A eqA {_} _.
 
+#[global]
 Hint Resolve irreflexivity : ord.
 
 Unset Implicit Arguments.
@@ -230,6 +243,7 @@ Ltac solve_relation :=
   | [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H
   end.
 
+#[global]
 Hint Extern 4 => solve_relation : relations.
 
 (** We can already dualize all these properties. *)
@@ -476,6 +490,7 @@ Section Binary.
   Proof. firstorder. Qed.
 End Binary.
 
+#[global]
 Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : typeclass_instances.
 
 (** The partial order defined by subrelation and relation equivalence. *)
diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v
index b4034b9cf9..afe69cae7f 100644
--- a/theories/Classes/RelationPairs.v
+++ b/theories/Classes/RelationPairs.v
@@ -160,6 +160,8 @@ Section RelProd_Instances.
   Proof. unfold RelCompFun; firstorder. Qed.
 End RelProd_Instances.
 
+#[global]
 Hint Unfold RelProd RelCompFun : core.
+#[global]
 Hint Extern 2 (RelProd _ _ _ _) => split : core.
 
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index ad0124db6d..bfa50d7fae 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -41,6 +41,7 @@ Local Open Scope Int_scope.
 Local Notation int := I.t.
 
 Definition key := X.t.
+#[global]
 Hint Transparent key : core.
 
 (** * Trees *)
@@ -495,7 +496,9 @@ Functional Scheme map2_opt_ind := Induction for map2_opt Sort Prop.
 
 (** * Automation and dedicated tactics. *)
 
+#[global]
 Hint Constructors tree MapsTo In bst : core.
+#[global]
 Hint Unfold lt_tree gt_tree : core.
 
 Tactic Notation "factornode" ident(l) ident(x) ident(d) ident(r) ident(h)
@@ -576,6 +579,7 @@ Lemma MapsTo_In : forall k e m, MapsTo k e m -> In k m.
 Proof.
  induction 1; auto.
 Qed.
+#[local]
 Hint Resolve MapsTo_In : core.
 
 Lemma In_MapsTo : forall k m, In k m -> exists e, MapsTo k e m.
@@ -595,6 +599,7 @@ Lemma MapsTo_1 :
 Proof.
  induction m; simpl; intuition_in; eauto with ordered_type.
 Qed.
+#[local]
 Hint Immediate MapsTo_1 : core.
 
 Lemma In_1 :
@@ -634,6 +639,7 @@ Proof.
  unfold gt_tree in *; intuition_in; order.
 Qed.
 
+#[local]
 Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node : core.
 
 Lemma lt_left : forall x y l r e h,
@@ -660,6 +666,7 @@ Proof.
  intuition_in.
 Qed.
 
+#[local]
 Hint Resolve lt_left lt_right gt_left gt_right : core.
 
 Lemma lt_tree_not_in :
@@ -686,6 +693,7 @@ Proof.
  eauto with ordered_type.
 Qed.
 
+#[local]
 Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans : core.
 
 (** * Empty map *)
@@ -818,6 +826,7 @@ Lemma create_bst :
 Proof.
  unfold create; auto.
 Qed.
+#[local]
 Hint Resolve create_bst : core.
 
 Lemma create_in :
@@ -835,6 +844,7 @@ Proof.
  (apply lt_tree_node || apply gt_tree_node); auto with ordered_type;
  (eapply lt_tree_trans || eapply gt_tree_trans); eauto with ordered_type.
 Qed.
+#[local]
 Hint Resolve bal_bst : core.
 
 Lemma bal_in : forall l x e r y,
@@ -876,6 +886,7 @@ Proof.
  apply MX.eq_lt with x; auto.
  apply MX.lt_eq with x; auto with ordered_type.
 Qed.
+#[local]
 Hint Resolve add_bst : core.
 
 Lemma add_1 : forall m x y e, X.eq x y -> MapsTo y e (add x e m).
@@ -956,6 +967,7 @@ Proof.
  destruct 1.
  apply H2; intuition.
 Qed.
+#[local]
 Hint Resolve remove_min_bst : core.
 
 Lemma remove_min_gt_tree : forall l x e r h,
@@ -975,6 +987,7 @@ Proof.
  assert (X.lt m#1 x) by order.
  decompose [or] H; order.
 Qed.
+#[local]
 Hint Resolve remove_min_gt_tree : core.
 
 Lemma remove_min_find : forall l x e r h y,
@@ -1127,6 +1140,7 @@ Proof.
  intuition; [ apply MX.lt_eq with x | ]; eauto with ordered_type.
  intuition; [ apply MX.eq_lt with x | ]; eauto with ordered_type.
 Qed.
+#[local]
 Hint Resolve join_bst : core.
 
 Lemma join_find : forall l x d r y,
@@ -1263,6 +1277,7 @@ Proof.
  rewrite remove_min_in, e1; simpl; auto with ordered_type.
  change (gt_tree (m2',xd)#2#1 (m2',xd)#1). rewrite <-e1; eauto.
 Qed.
+#[local]
 Hint Resolve concat_bst : core.
 
 Lemma concat_find : forall m1 m2 y, bst m1 -> bst m2 ->
@@ -1351,6 +1366,7 @@ Proof.
  intros; unfold elements; apply elements_aux_sort; auto.
  intros; inversion H0.
 Qed.
+#[local]
 Hint Resolve elements_sort : core.
 
 Lemma elements_nodup : forall s : t elt, bst s -> NoDupA eqk (elements s).
@@ -1620,6 +1636,7 @@ destruct (map_option_2 H) as (d0 & ? & ?).
 destruct (map_option_2 H') as (d0' & ? & ?).
 eapply X.lt_trans with x; eauto using MapsTo_In.
 Qed.
+#[local]
 Hint Resolve map_option_bst : core.
 
 Ltac nonify e :=
@@ -1719,6 +1736,7 @@ apply X.lt_trans with x1.
 destruct (map2_opt_2 H1 H6 Hy); intuition.
 destruct (map2_opt_2 H2 H7 Hy'); intuition.
 Qed.
+#[local]
 Hint Resolve map2_opt_bst : core.
 
 Ltac map2_aux :=
@@ -2075,6 +2093,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
   Proof.
    destruct c; simpl; intros; P.MX.elim_comp; auto with ordered_type.
   Qed.
+  #[global]
   Hint Resolve cons_Cmp : core.
 
   Lemma compare_end_Cmp :
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 2001201ec3..bb52166ca7 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -20,6 +20,7 @@ Require Export FMapInterface.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+#[global]
 Hint Extern 1 (Equivalence _) => constructor; congruence : core.
 
 (** * Facts about weak maps *)
@@ -371,6 +372,7 @@ Proof.
 intros. rewrite eq_option_alt. intro e'. rewrite <- 2 find_mapsto_iff.
 apply add_neq_mapsto_iff; auto.
 Qed.
+#[local]
 Hint Resolve add_neq_o : map.
 
 Lemma add_o : forall m x y e,
@@ -404,6 +406,7 @@ Proof.
 intros. rewrite eq_option_alt. intro e.
 rewrite <- find_mapsto_iff, remove_mapsto_iff; now intuition.
 Qed.
+#[local]
 Hint Resolve remove_eq_o : map.
 
 Lemma remove_neq_o : forall m x y,
@@ -412,6 +415,7 @@ Proof.
 intros. rewrite eq_option_alt. intro e.
 rewrite <- find_mapsto_iff, remove_neq_mapsto_iff; now intuition.
 Qed.
+#[local]
 Hint Resolve remove_neq_o : map.
 
 Lemma remove_o : forall m x y,
@@ -1100,6 +1104,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   contradict Hnotin; rewrite <- Hnotin; exists e0; auto.
   Qed.
 
+  #[local]
   Hint Resolve NoDupA_eqk_eqke NoDupA_rev elements_3w : map.
 
   Lemma fold_Equal : forall m1 m2 i, Equal m1 m2 ->
@@ -1232,6 +1237,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   Proof.
   intros; rewrite cardinal_Empty; auto.
   Qed.
+  #[local]
   Hint Resolve cardinal_inv_1 : map.
 
   Lemma cardinal_inv_2 :
@@ -1846,6 +1852,7 @@ Module OrdProperties (M:S).
    unfold leb; f_equal; apply gtb_compat; auto.
   Qed.
 
+  #[local]
   Hint Resolve gtb_compat leb_compat elements_3 : map.
 
   Lemma elements_split : forall p m,
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v
index 03e8d270e9..d26510ab9d 100644
--- a/theories/FSets/FMapFullAVL.v
+++ b/theories/FSets/FMapFullAVL.v
@@ -63,6 +63,7 @@ Inductive avl : t elt -> Prop :=
 
 (** * Automation and dedicated tactics about [avl]. *)
 
+#[local]
 Hint Constructors avl : core.
 
 Lemma height_non_negative : forall (s : t elt), avl s ->
@@ -100,6 +101,7 @@ Lemma avl_node : forall x e l r, avl l -> avl r ->
 Proof.
   intros; auto.
 Qed.
+#[local]
 Hint Resolve avl_node : core.
 
 (** Results about [height] *)
@@ -193,6 +195,7 @@ Lemma add_avl : forall m x e, avl m -> avl (add x e m).
 Proof.
  intros; generalize (add_avl_1 x e H); intuition.
 Qed.
+#[local]
 Hint Resolve add_avl : core.
 
 (** * Extraction of minimum binding *)
@@ -274,6 +277,7 @@ Lemma remove_avl : forall m x, avl m -> avl (remove x m).
 Proof.
  intros; generalize (remove_avl_1 x H); intuition.
 Qed.
+#[local]
 Hint Resolve remove_avl : core.
 
 
@@ -331,6 +335,7 @@ Lemma join_avl : forall l x d r, avl l -> avl r -> avl (join l x d r).
 Proof.
  intros; destruct (join_avl_1 x d H H0); auto.
 Qed.
+#[local]
 Hint Resolve join_avl : core.
 
 (** concat *)
@@ -341,6 +346,7 @@ Proof.
  intros; apply join_avl; auto.
  generalize (remove_min_avl H0); rewrite e1; simpl; auto.
 Qed.
+#[local]
 Hint Resolve concat_avl : core.
 
 (** split *)
@@ -355,6 +361,7 @@ Proof.
 Qed.
 
 End Elt.
+#[global]
 Hint Constructors avl : core.
 
 Section Map.
@@ -714,6 +721,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
   Proof.
    destruct c; simpl; intros; MX.elim_comp; auto with ordered_type.
   Qed.
+  #[global]
   Hint Resolve cons_Cmp : core.
 
   Lemma compare_aux_Cmp : forall e,
diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v
index ab87ba9722..77ce76721e 100644
--- a/theories/FSets/FMapInterface.v
+++ b/theories/FSets/FMapInterface.v
@@ -58,6 +58,7 @@ Definition Cmp (elt:Type)(cmp:elt->elt->bool) e1 e2 := cmp e1 e2 = true.
 Module Type WSfun (E : DecidableType).
 
   Definition key := E.t.
+  #[global]
   Hint Transparent key : core.
 
   Parameter t : Type -> Type.
@@ -243,9 +244,11 @@ Module Type WSfun (E : DecidableType).
 	(x:key)(f:option elt->option elt'->option elt''),
         In x (map2 f m m') -> In x m \/ In x m'.
 
+  #[global]
   Hint Immediate MapsTo_1 mem_2 is_empty_2
     map_2 mapi_2 add_3 remove_3 find_2
     : map.
+  #[global]
   Hint Resolve mem_1 is_empty_1 is_empty_2 add_1 add_2 remove_1
     remove_2 find_1 fold_1 map_1 mapi_1 mapi_2
     : map.
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index a5c00189c4..204e8d0199 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -51,6 +51,7 @@ Proof.
  intro abs.
  inversion abs.
 Qed.
+#[local]
 Hint Resolve empty_1 : core.
 
 Lemma empty_sorted : Sort empty.
@@ -216,6 +217,7 @@ Proof.
  compute in H0,H1.
  simpl; case (X.compare x x''); intuition.
 Qed.
+#[local]
 Hint Resolve add_Inf : core.
 
 Lemma add_sorted : forall m (Hm:Sort m) x e, Sort (add x e m).
@@ -302,6 +304,7 @@ Proof.
  inversion_clear Hm.
  apply Inf_lt with (x'',e''); auto.
 Qed.
+#[local]
 Hint Resolve remove_Inf : core.
 
 Lemma remove_sorted : forall m (Hm:Sort m) x, Sort (remove x m).
@@ -586,6 +589,7 @@ Proof.
  inversion_clear H; auto.
 Qed.
 
+#[local]
 Hint Resolve map_lelistA : core.
 
 Lemma map_sorted : forall (m: t elt)(Hm : sort (@ltk elt) m)(f:elt -> elt'),
@@ -655,6 +659,7 @@ Proof.
  inversion_clear H; auto.
 Qed.
 
+#[local]
 Hint Resolve mapi_lelistA : core.
 
 Lemma mapi_sorted : forall m (Hm : sort (@ltk elt) m)(f: key ->elt -> elt'),
@@ -782,6 +787,7 @@ Proof.
  inversion_clear H; auto.
  inversion_clear H0; auto.
 Qed.
+#[local]
 Hint Resolve combine_lelistA : core.
 
 Lemma combine_sorted :
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index c4bb67a52c..78e7ab69d8 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -49,6 +49,7 @@ Proof.
  inversion abs.
 Qed.
 
+#[local]
 Hint Resolve empty_1 : core.
 
 Lemma empty_NoDup : NoDupA empty.
@@ -621,6 +622,7 @@ Proof.
  inversion_clear 1.
  intros; apply add_NoDup; auto.
 Qed.
+#[local]
 Hint Resolve fold_right_pair_NoDup : core.
 
 Lemma combine_NoDup :
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index 73021a84a3..4917fcb5fd 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -137,6 +137,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
     generalize (E.eq_sym H0); case (Pdec x); case (Pdec y); firstorder.
   Qed.
 
+  #[global]
   Hint Resolve compat_P_aux : core.
 
   Definition filter :
@@ -467,6 +468,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
   Proof.
     intros; unfold elements; case (M.elements s); firstorder.
   Qed.
+  #[global]
   Hint Resolve elements_3 : core.
 
   Lemma elements_3w : forall s : t, NoDupA E.eq (elements s).
@@ -666,6 +668,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
       rewrite <- H1; firstorder.
   Qed.
 
+  #[global]
   Hint Resolve compat_P_aux : core.
 
   Definition filter (f : elt -> bool) (s : t) : t :=
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index 8a217a752a..d597c0404a 100644
--- a/theories/FSets/FSetDecide.v
+++ b/theories/FSets/FSetDecide.v
@@ -466,6 +466,7 @@ the above form:
     (** Here is the tactic that will throw away hypotheses that
         are not useful (for the intended scope of the [fsetdec]
         tactic). *)
+    #[global]
     Hint Constructors FSet_elt_Prop FSet_Prop : FSet_Prop.
     Ltac discard_nonFSet :=
       repeat (
@@ -518,6 +519,7 @@ the above form:
 
     (** The hint database [FSet_decidability] will be given to
         the [push_neg] tactic from the module [Negation]. *)
+    #[global]
     Hint Resolve dec_In dec_eq : FSet_decidability.
 
     (** ** Normalizing Propositions About Equality
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index ac08351ad9..7618880bd2 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -460,9 +460,11 @@ Qed.
 
 End BasicProperties.
 
+#[global]
 Hint Immediate empty_mem is_empty_equal_empty add_mem_1
    remove_mem_1 singleton_equal_add union_mem inter_mem
    diff_mem equal_sym add_remove remove_add : set.
+#[global]
 Hint Resolve equal_mem_1 subset_mem_1 choose_mem_1
    choose_mem_2 add_mem_2 remove_mem_2 equal_refl equal_equal
    subset_refl subset_equal subset_antisym
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index dfe22b7831..848c27cba1 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -253,13 +253,16 @@ Module Type WSfun (E : DecidableType).
 
   End Spec.
 
+  #[global]
   Hint Transparent elt : core.
+  #[global]
   Hint Resolve mem_1 equal_1 subset_1 empty_1
     is_empty_1 choose_1 choose_2 add_1 add_2 remove_1
     remove_2 singleton_2 union_1 union_2 union_3
     inter_3 diff_3 fold_1 filter_3 for_all_1 exists_1
     partition_1 partition_2 elements_1 elements_3w
     : set.
+  #[global]
   Hint Immediate In_1 mem_2 equal_2 subset_2 is_empty_2 add_3
     remove_3 singleton_1 inter_1 inter_2 diff_1 diff_2
     filter_1 filter_2 for_all_2 exists_2 elements_2
@@ -336,7 +339,9 @@ Module Type Sfun (E : OrderedType).
 
   End Spec.
 
+  #[global]
   Hint Resolve elements_3 : set.
+  #[global]
   Hint Immediate
     min_elt_1 min_elt_2 min_elt_3 max_elt_1 max_elt_2 max_elt_3 : set.
 
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 98b445580b..af034bbdd5 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -21,7 +21,9 @@ Require Import DecidableTypeEx FSetFacts FSetDecide.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+#[global]
 Hint Unfold transpose compat_op Proper respectful : fset.
+#[global]
 Hint Extern 1 (Equivalence _) => constructor; congruence : fset.
 
 (** First, a functor for Weak Sets in functorial version. *)
@@ -269,7 +271,9 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
 
   End BasicProperties.
 
+  #[global]
   Hint Immediate equal_sym add_remove remove_add union_sym inter_sym: set.
+  #[global]
   Hint Resolve equal_refl equal_trans subset_refl subset_equal subset_antisym
     subset_trans subset_empty subset_remove_3 subset_diff subset_add_3
     subset_add_2 in_subset empty_is_empty_1 empty_is_empty_2 add_equal
@@ -732,6 +736,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
   Proof.
   intros; rewrite cardinal_Empty; auto.
   Qed.
+  #[global]
   Hint Resolve cardinal_inv_1 : fset.
 
   Lemma cardinal_inv_2 :
@@ -769,6 +774,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
   exact Equal_cardinal.
   Qed.
 
+  #[global]
   Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal : fset.
 
   (** ** Cardinal and set operators *)
@@ -778,6 +784,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
   rewrite cardinal_fold; apply fold_1; auto with set fset.
   Qed.
 
+  #[global]
   Hint Immediate empty_cardinal cardinal_1 : set.
 
   Lemma singleton_cardinal : forall x, cardinal (singleton x) = 1.
@@ -788,6 +795,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
   apply cardinal_2 with x; auto with set.
   Qed.
 
+  #[global]
   Hint Resolve singleton_cardinal: set.
 
   Lemma diff_inter_cardinal :
@@ -887,6 +895,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
   auto with set fset.
   Qed.
 
+  #[global]
   Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2 : fset.
 
 End WProperties_fun.
@@ -952,6 +961,7 @@ Module OrdProperties (M:S).
    red; intros x a b H; unfold leb.
    f_equal; apply gtb_compat; auto.
   Qed.
+  #[global]
   Hint Resolve gtb_compat leb_compat : fset.
 
   Lemma elements_split : forall x s,
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 9984bff0c2..f013c857ea 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -83,6 +83,7 @@ Lemma andb_prop (a b:bool) : andb a b = true -> a = true /\ b = true.
 Proof.
   destruct a, b; repeat split; assumption.
 Qed.
+#[global]
 Hint Resolve andb_prop: bool.
 
 Register andb_prop as core.bool.andb_prop.
@@ -92,6 +93,7 @@ Lemma andb_true_intro (b1 b2:bool) :
 Proof.
   destruct b1; destruct b2; simpl; intros [? ?]; assumption.
 Qed.
+#[global]
 Hint Resolve andb_true_intro: bool.
 
 Register andb_true_intro as core.bool.andb_true_intro.
@@ -100,6 +102,7 @@ Register andb_true_intro as core.bool.andb_true_intro.
 
 Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.
 
+#[global]
 Hint Constructors eq_true : eq_true.
 
 Register eq_true as core.eq_true.type.
@@ -142,6 +145,7 @@ Defined.
 Inductive BoolSpec (P Q : Prop) : bool -> Prop :=
   | BoolSpecT : P -> BoolSpec P Q true
   | BoolSpecF : Q -> BoolSpec P Q false.
+#[global]
 Hint Constructors BoolSpec : core.
 
 Register BoolSpec as core.BoolSpec.type.
@@ -243,6 +247,7 @@ Section projections.
 
 End projections.
 
+#[global]
 Hint Resolve pair inl inr: core.
 
 Lemma surjective_pairing (A B:Type) (p:A * B) : p = (fst p, snd p).
@@ -380,6 +385,7 @@ Inductive CompareSpec (Peq Plt Pgt : Prop) : comparison -> Prop :=
  | CompEq : Peq -> CompareSpec Peq Plt Pgt Eq
  | CompLt : Plt -> CompareSpec Peq Plt Pgt Lt
  | CompGt : Pgt -> CompareSpec Peq Plt Pgt Gt.
+#[global]
 Hint Constructors CompareSpec : core.
 
 Register CompareSpec as core.CompareSpec.type.
@@ -395,6 +401,7 @@ Inductive CompareSpecT (Peq Plt Pgt : Prop) : comparison -> Type :=
  | CompEqT : Peq -> CompareSpecT Peq Plt Pgt Eq
  | CompLtT : Plt -> CompareSpecT Peq Plt Pgt Lt
  | CompGtT : Pgt -> CompareSpecT Peq Plt Pgt Gt.
+#[global]
 Hint Constructors CompareSpecT : core.
 
 Register CompareSpecT as core.CompareSpecT.type.
@@ -417,6 +424,7 @@ Definition CompSpec {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Prop :=
 
 Definition CompSpecT {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Type :=
  CompareSpecT (eq x y) (lt x y) (lt y x).
+#[global]
 Hint Unfold CompSpec CompSpecT : core.
 
 Lemma CompSpec2Type : forall A (eq lt:A->A->Prop) x y c,
@@ -435,6 +443,7 @@ Proof. intros. apply CompareSpec2Type; assumption. Defined.
 
 Inductive identity (A:Type) (a:A) : A -> Type :=
   identity_refl : identity a a.
+#[global]
 Hint Resolve identity_refl: core.
 
 Arguments identity_ind [A] a P f y i.
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 8012235143..023705e169 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -41,9 +41,12 @@ Register not as core.not.type.
   variables and constants explicitly. *)
 
 Create HintDb core.
+#[global]
 Hint Variables Opaque : core.
+#[global]
 Hint Constants Opaque : core.
 
+#[global]
 Hint Unfold not: core.
 
   (** [and A B], written [A /\ B], is the conjunction of [A] and [B]
@@ -119,6 +122,7 @@ Theorem iff_sym : forall A B:Prop, (A <-> B) -> (B <-> A).
 
 End Equivalence.
 
+#[global]
 Hint Unfold iff: extcore.
 
 (** Backward direction of the equivalences above does not need assumptions *)
@@ -364,8 +368,11 @@ Notation "x = y" := (eq x y) : type_scope.
 Notation "x <> y  :> T" := (~ x = y :>T) : type_scope.
 Notation "x <> y" := (~ (x = y)) : type_scope.
 
+#[global]
 Hint Resolve I conj or_introl or_intror : core.
+#[global]
 Hint Resolve eq_refl: core.
+#[global]
 Hint Resolve ex_intro ex_intro2: core.
 
 Register eq as core.eq.type.
@@ -733,6 +740,7 @@ Notation sym_equal := eq_sym (only parsing).
 Notation trans_equal := eq_trans (only parsing).
 Notation sym_not_equal := not_eq_sym (only parsing).
 
+#[global]
 Hint Immediate eq_sym not_eq_sym: core.
 
 (** Basic definitions about relations and properties *)
@@ -801,6 +809,7 @@ Qed.
 
 Inductive inhabited (A:Type) : Prop := inhabits : A -> inhabited A.
 
+#[global]
 Hint Resolve inhabits: core.
 
 Lemma exists_inhabited : forall (A:Type) (P:A->Prop),
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index 3d9937ae89..f8869615cd 100644
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -72,6 +72,7 @@ Definition identity_rect_r :
  intros A x P H y H0; case identity_sym with (1 := H0); trivial.
 Defined.
 
+#[global]
 Hint Immediate identity_sym not_identity_sym: core.
 
 Notation refl_id := identity_refl (only parsing).
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 98fd52f351..fb2a7a57fe 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -37,6 +37,7 @@ Local Notation "0" := O.
 Definition eq_S := f_equal S.
 Definition f_equal_nat := f_equal (A:=nat).
 
+#[global]
 Hint Resolve f_equal_nat: core.
 
 (** The predecessor function *)
@@ -53,12 +54,14 @@ Qed.
 (** Injectivity of successor *)
 
 Definition eq_add_S n m (H: S n = S m): n = m := f_equal pred H.
+#[global]
 Hint Immediate eq_add_S: core.
 
 Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m.
 Proof.
   red; auto.
 Qed.
+#[global]
 Hint Resolve not_eq_S: core.
 
 Definition IsSucc (n:nat) : Prop :=
@@ -73,12 +76,14 @@ Theorem O_S : forall n:nat, 0 <> S n.
 Proof.
   discriminate.
 Qed.
+#[global]
 Hint Resolve O_S: core.
 
 Theorem n_Sn : forall n:nat, n <> S n.
 Proof.
   intro n; induction n; auto.
 Qed.
+#[global]
 Hint Resolve n_Sn: core.
 
 (** Addition *)
@@ -88,6 +93,7 @@ Infix "+" := Nat.add : nat_scope.
 
 Definition f_equal2_plus := f_equal2 plus.
 Definition f_equal2_nat := f_equal2 (A1:=nat) (A2:=nat). 
+#[global]
 Hint Resolve f_equal2_nat: core.
 
 Lemma plus_n_O : forall n:nat, n = n + 0.
@@ -95,7 +101,9 @@ Proof.
   intro n; induction n; simpl; auto.
 Qed.
 
+#[global]
 Remove Hints eq_refl : core.
+#[global]
 Hint Resolve plus_n_O eq_refl: core.  (* We want eq_refl to have higher priority than plus_n_O *)
 
 Lemma plus_O_n : forall n:nat, 0 + n = n.
@@ -107,6 +115,7 @@ Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m.
 Proof.
   intros n m; induction n; simpl; auto.
 Qed.
+#[global]
 Hint Resolve plus_n_Sm: core.
 
 Lemma plus_Sn_m : forall n m:nat, S n + m = S (n + m).
@@ -125,12 +134,14 @@ Notation mult := Nat.mul (only parsing).
 Infix "*" := Nat.mul : nat_scope.
 
 Definition f_equal2_mult := f_equal2 mult.
+#[global]
 Hint Resolve f_equal2_mult: core.
 
 Lemma mult_n_O : forall n:nat, 0 = n * 0.
 Proof.
   intro n; induction n; simpl; auto.
 Qed.
+#[global]
 Hint Resolve mult_n_O: core.
 
 Lemma mult_n_Sm : forall n m:nat, n * m + n = n * S m.
@@ -139,6 +150,7 @@ Proof.
   destruct H; rewrite <- plus_n_Sm; apply eq_S.
   pattern m at 1 3; elim m; simpl; auto.
 Qed.
+#[global]
 Hint Resolve mult_n_Sm: core.
 
 (** Standard associated names *)
@@ -162,20 +174,24 @@ where "n <= m" := (le n m) : nat_scope.
 
 Register le_n as num.nat.le_n.
 
+#[global]
 Hint Constructors le: core.
 (*i equivalent to : "Hints Resolve le_n le_S : core." i*)
 
 Definition lt (n m:nat) := S n <= m.
+#[global]
 Hint Unfold lt: core.
 
 Infix "<" := lt : nat_scope.
 
 Definition ge (n m:nat) := m <= n.
+#[global]
 Hint Unfold ge: core.
 
 Infix ">=" := ge : nat_scope.
 
 Definition gt (n m:nat) := m < n.
+#[global]
 Hint Unfold gt: core.
 
 Infix ">" := gt : nat_scope.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 1fb6dabe6f..5d759f3234 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -797,5 +797,7 @@ Proof.
   apply (h2 h1).
 Defined.
 
+#[global]
 Hint Resolve left right inleft inright: core.
+#[global]
 Hint Resolve exist exist2 existT existT2: core.
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 35bab1021e..8721b7c797 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -339,5 +339,6 @@ Tactic Notation "assert_fails" tactic3(tac) :=
   assert_fails tac.
 
 Create HintDb rewrite discriminated.
+#[global]
 Hint Variables Opaque : rewrite.
 Create HintDb typeclass_instances discriminated.
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 4cc3597029..115c7cb365 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -163,6 +163,7 @@ Section Facts.
   Proof.
      auto using app_assoc.
   Qed.
+  #[local]
   Hint Resolve app_assoc_reverse : core.
   (* end hide *)
 
@@ -385,10 +386,15 @@ Section Facts.
 
 End Facts.
 
+#[global]
 Hint Resolve app_assoc app_assoc_reverse: datatypes.
+#[global]
 Hint Resolve app_comm_cons app_cons_not_nil: datatypes.
+#[global]
 Hint Immediate app_eq_nil: datatypes.
+#[global]
 Hint Resolve app_eq_unit app_inj_tail: datatypes.
+#[global]
 Hint Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app: datatypes.
 
 
@@ -1928,6 +1934,7 @@ Section length_order.
   Qed.
 End length_order.
 
+#[global]
 Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons:
   datatypes.
 
@@ -1941,6 +1948,7 @@ Section SetIncl.
   Variable A : Type.
 
   Definition incl (l m:list A) := forall a:A, In a l -> In a m.
+  #[local]
   Hint Unfold incl : core.
 
   Lemma incl_nil_l : forall l, incl nil l.
@@ -1959,12 +1967,14 @@ Section SetIncl.
   Proof.
     auto.
   Qed.
+  #[local]
   Hint Resolve incl_refl : core.
 
   Lemma incl_tl : forall (a:A) (l m:list A), incl l m -> incl l (a :: m).
   Proof.
     auto with datatypes.
   Qed.
+  #[local]
   Hint Immediate incl_tl : core.
 
   Lemma incl_tran : forall l m n:list A, incl l m -> incl m n -> incl l n.
@@ -1976,12 +1986,14 @@ Section SetIncl.
   Proof.
     auto with datatypes.
   Qed.
+  #[local]
   Hint Immediate incl_appl : core.
 
   Lemma incl_appr : forall l m n:list A, incl l n -> incl l (m ++ n).
   Proof.
     auto with datatypes.
   Qed.
+  #[local]
   Hint Immediate incl_appr : core.
 
   Lemma incl_cons :
@@ -1997,6 +2009,7 @@ Section SetIncl.
     now_show (In a0 l -> In a0 m).
     auto.
   Qed.
+  #[local]
   Hint Resolve incl_cons : core.
 
   Lemma incl_cons_inv : forall (a:A) (l m:list A),
@@ -2012,6 +2025,7 @@ Section SetIncl.
     now_show (In a n).
     elim (in_app_or _ _ _ H1); auto.
   Qed.
+  #[local]
   Hint Resolve incl_app : core.
 
   Lemma incl_app_app : forall l1 l2 m1 m2:list A,
@@ -2054,6 +2068,7 @@ Proof.
   apply in_map; intuition.
 Qed.
 
+#[global]
 Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons
   incl_app incl_map: datatypes.
 
@@ -2738,6 +2753,7 @@ Section Exists_Forall.
       | Exists_cons_hd : forall x l, P x -> Exists (x::l)
       | Exists_cons_tl : forall x l, Exists l -> Exists (x::l).
 
+    #[local]
     Hint Constructors Exists : core.
 
     Lemma Exists_exists (l:list A) :
@@ -2815,6 +2831,7 @@ Section Exists_Forall.
       | Forall_nil : Forall nil
       | Forall_cons : forall x l, P x -> Forall l -> Forall (x::l).
 
+    #[local]
     Hint Constructors Forall : core.
 
     Lemma Forall_forall (l:list A):
@@ -2999,7 +3016,9 @@ Section Exists_Forall.
 
 End Exists_Forall.
 
+#[global]
 Hint Constructors Exists : core.
+#[global]
 Hint Constructors Forall : core.
 
 Lemma exists_Forall A B : forall (P : A -> B -> Prop) l,
@@ -3064,6 +3083,7 @@ Section Forall2.
     | Forall2_cons : forall x y l l',
       R x y -> Forall2 l l' -> Forall2 (x::l) (y::l').
 
+  #[local]
   Hint Constructors Forall2 : core.
 
   Theorem Forall2_refl : Forall2 [] [].
@@ -3098,6 +3118,7 @@ Section Forall2.
   Qed.
 End Forall2.
 
+#[global]
 Hint Constructors Forall2 : core.
 
 Section ForallPairs.
@@ -3119,6 +3140,7 @@ Section ForallPairs.
     | FOP_cons : forall a l,
       Forall (R a) l -> ForallOrdPairs l -> ForallOrdPairs (a::l).
 
+  #[local]
   Hint Constructors ForallOrdPairs : core.
 
   Lemma ForallOrdPairs_In : forall l,
@@ -3344,6 +3366,7 @@ Notation rev_acc := rev_append (only parsing).
 Notation rev_acc_rev := rev_append_rev (only parsing).
 Notation AllS := Forall (only parsing). (* was formerly in TheoryList *)
 
+#[global]
 Hint Resolve app_nil_end : datatypes.
 (* end hide *)
 
diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index 7f5148d0dd..458d08ccb9 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -193,6 +193,7 @@ Section first_definitions.
      | auto with datatypes ].
   Qed.
 
+  #[local]
   Hint Resolve set_add_intro1 set_add_intro2 : core.
 
   Lemma set_add_intro :
@@ -224,6 +225,7 @@ Section first_definitions.
    case H1; trivial.
    Qed.
 
+  #[local]
   Hint Resolve set_add_intro set_add_elim set_add_elim2 : core.
 
   Lemma set_add_not_empty : forall (a:A) (x:set), set_add a x <> empty_set.
@@ -310,6 +312,7 @@ Section first_definitions.
     intros; elim H0; auto with datatypes.
   Qed.
 
+  #[local]
   Hint Resolve set_union_intro2 set_union_intro1 : core.
 
   Lemma set_union_intro :
@@ -393,6 +396,7 @@ Section first_definitions.
     eauto with datatypes.
   Qed.
 
+  #[local]
   Hint Resolve set_inter_elim1 set_inter_elim2 : core.
 
   Lemma set_inter_elim :
@@ -471,6 +475,7 @@ Section first_definitions.
   apply (set_diff_elim1 _ _ _ H).
   Qed.
 
+#[local]
 Hint Resolve set_diff_intro set_diff_trivial : core.
 
 
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index 48e9f992fd..826815410a 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -30,6 +30,7 @@ Inductive InA (x : A) : list A -> Prop :=
   | InA_cons_hd : forall y l, eqA x y -> InA x (y :: l)
   | InA_cons_tl : forall y l, InA x l -> InA x (y :: l).
 
+#[local]
 Hint Constructors InA : core.
 
 (** TODO: it would be nice to have a generic definition instead
@@ -62,6 +63,7 @@ Inductive NoDupA : list A -> Prop :=
   | NoDupA_nil : NoDupA nil
   | NoDupA_cons : forall x l, ~ InA x l -> NoDupA l -> NoDupA (x::l).
 
+#[local]
 Hint Constructors NoDupA : core.
 
 (** An alternative definition of [NoDupA] based on [ForallOrdPairs] *)
@@ -84,6 +86,7 @@ Definition equivlistA l l' := forall x, InA x l <-> InA x l'.
 
 Lemma incl_nil l : inclA nil l.
 Proof. intro. intros. inversion H. Qed.
+#[local]
 Hint Resolve incl_nil : list.
 
 (** lists with same elements modulo [eqA] at the same place *)
@@ -93,6 +96,7 @@ Inductive eqlistA : list A -> list A -> Prop :=
   | eqlistA_cons : forall x x' l l',
       eqA x x' -> eqlistA l l' -> eqlistA (x::l) (x'::l').
 
+#[local]
 Hint Constructors eqlistA : core.
 
 (** We could also have written [eqlistA = Forall2 eqA]. *)
@@ -107,7 +111,9 @@ Definition eqarefl := (@Equivalence_Reflexive _ _ eqA_equiv).
 Definition eqatrans := (@Equivalence_Transitive _ _ eqA_equiv).
 Definition eqasym := (@Equivalence_Symmetric _ _ eqA_equiv).
  
+#[local]
 Hint Resolve eqarefl eqatrans : core.
+#[local]
 Hint Immediate eqasym : core.
 
 Ltac inv := invlist InA; invlist sort; invlist lelistA; invlist NoDupA.
@@ -154,6 +160,7 @@ Lemma InA_eqA : forall l x y, eqA x y -> InA x l -> InA y l.
 Proof.
  intros l x y H H'. rewrite <- H. auto.
 Qed.
+#[local]
 Hint Immediate InA_eqA : core.
 
 Lemma In_InA : forall l x, In x l -> InA x l.
@@ -161,6 +168,7 @@ Proof.
  simple induction l; simpl; intuition.
  subst; auto.
 Qed.
+#[local]
 Hint Resolve In_InA : core.
 
 Lemma InA_split : forall l x, InA x l ->
@@ -786,11 +794,13 @@ Hypothesis ltA_compat : Proper (eqA==>eqA==>iff) ltA.
 
 Let sotrans := (@StrictOrder_Transitive _ _ ltA_strorder).
 
+#[local]
 Hint Resolve sotrans : core.
 
 Notation InfA:=(lelistA ltA).
 Notation SortA:=(sort ltA).
 
+#[local]
 Hint Constructors lelistA sort : core.
 
 Lemma InfA_ltA :
@@ -814,6 +824,7 @@ Lemma InfA_eqA l x y : eqA x y -> InfA y l -> InfA x l.
 Proof using eqA_equiv ltA_compat.
  intros H; now rewrite H.
 Qed.
+#[local]
 Hint Immediate InfA_ltA InfA_eqA : core.
 
 Lemma SortA_InfA_InA :
@@ -1005,6 +1016,7 @@ Qed.
 End Filter.
 End Type_with_equality.
 
+#[global]
 Hint Constructors InA eqlistA NoDupA sort lelistA : core.
 
 Arguments equivlistA_cons_nil {A} eqA {eqA_equiv} x l _.
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index 7a275a8231..f16d70a4c2 100644
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -54,6 +54,7 @@ Lemma tl_nth_tl :
 Proof.
   simple induction n; simpl; auto.
 Qed.
+#[local]
 Hint Resolve tl_nth_tl: datatypes.
 
 Lemma Str_nth_tl_plus :
diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v
index e5d364297d..b2b5985ff1 100644
--- a/theories/Logic/Classical_Prop.v
+++ b/theories/Logic/Classical_Prop.v
@@ -16,6 +16,7 @@
 
 Require Import ClassicalFacts.
 
+#[global]
 Hint Unfold not: core.
 
 Axiom classic : forall P:Prop, P \/ ~ P.
diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v
index 998497f13e..5fb6bb3907 100644
--- a/theories/Logic/Decidable.v
+++ b/theories/Logic/Decidable.v
@@ -206,6 +206,7 @@ Qed.
 (** With the following hint database, we can leverage [auto] to check
     decidability of propositions. *)
 
+#[global]
 Hint Resolve dec_True dec_False dec_or dec_and dec_imp dec_not dec_iff
  : decidable_prop.
 
diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v
index f2e15c9abb..934806de93 100644
--- a/theories/Logic/Eqdep.v
+++ b/theories/Logic/Eqdep.v
@@ -35,5 +35,7 @@ Export EqdepTheory.
 
 (** Exported hints *)
 
+#[global]
 Hint Resolve eq_dep_eq: eqdep.
+#[global]
 Hint Resolve inj_pair2 inj_pairT2: eqdep.
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index a918d1ecd7..6589e75289 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -65,6 +65,7 @@ Section Dependent_Equality.
 
   Inductive eq_dep (p:U) (x:P p) : forall q:U, P q -> Prop :=
     eq_dep_intro : eq_dep p x p x.
+  #[local]
   Hint Constructors eq_dep: core.
 
   Lemma eq_dep_refl : forall (p:U) (x:P p), eq_dep p x p x.
@@ -75,6 +76,7 @@ Section Dependent_Equality.
   Proof.
     destruct 1; auto.
   Qed.
+  #[local]
   Hint Immediate eq_dep_sym: core.
 
   Lemma eq_dep_trans :
@@ -221,7 +223,9 @@ Unset Implicit Arguments.
 
 (** Exported hints *)
 
+#[global]
 Hint Resolve eq_dep_intro: core.
+#[global]
 Hint Immediate eq_dep_sym: core.
 
 (************************************************************************)
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index ccd7db177c..7ee3a99d60 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -31,6 +31,7 @@ Arguments JMeq_refl {A x} , [A] x.
 Register JMeq as core.JMeq.type.
 Register JMeq_refl as core.JMeq.refl.
 
+#[global]
 Hint Resolve JMeq_refl : core.
 
 Definition JMeq_hom {A : Type} (x y : A) := JMeq x y.
@@ -42,6 +43,7 @@ Proof.
 intros; destruct H; trivial.
 Qed.
 
+#[global]
 Hint Immediate JMeq_sym : core.
 
 Register JMeq_sym as core.JMeq.sym.
diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v
index 0f62a9419b..aa0c419f0e 100644
--- a/theories/MSets/MSetDecide.v
+++ b/theories/MSets/MSetDecide.v
@@ -466,6 +466,7 @@ the above form:
     (** Here is the tactic that will throw away hypotheses that
         are not useful (for the intended scope of the [fsetdec]
         tactic). *)
+    #[global]
     Hint Constructors MSet_elt_Prop MSet_Prop : MSet_Prop.
     Ltac discard_nonMSet :=
       repeat (
@@ -518,6 +519,7 @@ the above form:
 
     (** The hint database [MSet_decidability] will be given to
         the [push_neg] tactic from the module [Negation]. *)
+    #[global]
     Hint Resolve dec_In dec_eq : MSet_decidability.
 
     (** ** Normalizing Propositions About Equality
diff --git a/theories/MSets/MSetEqProperties.v b/theories/MSets/MSetEqProperties.v
index dc22af4948..b439be9b3f 100644
--- a/theories/MSets/MSetEqProperties.v
+++ b/theories/MSets/MSetEqProperties.v
@@ -462,9 +462,11 @@ Qed.
 
 End BasicProperties.
 
+#[global]
 Hint Immediate empty_mem is_empty_equal_empty add_mem_1
    remove_mem_1 singleton_equal_add union_mem inter_mem
    diff_mem equal_sym add_remove remove_add : set.
+#[global]
 Hint Resolve equal_mem_1 subset_mem_1 choose_mem_1
    choose_mem_2 add_mem_2 remove_mem_2 equal_refl equal_equal
    subset_refl subset_equal subset_antisym
diff --git a/theories/MSets/MSetFacts.v b/theories/MSets/MSetFacts.v
index 7dbb658e46..ea86c7a4d7 100644
--- a/theories/MSets/MSetFacts.v
+++ b/theories/MSets/MSetFacts.v
@@ -139,12 +139,14 @@ Notation choose_1 := choose_spec1 (only parsing).
 Notation choose_2 := choose_spec2 (only parsing).
 Notation elements_3w := elements_spec2w (only parsing).
 
+#[global]
 Hint Resolve mem_1 equal_1 subset_1 empty_1
     is_empty_1 choose_1 choose_2 add_1 add_2 remove_1
     remove_2 singleton_2 union_1 union_2 union_3
     inter_3 diff_3 fold_1 filter_3 for_all_1 exists_1
     partition_1 partition_2 elements_1 elements_3w
     : set.
+#[global]
 Hint Immediate In_1 mem_2 equal_2 subset_2 is_empty_2 add_3
     remove_3 singleton_1 inter_1 inter_2 diff_1 diff_2
     filter_1 filter_2 for_all_2 exists_2 elements_2
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v
index 58656b666e..37d20bffad 100644
--- a/theories/MSets/MSetGenTree.v
+++ b/theories/MSets/MSetGenTree.v
@@ -46,6 +46,7 @@ End InfoTyp.
 Module Type Ops (X:OrderedType)(Info:InfoTyp).
 
 Definition elt := X.t.
+#[global]
 Hint Transparent elt : core.
 
 Inductive tree  : Type :=
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index fe5d721ffa..c0567f9ef1 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -442,6 +442,7 @@ Module WRaw2SetsOn (E:DecidableType)(M:WRawSets E) <: WSetsOn E.
  Record t_ := Mkt {this :> M.t; is_ok : M.Ok this}.
  Definition t := t_.
  Arguments Mkt this {is_ok}.
+ #[global]
  Hint Resolve is_ok : typeclass_instances.
 
  Definition In (x : elt)(s : t) := M.In x (this s).
@@ -884,9 +885,11 @@ Module MakeListOrdering (O:OrderedType).
         O.lt x y -> lt_list (x :: s) (y :: s')
     | lt_cons_eq : forall x y s s',
         O.eq x y -> lt_list s s' -> lt_list (x :: s) (y :: s').
+ #[global]
  Hint Constructors lt_list : core.
 
  Definition lt := lt_list.
+ #[global]
  Hint Unfold lt : core.
 
  Instance lt_strorder : StrictOrder lt.
@@ -933,6 +936,7 @@ Module MakeListOrdering (O:OrderedType).
   left; MO.order. right; rewrite <- E12; auto.
   left; MO.order. right; rewrite E12; auto.
  Qed.
+ #[global]
  Hint Resolve eq_cons : core.
 
  Lemma cons_CompSpec : forall c x1 x2 l1 l2, O.eq x1 x2 ->
@@ -940,6 +944,7 @@ Module MakeListOrdering (O:OrderedType).
  Proof.
   destruct c; simpl; inversion_clear 2; auto with relations.
  Qed.
+ #[global]
  Hint Resolve cons_CompSpec : core.
 
 End MakeListOrdering.
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index d2878b4710..84cf620474 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -231,13 +231,16 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Notation In := (InA X.eq).
 
   Existing Instance X.eq_equiv.
+  #[local]
   Hint Extern 20 => solve [order] : core.
 
   Definition IsOk s := Sort s.
 
   Class Ok (s:t) : Prop := ok : Sort s.
 
+  #[local]
   Hint Resolve ok : core.
+  #[local]
   Hint Unfold Ok : core.
 
   Instance Sort_Ok s `(Hs : Sort s) : Ok s := { ok := Hs }.
@@ -276,6 +279,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
     destruct H; constructor; tauto.
   Qed.
 
+  #[local]
   Hint Extern 1 (Ok _) => rewrite <- isok_iff : core.
 
   Ltac inv_ok := match goal with
@@ -326,6 +330,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   intuition.
   intros; elim_compare x a; inv; intuition.
   Qed.
+  #[local]
   Hint Resolve add_inf : core.
 
   Global Instance add_ok s x : forall `(Ok s), Ok (add x s).
@@ -353,6 +358,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   intros; elim_compare x a; inv; auto.
   apply Inf_lt with a; auto.
   Qed.
+  #[local]
   Hint Resolve remove_inf : core.
 
   Global Instance remove_ok s x : forall `(Ok s), Ok (remove x s).
@@ -396,6 +402,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Proof.
   induction2.
   Qed.
+  #[local]
   Hint Resolve union_inf : core.
 
   Global Instance union_ok s s' : forall `(Ok s, Ok s'), Ok (union s s').
@@ -422,6 +429,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   apply Hrec'; auto.
   apply Inf_lt with x'; auto.
   Qed.
+  #[local]
   Hint Resolve inter_inf : core.
 
   Global Instance inter_ok s s' : forall `(Ok s, Ok s'), Ok (inter s s').
@@ -452,6 +460,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   apply Hrec'; auto.
   apply Inf_lt with x'; auto.
   Qed.
+  #[local]
   Hint Resolve diff_inf : core.
 
   Global Instance diff_ok s s' : forall `(Ok s, Ok s'), Ok (diff s s').
diff --git a/theories/MSets/MSetProperties.v b/theories/MSets/MSetProperties.v
index 51807e5cda..b49a91ed14 100644
--- a/theories/MSets/MSetProperties.v
+++ b/theories/MSets/MSetProperties.v
@@ -21,6 +21,7 @@ Require Import DecidableTypeEx OrdersLists MSetFacts MSetDecide.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+#[global]
 Hint Unfold transpose : core.
 
 (** First, a functor for Weak Sets in functorial version. *)
@@ -268,7 +269,9 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
 
   End BasicProperties.
 
+  #[global]
   Hint Immediate equal_sym add_remove remove_add union_sym inter_sym: set.
+  #[global]
   Hint Resolve equal_refl equal_trans subset_refl subset_equal subset_antisym
     subset_trans subset_empty subset_remove_3 subset_diff subset_add_3
     subset_add_2 in_subset empty_is_empty_1 empty_is_empty_2 add_equal
@@ -735,6 +738,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
   Proof.
   intros; rewrite cardinal_Empty; auto.
   Qed.
+  #[global]
   Hint Resolve cardinal_inv_1 : core.
 
   Lemma cardinal_inv_2 :
@@ -774,6 +778,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
   exact Equal_cardinal.
   Qed.
 
+  #[global]
   Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal : core.
 
   (** ** Cardinal and set operators *)
@@ -783,6 +788,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
   rewrite cardinal_fold; apply fold_1; auto with *.
   Qed.
 
+  #[global]
   Hint Immediate empty_cardinal cardinal_1 : set.
 
   Lemma singleton_cardinal : forall x, cardinal (singleton x) = 1.
@@ -793,6 +799,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
   apply cardinal_2 with x; auto with set.
   Qed.
 
+  #[global]
   Hint Resolve singleton_cardinal: set.
 
   Lemma diff_inter_cardinal :
@@ -898,6 +905,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
   auto with set.
   Qed.
 
+  #[global]
   Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2 : core.
 
 End WPropertiesOn.
@@ -922,7 +930,9 @@ Module OrdProperties (M:Sets).
   Import M.E.
   Import M.
 
+  #[global]
   Hint Resolve elements_spec2 : core.
+  #[global]
   Hint Immediate
     min_elt_spec1 min_elt_spec2 min_elt_spec3
     max_elt_spec1 max_elt_spec2 max_elt_spec3 : set.
@@ -961,6 +971,7 @@ Module OrdProperties (M:Sets).
   Proof.
    intros a b H; unfold leb. rewrite H; auto.
   Qed.
+  #[global]
   Hint Resolve gtb_compat leb_compat : core.
 
   Lemma elements_split : forall x s,
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v
index 2498d82889..8a5ba2d80f 100644
--- a/theories/MSets/MSetWeakList.v
+++ b/theories/MSets/MSetWeakList.v
@@ -123,14 +123,18 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
   Let eqr:= (@Equivalence_Reflexive _ _ X.eq_equiv).
   Let eqsym:= (@Equivalence_Symmetric _ _ X.eq_equiv).
   Let eqtrans:= (@Equivalence_Transitive _ _ X.eq_equiv).
+  #[local]
   Hint Resolve eqr eqtrans : core.
+  #[local]
   Hint Immediate eqsym : core.
 
   Definition IsOk := NoDup.
 
   Class Ok (s:t) : Prop := ok : NoDup s.
 
+  #[local]
   Hint Unfold Ok : core.
+  #[local]
   Hint Resolve ok : core.
 
   Instance NoDup_Ok s (nd : NoDup s) : Ok s := { ok := nd }.
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index f6b2544b6e..c5c75fc17a 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -467,6 +467,7 @@ Section Basics.
  apply phibis_aux_pos.
  Qed.
 
+ #[local]
  Hint Resolve phi_nonneg : zarith.
 
  Lemma phi_bounded  : forall x, (0 <= phi x < 2 ^ (Z.of_nat size))%Z.
diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v
index 383c0aff3a..dbca2f0947 100644
--- a/theories/Numbers/Cyclic/Int63/Int63.v
+++ b/theories/Numbers/Cyclic/Int63/Int63.v
@@ -290,6 +290,7 @@ Proof. intros h; apply Z.lt_gt, Zpower_gt_0; lia. Qed.
 Lemma pow2_nz n : 0 <= n → 2 ^ n ≠ 0.
 Proof. intros h; generalize (pow2_pos _ h); lia. Qed.
 
+#[global]
 Hint Resolve pow2_pos pow2_nz : zarith.
 
 (* =================================================== *)
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
index 5e486333b2..6aad65899a 100644
--- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v
+++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
@@ -61,6 +61,7 @@ Section ZModulo.
   apply Z.lt_gt.
   unfold wB, base; auto with zarith.
  Qed.
+ #[local]
  Hint Resolve wB_pos : core.
 
  Lemma spec_to_Z_1 : forall x, 0 <= [|x|].
@@ -72,6 +73,7 @@ Section ZModulo.
  Proof.
   unfold to_Z; intros; destruct (Z_mod_lt x wB wB_pos); auto.
  Qed.
+ #[local]
  Hint Resolve spec_to_Z_1 spec_to_Z_2 : core.
 
  Lemma spec_to_Z : forall x, 0 <= [|x|] < wB.
@@ -706,6 +708,7 @@ Section ZModulo.
  Proof.
  induction p; simpl; auto with zarith.
  Qed.
+ #[local]
  Hint Resolve Ptail_pos : core.
 
  Lemma Ptail_bounded : forall p d, Zpos p < 2^(Zpos d) -> Ptail p < Zpos d.
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index 019b138b4d..2f8fcc7290 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -383,6 +383,7 @@ f_equiv. apply E, half_decrease.
 rewrite two_succ, <- not_true_iff_false, ltb_lt, nlt_ge, le_succ_l in H.
 order'.
 Qed.
+#[global]
 Hint Resolve log_good_step : core.
 
 Theorem log_init : forall n, n < 2 -> log n == 0.
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index 3e282f696a..3ecb5a5a61 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -26,6 +26,7 @@ Arguments id {A} x.
 Definition compose {A B C} (g : B -> C) (f : A -> B) :=
   fun x : A => g (f x).
 
+#[global]
 Hint Unfold compose : core.
 
 Declare Scope program_scope.
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 5862a08838..25af2d5ffb 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -21,6 +21,7 @@ Ltac is_ground_goal :=
 
 (** Try to find a contradiction. *)
 
+#[global]
 Hint Extern 10 => is_ground_goal ; progress exfalso : exfalso.
 
 (** We will use the [block] definition to separate the goal from the 
@@ -308,6 +309,7 @@ Proof. intros. rewrite (UIP_refl A). assumption. Defined.
 (** This hint database and the following tactic can be used with [autounfold] to 
    unfold everything to [eq_rect]s. *)
 
+#[global]
 Hint Unfold solution_left solution_right deletion simplification_heq
   simplification_existT1 simplification_existT2 simplification_K
   eq_rect_r eq_rec eq_ind : dep_elim.
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 688db8b812..d1be8812e9 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -108,6 +108,7 @@ Section Measure_well_founded.
 
 End Measure_well_founded.
 
+#[global]
 Hint Resolve measure_wf : core.
 
 Section Fix_rects.
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index fa4f9134cc..b008c6c2aa 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -95,7 +95,9 @@ Proof.
 symmetry. apply Z.ge_le_iff.
 Qed.
 
+#[global]
 Hint Unfold Qeq Qlt Qle : qarith.
+#[global]
 Hint Extern 5 (?X1 <> ?X2) => intro; discriminate: qarith.
 
 Lemma Qcompare_antisym x y : CompOpp (x ?= y) = (y ?= x).
@@ -127,7 +129,9 @@ apply Z.mul_reg_r with (QDen y); [auto with qarith|].
 now rewrite Z.mul_shuffle0, XY, Z.mul_shuffle0, YZ, Z.mul_shuffle0.
 Qed.
 
+#[global]
 Hint Immediate Qeq_sym : qarith.
+#[global]
 Hint Resolve Qeq_refl Qeq_trans : qarith.
 
 (** In a word, [Qeq] is a setoid equality. *)
@@ -203,6 +207,7 @@ Proof.
   rewrite !Qeq_bool_iff; apply Qeq_trans.
 Qed.
 
+#[global]
 Hint Resolve Qnot_eq_sym : qarith.
 
 (** * Addition, multiplication and opposite *)
@@ -783,6 +788,7 @@ Proof.
   Close Scope Z_scope.
 Qed.
 
+#[global]
 Hint Resolve Qle_trans : qarith.
 
 Lemma Qlt_irrefl x : ~x<x.
@@ -863,6 +869,7 @@ Proof.
   unfold Qle, Qlt, Qeq; intros; now apply Z.lt_eq_cases.
 Qed.
 
+#[global]
 Hint Resolve Qle_not_lt Qlt_not_le Qnot_le_lt Qnot_lt_le
  Qlt_le_weak Qlt_not_eq Qle_antisym Qle_refl: qarith.
 
@@ -904,6 +911,7 @@ Proof.
 Qed.
 
 
+#[global]
 Hint Resolve Qopp_le_compat : qarith.
 
 Lemma Qle_minus_iff : forall p q, p <= q <-> 0 <= q+-p.
diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v
index 13e88fc093..d1ff1fc794 100644
--- a/theories/QArith/Qabs.v
+++ b/theories/QArith/Qabs.v
@@ -11,6 +11,7 @@
 Require Export QArith.
 Require Export Qreduction.
 
+#[global]
 Hint Resolve Qlt_le_weak : qarith.
 
 Definition Qabs (x:Q) := let (n,d):=x in (Z.abs n#d).
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index 63b0a5afb7..bd43f901bb 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -66,6 +66,7 @@ Proof.
   rewrite hq, hq' in H'. subst q'. f_equal.
   apply eq_proofs_unicity. intros.  repeat decide equality.
 Qed.
+#[global]
 Hint Resolve Qc_is_canon : core.
 
 Theorem Qc_decomp: forall q q': Qc, (q:Q) = q' -> q = q'.
diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v
index 20b5cb236b..5a23a20811 100644
--- a/theories/QArith/Qreals.v
+++ b/theories/QArith/Qreals.v
@@ -19,6 +19,7 @@ intros.
 now apply not_O_IZR.
 Qed.
 
+#[global]
 Hint Resolve IZR_nz Rmult_integral_contrapositive : core.
 
 Lemma eqR_Qeq : forall x y : Q, Q2R x = Q2R y -> x==y.
diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v
index 8fd342ab15..06f4ca02d1 100644
--- a/theories/QArith/Qround.v
+++ b/theories/QArith/Qround.v
@@ -18,6 +18,7 @@ rewrite !Z.mul_opp_l.
 apply Z.opp_lt_mono.
 Qed.
 
+#[global]
 Hint Resolve Qopp_lt_compat : qarith.
 
 (************)
@@ -54,6 +55,7 @@ rewrite Z.mul_comm.
 now apply Z.mul_div_le.
 Qed.
 
+#[global]
 Hint Resolve Qfloor_le : qarith.
 
 Lemma Qle_ceiling : forall x, x <= Qceiling x.
@@ -66,6 +68,7 @@ change (Qceiling x:Q) with (-(Qfloor(-x))).
 auto with *.
 Qed.
 
+#[global]
 Hint Resolve Qle_ceiling : qarith.
 
 Lemma Qle_floor_ceiling : forall x, Qfloor x <= Qceiling x.
@@ -88,6 +91,7 @@ rewrite <- Z.lt_add_lt_sub_r.
 destruct (Z_mod_lt n (Zpos d)); auto with *.
 Qed.
 
+#[global]
 Hint Resolve Qlt_floor : qarith.
 
 Lemma Qceiling_lt : forall x, (Qceiling x-1)%Z < x.
@@ -101,6 +105,7 @@ rewrite Qopp_involutive.
 auto with *.
 Qed.
 
+#[global]
 Hint Resolve Qceiling_lt : qarith.
 
 Lemma Qfloor_resp_le : forall x y, x <= y -> (Qfloor x <= Qfloor y)%Z.
@@ -114,6 +119,7 @@ rewrite (Z.mul_comm (Zpos yd) (Zpos xd)).
 apply Z_div_le; auto with *.
 Qed.
 
+#[global]
 Hint Resolve Qfloor_resp_le : qarith.
 
 Lemma Qceiling_resp_le : forall x y, x <= y -> (Qceiling x <= Qceiling y)%Z.
@@ -123,6 +129,7 @@ unfold Qceiling.
 rewrite <- Z.opp_le_mono; auto with qarith.
 Qed.
 
+#[global]
 Hint Resolve Qceiling_resp_le : qarith.
 
 Add Morphism Qfloor with signature Qeq ==> eq as Qfloor_comp.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 993b7b3ec4..fd8acf481a 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -37,10 +37,12 @@ Lemma Rle_refl : forall r, r <= r.
 Proof.
   intro; right; reflexivity.
 Qed.
+#[global]
 Hint Immediate Rle_refl: rorders.
 
 Lemma Rge_refl : forall r, r <= r.
 Proof. exact Rle_refl. Qed.
+#[global]
 Hint Immediate Rge_refl: rorders.
 
 (** Irreflexivity of the strict order *)
@@ -49,6 +51,7 @@ Lemma Rlt_irrefl : forall r, ~ r < r.
 Proof.
   intros r H; eapply Rlt_asym; eauto.
 Qed.
+#[global]
 Hint Resolve Rlt_irrefl: real.
 
 Lemma Rgt_irrefl : forall r, ~ r > r.
@@ -72,6 +75,7 @@ Proof.
   - apply Rlt_not_eq in H1. eauto.
   - apply Rgt_not_eq in H1. eauto.
 Qed.
+#[global]
 Hint Resolve Rlt_dichotomy_converse: real.
 
 (** Reasoning by case on equality and order *)
@@ -82,6 +86,7 @@ Proof.
   intros; generalize (total_order_T r1 r2) Rlt_dichotomy_converse;
     unfold not; intuition eauto 3.
 Qed.
+#[global]
 Hint Resolve Req_dec: real.
 
 (**********)
@@ -110,6 +115,7 @@ Lemma Rlt_le : forall r1 r2, r1 < r2 -> r1 <= r2.
 Proof.
   intros; red; tauto.
 Qed.
+#[global]
 Hint Resolve Rlt_le: real.
 
 Lemma Rgt_ge : forall r1 r2, r1 > r2 -> r1 >= r2.
@@ -122,14 +128,18 @@ Lemma Rle_ge : forall r1 r2, r1 <= r2 -> r2 >= r1.
 Proof.
   destruct 1; red; auto with real.
 Qed.
+#[global]
 Hint Immediate Rle_ge: real.
+#[global]
 Hint Resolve Rle_ge: rorders.
 
 Lemma Rge_le : forall r1 r2, r1 >= r2 -> r2 <= r1.
 Proof.
   destruct 1; red; auto with real.
 Qed.
+#[global]
 Hint Resolve Rge_le: real.
+#[global]
 Hint Immediate Rge_le: rorders.
 
 (**********)
@@ -137,12 +147,14 @@ Lemma Rlt_gt : forall r1 r2, r1 < r2 -> r2 > r1.
 Proof.
   trivial.
 Qed.
+#[global]
 Hint Resolve Rlt_gt: rorders.
 
 Lemma Rgt_lt : forall r1 r2, r1 > r2 -> r2 < r1.
 Proof.
   trivial.
 Qed.
+#[global]
 Hint Immediate Rgt_lt: rorders.
 
 (**********)
@@ -151,6 +163,7 @@ Lemma Rnot_le_lt : forall r1 r2, ~ r1 <= r2 -> r2 < r1.
 Proof.
   intros r1 r2; generalize (Rtotal_order r1 r2); unfold Rle; tauto.
 Qed.
+#[global]
 Hint Immediate Rnot_le_lt: real.
 
 Lemma Rnot_ge_gt : forall r1 r2, ~ r1 >= r2 -> r2 > r1.
@@ -183,6 +196,7 @@ Proof.
   generalize Rlt_asym Rlt_dichotomy_converse; unfold Rle.
   unfold not; intuition eauto 3.
 Qed.
+#[global]
 Hint Immediate Rlt_not_le: real.
 
 Lemma Rgt_not_le : forall r1 r2, r1 > r2 -> ~ r1 <= r2.
@@ -190,6 +204,7 @@ Proof. exact Rlt_not_le. Qed.
 
 Lemma Rlt_not_ge : forall r1 r2, r1 < r2 -> ~ r1 >= r2.
 Proof. red; intros; eapply Rlt_not_le; eauto with real. Qed.
+#[global]
 Hint Immediate Rlt_not_ge: real.
 
 Lemma Rgt_not_ge : forall r1 r2, r2 > r1 -> ~ r1 >= r2.
@@ -215,24 +230,28 @@ Lemma Req_le : forall r1 r2, r1 = r2 -> r1 <= r2.
 Proof.
   unfold Rle; tauto.
 Qed.
+#[global]
 Hint Immediate Req_le: real.
 
 Lemma Req_ge : forall r1 r2, r1 = r2 -> r1 >= r2.
 Proof.
   unfold Rge; tauto.
 Qed.
+#[global]
 Hint Immediate Req_ge: real.
 
 Lemma Req_le_sym : forall r1 r2, r2 = r1 -> r1 <= r2.
 Proof.
   unfold Rle; auto.
 Qed.
+#[global]
 Hint Immediate Req_le_sym: real.
 
 Lemma Req_ge_sym : forall r1 r2, r2 = r1 -> r1 >= r2.
 Proof.
   unfold Rge; auto.
 Qed.
+#[global]
 Hint Immediate Req_ge_sym: real.
 
 (** *** Asymmetry *)
@@ -248,6 +267,7 @@ Lemma Rle_antisym : forall r1 r2, r1 <= r2 -> r2 <= r1 -> r1 = r2.
 Proof.
   intros r1 r2; generalize (Rlt_asym r1 r2); unfold Rle; intuition.
 Qed.
+#[global]
 Hint Resolve Rle_antisym: real.
 
 Lemma Rge_antisym : forall r1 r2, r1 >= r2 -> r2 >= r1 -> r1 = r2.
@@ -387,12 +407,14 @@ Lemma Rplus_0_r : forall r, r + 0 = r.
 Proof.
   intro; ring.
 Qed.
+#[global]
 Hint Resolve Rplus_0_r: real.
 
 Lemma Rplus_ne : forall r, r + 0 = r /\ 0 + r = r.
 Proof.
   split; ring.
 Qed.
+#[global]
 Hint Resolve Rplus_ne: real.
 
 (**********)
@@ -403,6 +425,7 @@ Lemma Rplus_opp_l : forall r, - r + r = 0.
 Proof.
   intro; ring.
 Qed.
+#[global]
 Hint Resolve Rplus_opp_l: real.
 
 (**********)
@@ -415,6 +438,7 @@ Qed.
 
 Definition f_equal_R := (f_equal (A:=R)).
 
+#[global]
 Hint Resolve f_equal_R : real.
 
 Lemma Rplus_eq_compat_l : forall r r1 r2, r1 = r2 -> r + r1 = r + r2.
@@ -439,6 +463,7 @@ Proof.
   repeat rewrite Rplus_assoc; rewrite <- H; reflexivity.
   ring.
 Qed.
+#[global]
 Hint Resolve Rplus_eq_reg_l: real.
 
 Lemma Rplus_eq_reg_r : forall r r1 r2, r1 + r = r2 + r -> r1 = r2.
@@ -485,18 +510,21 @@ Lemma Rinv_r : forall r, r <> 0 -> r * / r = 1.
 Proof.
   intros; field; trivial.
 Qed.
+#[global]
 Hint Resolve Rinv_r: real.
 
 Lemma Rinv_l_sym : forall r, r <> 0 -> 1 = / r * r.
 Proof.
   intros; field; trivial.
 Qed.
+#[global]
 Hint Resolve Rinv_l_sym: real.
 
 Lemma Rinv_r_sym : forall r, r <> 0 -> 1 = r * / r.
 Proof.
   intros; field; trivial.
 Qed.
+#[global]
 Hint Resolve Rinv_r_sym: real.
 
 (**********)
@@ -504,6 +532,7 @@ Lemma Rmult_0_r : forall r, r * 0 = 0.
 Proof.
   intro; ring.
 Qed.
+#[global]
 Hint Resolve Rmult_0_r: real.
 
 (**********)
@@ -511,6 +540,7 @@ Lemma Rmult_0_l : forall r, 0 * r = 0.
 Proof.
   intro; ring.
 Qed.
+#[global]
 Hint Resolve Rmult_0_l: real.
 
 (**********)
@@ -518,6 +548,7 @@ Lemma Rmult_ne : forall r, r * 1 = r /\ 1 * r = r.
 Proof.
   intro; split; ring.
 Qed.
+#[global]
 Hint Resolve Rmult_ne: real.
 
 (**********)
@@ -525,6 +556,7 @@ Lemma Rmult_1_r : forall r, r * 1 = r.
 Proof.
   intro; ring.
 Qed.
+#[global]
 Hint Resolve Rmult_1_r: real.
 
 (**********)
@@ -572,6 +604,7 @@ Proof.
   intros r1 r2 [H| H]; rewrite H; auto with real.
 Qed.
 
+#[global]
 Hint Resolve Rmult_eq_0_compat: real.
 
 (**********)
@@ -599,6 +632,7 @@ Proof.
   red; intros r1 r2 [H1 H2] H.
   case (Rmult_integral r1 r2); auto with real.
 Qed.
+#[global]
 Hint Resolve Rmult_integral_contrapositive: real.
 
 Lemma Rmult_integral_contrapositive_currified :
@@ -640,6 +674,7 @@ Lemma Ropp_eq_compat : forall r1 r2, r1 = r2 -> - r1 = - r2.
 Proof.
   auto with real.
 Qed.
+#[global]
 Hint Resolve Ropp_eq_compat: real.
 
 (**********)
@@ -647,6 +682,7 @@ Lemma Ropp_0 : -0 = 0.
 Proof.
   ring.
 Qed.
+#[global]
 Hint Resolve Ropp_0: real.
 
 (**********)
@@ -654,6 +690,7 @@ Lemma Ropp_eq_0_compat : forall r, r = 0 -> - r = 0.
 Proof.
   intros; rewrite H; auto with real.
 Qed.
+#[global]
 Hint Resolve Ropp_eq_0_compat: real.
 
 (**********)
@@ -661,6 +698,7 @@ Lemma Ropp_involutive : forall r, - - r = r.
 Proof.
   intro; ring.
 Qed.
+#[global]
 Hint Resolve Ropp_involutive: real.
 
 (*********)
@@ -670,6 +708,7 @@ Proof.
   apply H.
   transitivity (- - r); auto with real.
 Qed.
+#[global]
 Hint Resolve Ropp_neq_0_compat: real.
 
 (**********)
@@ -677,6 +716,7 @@ Lemma Ropp_plus_distr : forall r1 r2, - (r1 + r2) = - r1 + - r2.
 Proof.
   intros; ring.
 Qed.
+#[global]
 Hint Resolve Ropp_plus_distr: real.
 
 (*********************************************************)
@@ -692,6 +732,7 @@ Lemma Ropp_mult_distr_l_reverse : forall r1 r2, - r1 * r2 = - (r1 * r2).
 Proof.
   intros; ring.
 Qed.
+#[global]
 Hint Resolve Ropp_mult_distr_l_reverse: real.
 
 (**********)
@@ -699,6 +740,7 @@ Lemma Rmult_opp_opp : forall r1 r2, - r1 * - r2 = r1 * r2.
 Proof.
   intros; ring.
 Qed.
+#[global]
 Hint Resolve Rmult_opp_opp: real.
 
 Lemma Ropp_mult_distr_r : forall r1 r2, - (r1 * r2) = r1 * - r2.
@@ -719,12 +761,14 @@ Lemma Rminus_0_r : forall r, r - 0 = r.
 Proof.
   intro; ring.
 Qed.
+#[global]
 Hint Resolve Rminus_0_r: real.
 
 Lemma Rminus_0_l : forall r, 0 - r = - r.
 Proof.
   intro; ring.
 Qed.
+#[global]
 Hint Resolve Rminus_0_l: real.
 
 (**********)
@@ -732,6 +776,7 @@ Lemma Ropp_minus_distr : forall r1 r2, - (r1 - r2) = r2 - r1.
 Proof.
   intros; ring.
 Qed.
+#[global]
 Hint Resolve Ropp_minus_distr: real.
 
 Lemma Ropp_minus_distr' : forall r1 r2, - (r2 - r1) = r1 - r2.
@@ -744,6 +789,7 @@ Lemma Rminus_diag_eq : forall r1 r2, r1 = r2 -> r1 - r2 = 0.
 Proof.
   intros; rewrite H; ring.
 Qed.
+#[global]
 Hint Resolve Rminus_diag_eq: real.
 
 Lemma Rminus_eq_0 x : x - x = 0.
@@ -755,6 +801,7 @@ Proof.
   intros r1 r2; unfold Rminus; rewrite Rplus_comm; intro.
   rewrite <- (Ropp_involutive r2); apply (Rplus_opp_r_uniq (- r2) r1 H).
 Qed.
+#[global]
 Hint Immediate Rminus_diag_uniq: real.
 
 Lemma Rminus_diag_uniq_sym : forall r1 r2, r2 - r1 = 0 -> r1 = r2.
@@ -762,12 +809,14 @@ Proof.
   intros; generalize (Rminus_diag_uniq r2 r1 H); clear H; intro H; rewrite H;
     ring.
 Qed.
+#[global]
 Hint Immediate Rminus_diag_uniq_sym: real.
 
 Lemma Rplus_minus : forall r1 r2, r1 + (r2 - r1) = r2.
 Proof.
   intros; ring.
 Qed.
+#[global]
 Hint Resolve Rplus_minus: real.
 
 (**********)
@@ -776,18 +825,21 @@ Proof.
   red; intros r1 r2 H H0.
   apply H; auto with real.
 Qed.
+#[global]
 Hint Resolve Rminus_eq_contra: real.
 
 Lemma Rminus_not_eq : forall r1 r2, r1 - r2 <> 0 -> r1 <> r2.
 Proof.
   red; intros; elim H; apply Rminus_diag_eq; auto.
 Qed.
+#[global]
 Hint Resolve Rminus_not_eq: real.
 
 Lemma Rminus_not_eq_right : forall r1 r2, r2 - r1 <> 0 -> r1 <> r2.
 Proof.
   red; intros; elim H; rewrite H0; ring.
 Qed.
+#[global]
 Hint Resolve Rminus_not_eq_right: real.
 
 (**********)
@@ -809,6 +861,7 @@ Lemma Rinv_1 : / 1 = 1.
 Proof.
   field.
 Qed.
+#[global]
 Hint Resolve Rinv_1: real.
 
 (*********)
@@ -817,6 +870,7 @@ Proof.
   red; intros; apply R1_neq_R0.
   replace 1 with (/ r * r); auto with real.
 Qed.
+#[global]
 Hint Resolve Rinv_neq_0_compat: real.
 
 (*********)
@@ -824,6 +878,7 @@ Lemma Rinv_involutive : forall r, r <> 0 -> / / r = r.
 Proof.
   intros; field; trivial.
 Qed.
+#[global]
 Hint Resolve Rinv_involutive: real.
 
 (*********)
@@ -857,6 +912,7 @@ Proof.
   transitivity (r2 * (r1 * / r1)); auto with real.
   ring.
 Qed.
+#[global]
 Hint Resolve Rinv_r_simpl_l Rinv_r_simpl_r Rinv_r_simpl_m: real.
 
 (*********)
@@ -878,6 +934,7 @@ Qed.
 
 Lemma Rplus_gt_compat_l : forall r r1 r2, r1 > r2 -> r + r1 > r + r2.
 Proof. eauto using Rplus_lt_compat_l with rorders. Qed.
+#[global]
 Hint Resolve Rplus_gt_compat_l: real.
 
 (**********)
@@ -886,6 +943,7 @@ Proof.
   intros.
   rewrite (Rplus_comm r1 r); rewrite (Rplus_comm r2 r); auto with real.
 Qed.
+#[global]
 Hint Resolve Rplus_lt_compat_r: real.
 
 Lemma Rplus_gt_compat_r : forall r r1 r2, r1 > r2 -> r1 + r > r2 + r.
@@ -901,6 +959,7 @@ Qed.
 
 Lemma Rplus_ge_compat_l : forall r r1 r2, r1 >= r2 -> r + r1 >= r + r2.
 Proof. auto using Rplus_le_compat_l with rorders. Qed.
+#[global]
 Hint Resolve Rplus_ge_compat_l: real.
 
 (**********)
@@ -911,6 +970,7 @@ Proof.
   right; rewrite <- H0; auto with real.
 Qed.
 
+#[global]
 Hint Resolve Rplus_le_compat_l Rplus_le_compat_r: real.
 
 Lemma Rplus_ge_compat_r : forall r r1 r2, r1 >= r2 -> r1 + r >= r2 + r.
@@ -922,6 +982,7 @@ Lemma Rplus_lt_compat :
 Proof.
   intros; apply Rlt_trans with (r2 + r3); auto with real.
 Qed.
+#[global]
 Hint Immediate Rplus_lt_compat: real.
 
 Lemma Rplus_le_compat :
@@ -929,6 +990,7 @@ Lemma Rplus_le_compat :
 Proof.
   intros; apply Rle_trans with (r2 + r3); auto with real.
 Qed.
+#[global]
 Hint Immediate Rplus_le_compat: real.
 
 Lemma Rplus_gt_compat :
@@ -952,6 +1014,7 @@ Proof.
   intros; apply Rle_lt_trans with (r2 + r3); auto with real.
 Qed.
 
+#[global]
 Hint Immediate Rplus_lt_le_compat Rplus_le_lt_compat: real.
 
 Lemma Rplus_gt_ge_compat :
@@ -1091,6 +1154,7 @@ Proof.
   apply CReal_opp_gt_lt_contravar. unfold Rgt in H.
   rewrite Rlt_def in H. apply CRealLtEpsilon. exact H.
 Qed.
+#[global]
 Hint Resolve Ropp_gt_lt_contravar : core.
 
 Lemma Ropp_lt_gt_contravar : forall r1 r2, r1 < r2 -> - r1 > - r2.
@@ -1100,6 +1164,7 @@ Proof.
   apply CReal_opp_gt_lt_contravar. rewrite Rlt_def in H.
   apply CRealLtEpsilon. exact H.
 Qed.
+#[global]
 Hint Resolve Ropp_lt_gt_contravar: real.
 
 (**********)
@@ -1107,6 +1172,7 @@ Lemma Ropp_lt_contravar : forall r1 r2, r2 < r1 -> - r1 < - r2.
 Proof.
   auto with real.
 Qed.
+#[global]
 Hint Resolve Ropp_lt_contravar: real.
 
 Lemma Ropp_gt_contravar : forall r1 r2, r2 > r1 -> - r1 > - r2.
@@ -1117,12 +1183,14 @@ Lemma Ropp_le_ge_contravar : forall r1 r2, r1 <= r2 -> - r1 >= - r2.
 Proof.
   unfold Rge; intros r1 r2 [H| H]; auto with real.
 Qed.
+#[global]
 Hint Resolve Ropp_le_ge_contravar: real.
 
 Lemma Ropp_ge_le_contravar : forall r1 r2, r1 >= r2 -> - r1 <= - r2.
 Proof.
   unfold Rle; intros r1 r2 [H| H]; auto with real.
 Qed.
+#[global]
 Hint Resolve Ropp_ge_le_contravar: real.
 
 (**********)
@@ -1130,6 +1198,7 @@ Lemma Ropp_le_contravar : forall r1 r2, r2 <= r1 -> - r1 <= - r2.
 Proof.
   intros r1 r2 H; elim H; auto with real.
 Qed.
+#[global]
 Hint Resolve Ropp_le_contravar: real.
 
 Lemma Ropp_ge_contravar : forall r1 r2, r2 >= r1 -> - r1 >= - r2.
@@ -1140,12 +1209,14 @@ Lemma Ropp_0_lt_gt_contravar : forall r, 0 < r -> 0 > - r.
 Proof.
   intros; replace 0 with (-0); auto with real.
 Qed.
+#[global]
 Hint Resolve Ropp_0_lt_gt_contravar: real.
 
 Lemma Ropp_0_gt_lt_contravar : forall r, 0 > r -> 0 < - r.
 Proof.
   intros; replace 0 with (-0); auto with real.
 Qed.
+#[global]
 Hint Resolve Ropp_0_gt_lt_contravar: real.
 
 (**********)
@@ -1153,12 +1224,14 @@ Lemma Ropp_lt_gt_0_contravar : forall r, r > 0 -> - r < 0.
 Proof.
   intros; rewrite <- Ropp_0; auto with real.
 Qed.
+#[global]
 Hint Resolve Ropp_lt_gt_0_contravar: real.
 
 Lemma Ropp_gt_lt_0_contravar : forall r, r < 0 -> - r > 0.
 Proof.
   intros; rewrite <- Ropp_0; auto with real.
 Qed.
+#[global]
 Hint Resolve Ropp_gt_lt_0_contravar: real.
 
 (**********)
@@ -1166,12 +1239,14 @@ Lemma Ropp_0_le_ge_contravar : forall r, 0 <= r -> 0 >= - r.
 Proof.
   intros; replace 0 with (-0); auto with real.
 Qed.
+#[global]
 Hint Resolve Ropp_0_le_ge_contravar: real.
 
 Lemma Ropp_0_ge_le_contravar : forall r, 0 >= r -> 0 <= - r.
 Proof.
   intros; replace 0 with (-0); auto with real.
 Qed.
+#[global]
 Hint Resolve Ropp_0_ge_le_contravar: real.
 
 (** *** Cancellation *)
@@ -1182,6 +1257,7 @@ Proof.
   rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y);
     auto with real.
 Qed.
+#[global]
 Hint Immediate Ropp_lt_cancel: real.
 
 Lemma Ropp_gt_cancel : forall r1 r2, - r2 > - r1 -> r1 > r2.
@@ -1194,6 +1270,7 @@ Proof.
   intro H1; rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y);
     rewrite H1; auto with real.
 Qed.
+#[global]
 Hint Immediate Ropp_le_cancel: real.
 
 Lemma Ropp_ge_cancel : forall r1 r2, - r2 >= - r1 -> r1 >= r2.
@@ -1211,6 +1288,7 @@ Lemma Rmult_lt_compat_r : forall r r1 r2, 0 < r -> r1 < r2 -> r1 * r < r2 * r.
 Proof.
   intros; rewrite (Rmult_comm r1 r); rewrite (Rmult_comm r2 r); auto with real.
 Qed.
+#[global]
 Hint Resolve Rmult_lt_compat_r : core.
 
 Lemma Rmult_gt_compat_r : forall r r1 r2, r > 0 -> r1 > r2 -> r1 * r > r2 * r.
@@ -1227,6 +1305,7 @@ Proof.
     auto with real.
   right; rewrite <- H; do 2 rewrite Rmult_0_l; reflexivity.
 Qed.
+#[global]
 Hint Resolve Rmult_le_compat_l: real.
 
 Lemma Rmult_le_compat_r :
@@ -1235,6 +1314,7 @@ Proof.
   intros r r1 r2 H; rewrite (Rmult_comm r1 r); rewrite (Rmult_comm r2 r);
     auto with real.
 Qed.
+#[global]
 Hint Resolve Rmult_le_compat_r: real.
 
 Lemma Rmult_ge_compat_l :
@@ -1256,6 +1336,7 @@ Proof.
   apply Rmult_le_compat_l; auto.
   apply Rle_trans with z; auto.
 Qed.
+#[global]
 Hint Resolve Rmult_le_compat: real.
 
 Lemma Rmult_ge_compat :
@@ -1297,6 +1378,7 @@ Proof.
   do 2 rewrite (Ropp_mult_distr_l_reverse (- r)).
   apply Ropp_le_contravar; auto with real.
 Qed.
+#[global]
 Hint Resolve Rmult_le_compat_neg_l: real.
 
 Lemma Rmult_le_ge_compat_neg_l :
@@ -1304,6 +1386,7 @@ Lemma Rmult_le_ge_compat_neg_l :
 Proof.
   intros; apply Rle_ge; auto with real.
 Qed.
+#[global]
 Hint Resolve Rmult_le_ge_compat_neg_l: real.
 
 Lemma Rmult_lt_gt_compat_neg_l :
@@ -1368,6 +1451,7 @@ Proof.
   replace (r2 + (r1 - r2)) with r1 by ring.
   now rewrite Rplus_0_r.
 Qed.
+#[global]
 Hint Resolve Rlt_minus: real.
 
 Lemma Rgt_minus : forall r1 r2, r1 > r2 -> r1 - r2 > 0.
@@ -1436,6 +1520,7 @@ Proof.
   intros; apply not_eq_sym; apply Rlt_not_eq.
   rewrite Rplus_comm; replace 0 with (0 + 0); auto with real.
 Qed.
+#[global]
 Hint Immediate tech_Rplus: real.
 
 (*********************************************************)
@@ -1458,6 +1543,7 @@ Proof.
   replace 0 with (- r * 0); auto with real.
   replace 0 with (0 * r); auto with real.
 Qed.
+#[global]
 Hint Resolve Rle_0_sqr Rlt_0_sqr: real.
 
 (***********)
@@ -1485,6 +1571,7 @@ Proof.
   replace 1 with (Rsqr 1); auto with real.
   unfold Rsqr; auto with real.
 Qed.
+#[global]
 Hint Resolve Rlt_0_1: real.
 
 Lemma Rle_0_1 : 0 <= 1.
@@ -1504,6 +1591,7 @@ Proof.
   replace 1 with (r * / r); auto with real.
   replace 0 with (r * 0); auto with real.
 Qed.
+#[global]
 Hint Resolve Rinv_0_lt_compat: real.
 
 (*********)
@@ -1514,6 +1602,7 @@ Proof.
   replace 1 with (r * / r); auto with real.
   replace 0 with (r * 0); auto with real.
 Qed.
+#[global]
 Hint Resolve Rinv_lt_0_compat: real.
 
 (*********)
@@ -1543,6 +1632,7 @@ Proof.
   apply Rlt_dichotomy_converse; right.
   red; apply Rlt_trans with (r2 := x); auto with real.
 Qed.
+#[global]
 Hint Resolve Rinv_1_lt_contravar: real.
 
 (*********************************************************)
@@ -1556,6 +1646,7 @@ Proof.
   apply Rlt_le_trans with 1; auto with real.
   pattern 1 at 1; replace 1 with (0 + 1); auto with real.
 Qed.
+#[global]
 Hint Resolve Rle_lt_0_plus_1: real.
 
 (**********)
@@ -1564,6 +1655,7 @@ Proof.
   intros.
   pattern r at 1; replace r with (r + 0); auto with real.
 Qed.
+#[global]
 Hint Resolve Rlt_plus_1: real.
 
 (**********)
@@ -1598,6 +1690,7 @@ Proof.
   repeat rewrite S_INR.
   rewrite Hrecn; ring.
 Qed.
+#[global]
 Hint Resolve plus_INR: real.
 
 (**********)
@@ -1608,6 +1701,7 @@ Proof.
   intros; repeat rewrite S_INR; simpl.
   rewrite H0; ring.
 Qed.
+#[global]
 Hint Resolve minus_INR: real.
 
 (*********)
@@ -1618,6 +1712,7 @@ Proof.
   intros; repeat rewrite S_INR; simpl.
   rewrite plus_INR; rewrite Hrecn; ring.
 Qed.
+#[global]
 Hint Resolve mult_INR: real.
 
 Lemma pow_INR (m n: nat) :  INR (m ^ n) = pow (INR m) n.
@@ -1629,6 +1724,7 @@ Proof.
   simple induction 1; intros; auto with real.
   rewrite S_INR; auto with real.
 Qed.
+#[global]
 Hint Resolve lt_0_INR: real.
 
 Lemma lt_INR : forall n m:nat, (n < m)%nat -> INR n < INR m.
@@ -1637,12 +1733,14 @@ Proof.
   rewrite S_INR; auto with real.
   rewrite S_INR; apply Rlt_trans with (INR m0); auto with real.
 Qed.
+#[global]
 Hint Resolve lt_INR: real.
 
 Lemma lt_1_INR : forall n:nat, (1 < n)%nat -> 1 < INR n.
 Proof.
   apply lt_INR.
 Qed.
+#[global]
 Hint Resolve lt_1_INR: real.
 
 (**********)
@@ -1652,6 +1750,7 @@ Proof.
   simpl; auto with real.
   apply Pos2Nat.is_pos.
 Qed.
+#[global]
 Hint Resolve pos_INR_nat_of_P: real.
 
 (**********)
@@ -1661,6 +1760,7 @@ Proof.
   simpl; auto with real.
   auto with arith real.
 Qed.
+#[global]
 Hint Resolve pos_INR: real.
 
 Lemma INR_lt : forall n m:nat, INR n < INR m -> (n < m)%nat.
@@ -1676,6 +1776,7 @@ Proof.
     rewrite 2!S_INR in H.
     apply Rplus_lt_reg_r with (1 := H).
 Qed.
+#[global]
 Hint Resolve INR_lt: real.
 
 (*********)
@@ -1685,6 +1786,7 @@ Proof.
   rewrite S_INR.
   apply Rle_trans with (INR m0); auto with real.
 Qed.
+#[global]
 Hint Resolve le_INR: real.
 
 (**********)
@@ -1694,6 +1796,7 @@ Proof.
   apply H.
   rewrite H1; trivial.
 Qed.
+#[global]
 Hint Immediate INR_not_0: real.
 
 (**********)
@@ -1704,6 +1807,7 @@ Proof.
   intros; rewrite S_INR.
   apply Rgt_not_eq; red; auto with real.
 Qed.
+#[global]
 Hint Resolve not_0_INR: real.
 
 Lemma not_INR : forall n m:nat, n <> m -> INR n <> INR m.
@@ -1714,6 +1818,7 @@ Proof.
   exfalso; auto.
   apply not_eq_sym; apply Rlt_dichotomy_converse; auto with real.
 Qed.
+#[global]
 Hint Resolve not_INR: real.
 
 Lemma INR_eq : forall n m:nat, INR n = INR m -> n = m.
@@ -1730,6 +1835,7 @@ Proof.
   generalize (INR_lt n m H0); intro; auto with arith.
   generalize (INR_eq n m H0); intro; rewrite H1; auto.
 Qed.
+#[global]
 Hint Resolve INR_le: real.
 
 Lemma not_1_INR : forall n:nat, n <> 1%nat -> INR n <> 1.
@@ -1737,6 +1843,7 @@ Proof.
   intros n.
   apply not_INR.
 Qed.
+#[global]
 Hint Resolve not_1_INR: real.
 
 (*********************************************************)
@@ -1967,10 +2074,15 @@ Proof.
 intros; red; intro; elim H; apply eq_IZR; assumption.
 Qed.
 
+#[global]
 Hint Extern 0 (IZR _ <= IZR _) => apply IZR_le, Zle_bool_imp_le, eq_refl : real.
+#[global]
 Hint Extern 0 (IZR _ >= IZR _) => apply Rle_ge, IZR_le, Zle_bool_imp_le, eq_refl : real.
+#[global]
 Hint Extern 0 (IZR _ <  IZR _) => apply IZR_lt, eq_refl : real.
+#[global]
 Hint Extern 0 (IZR _ >  IZR _) => apply IZR_lt, eq_refl : real.
+#[global]
 Hint Extern 0 (IZR _ <> IZR _) => apply IZR_neq, Zeq_bool_neq, eq_refl : real.
 
 Lemma one_IZR_lt1 : forall n:Z, -1 < IZR n < 1 -> n = 0%Z.
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index 338c939a06..f1c9eb8eee 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -119,6 +119,7 @@ Lemma Rplus_comm : forall r1 r2:R, r1 + r2 = r2 + r1.
 Proof.
   intros. apply Rquot1. do 2 rewrite Rrepr_plus. apply CReal_plus_comm.
 Qed.
+#[global]
 Hint Resolve Rplus_comm: real.
 
 (**********)
@@ -127,6 +128,7 @@ Proof.
   intros. apply Rquot1. repeat rewrite Rrepr_plus.
   apply CReal_plus_assoc.
 Qed.
+#[global]
 Hint Resolve Rplus_assoc: real.
 
 (**********)
@@ -135,6 +137,7 @@ Proof.
   intros. apply Rquot1. rewrite Rrepr_plus, Rrepr_opp, Rrepr_0.
   apply CReal_plus_opp_r.
 Qed.
+#[global]
 Hint Resolve Rplus_opp_r: real.
 
 (**********)
@@ -143,6 +146,7 @@ Proof.
   intros. apply Rquot1. rewrite Rrepr_plus, Rrepr_0.
   apply CReal_plus_0_l.
 Qed.
+#[global]
 Hint Resolve Rplus_0_l: real.
 
 (***********************************************************)
@@ -154,6 +158,7 @@ Lemma Rmult_comm : forall r1 r2:R, r1 * r2 = r2 * r1.
 Proof.
   intros. apply Rquot1. do 2 rewrite Rrepr_mult. apply CReal_mult_comm.
 Qed.
+#[global]
 Hint Resolve Rmult_comm: real.
 
 (**********)
@@ -162,6 +167,7 @@ Proof.
   intros. apply Rquot1. repeat rewrite Rrepr_mult.
   apply CReal_mult_assoc.
 Qed.
+#[global]
 Hint Resolve Rmult_assoc: real.
 
 (**********)
@@ -171,6 +177,7 @@ Proof.
   - contradiction.
   - apply Rquot1. rewrite Rrepr_mult, Rquot2, Rrepr_1. apply CReal_inv_l.
 Qed.
+#[global]
 Hint Resolve Rinv_l: real.
 
 (**********)
@@ -179,6 +186,7 @@ Proof.
   intros. apply Rquot1. rewrite Rrepr_mult, Rrepr_1.
   apply CReal_mult_1_l.
 Qed.
+#[global]
 Hint Resolve Rmult_1_l: real.
 
 (**********)
@@ -197,6 +205,7 @@ Proof.
   pose proof (CRealLt_morph 0%CReal 0%CReal (CRealEq_refl _) 1%CReal 0%CReal H).
   apply (CRealLt_irrefl 0%CReal). apply H0. apply CRealLt_0_1.
 Qed.
+#[global]
 Hint Resolve R1_neq_R0: real.
 
 (*********************************************************)
@@ -211,6 +220,7 @@ Proof.
   rewrite Rrepr_mult, Rrepr_plus, Rrepr_plus, Rrepr_mult, Rrepr_mult.
   apply CReal_mult_plus_distr_l.
 Qed.
+#[global]
 Hint Resolve Rmult_plus_distr_l: real.
 
 (*********************************************************)
@@ -256,6 +266,7 @@ Proof.
   rewrite RbaseSymbolsImpl.Rlt_def in H0. apply CRealLtEpsilon. exact H0.
 Qed.
 
+#[global]
 Hint Resolve Rlt_asym Rplus_lt_compat_l Rmult_lt_compat_l: real.
 
 (**********************************************************)
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index d64e635d0f..4aa6edb2c4 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -102,6 +102,7 @@ Proof.
   apply H; assumption.
 Qed.
 
+#[global]
 Hint Resolve pow_O pow_1 pow_add pow_nonzero: real.
 
 Lemma pow_RN_plus :
@@ -117,6 +118,7 @@ Proof.
   intros x n; elim n; simpl; auto with real.
   intros n0 H' H'0; replace 0 with (x * 0); auto with real.
 Qed.
+#[global]
 Hint Resolve pow_lt: real.
 
 Lemma Rlt_pow_R1 : forall (x:R) (n:nat), 1 < x -> (0 < n)%nat -> 1 < x ^ n.
@@ -132,6 +134,7 @@ Proof.
   apply Rlt_trans with (r2 := 1); auto with real.
   apply H'; auto with arith.
 Qed.
+#[global]
 Hint Resolve Rlt_pow_R1: real.
 
 Lemma Rlt_pow : forall (x:R) (n m:nat), 1 < x -> (n < m)%nat -> x ^ n < x ^ m.
@@ -153,6 +156,7 @@ Proof.
   rewrite le_plus_minus_r; auto with arith; rewrite <- plus_n_O; auto.
   rewrite plus_comm; auto with arith.
 Qed.
+#[global]
 Hint Resolve Rlt_pow: real.
 
 (*********)
@@ -628,6 +632,7 @@ Proof.
     rewrite pow_add; auto with real.
     apply Rinv_mult_distr; apply pow_nonzero; auto.
 Qed.
+#[local]
 Hint Resolve powerRZ_O powerRZ_1 powerRZ_NOR powerRZ_add: real.
 
 Lemma Zpower_nat_powerRZ :
@@ -661,12 +666,14 @@ Lemma powerRZ_lt : forall (x:R) (z:Z), 0 < x -> 0 < x ^Z z.
 Proof.
   intros x z; case z; simpl; auto with real.
 Qed.
+#[local]
 Hint Resolve powerRZ_lt: real.
 
 Lemma powerRZ_le : forall (x:R) (z:Z), 0 < x -> 0 <= x ^Z z.
 Proof.
   intros x z H'; apply Rlt_le; auto with real.
 Qed.
+#[local]
 Hint Resolve powerRZ_le: real.
 
 Lemma Zpower_nat_powerRZ_absolu :
diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v
index 7d0dffdd00..d0d633a0c4 100644
--- a/theories/Relations/Relation_Definitions.v
+++ b/theories/Relations/Relation_Definitions.v
@@ -68,10 +68,13 @@ Section Relation_Definition.
 
 End Relation_Definition.
 
+#[global]
 Hint Unfold reflexive transitive antisymmetric symmetric: sets.
 
+#[global]
 Hint Resolve Build_preorder Build_order Build_equivalence Build_PER
   preord_refl preord_trans ord_refl ord_trans ord_antisym equiv_refl
   equiv_trans equiv_sym per_sym per_trans: sets.
 
+#[global]
 Hint Unfold inclusion same_relation commut: sets.
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index f0f36149d1..520333332a 100644
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -228,8 +228,11 @@ Section Lexicographic_Exponentiation.
 
 End Lexicographic_Exponentiation.
 
+#[global]
 Hint Unfold transp union: sets.
+#[global]
 Hint Resolve t_step rt_step rt_refl rst_step rst_refl: sets.
+#[global]
 Hint Immediate rst_sym: sets.
 
 (* begin hide *)
diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v
index 68d200e189..430f35eecb 100644
--- a/theories/Sets/Classical_sets.v
+++ b/theories/Sets/Classical_sets.v
@@ -77,6 +77,7 @@ Section Ensembles_classical.
   Proof.
     unfold Subtract at 1; auto with sets.
   Qed.
+  #[local]
   Hint Resolve Subtract_intro : sets.
 
   Lemma Subtract_inv :
@@ -123,5 +124,6 @@ Section Ensembles_classical.
 
 End Ensembles_classical.
 
+ #[global]
  Hint Resolve Strict_super_set_contains_new_element Subtract_intro
   not_SIncl_empty: sets.
diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v
index 5027679266..ae7cdc9a0f 100644
--- a/theories/Sets/Constructive_sets.v
+++ b/theories/Sets/Constructive_sets.v
@@ -140,6 +140,7 @@ Section Ensembles_facts.
 
 End Ensembles_facts.
 
+#[global]
 Hint Resolve Singleton_inv Singleton_intro Add_intro1 Add_intro2
   Intersection_inv Couple_inv Setminus_intro Strict_Included_intro
   Strict_Included_strict Noone_in_empty Inhabited_not_empty Add_not_Empty
diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v
index face010746..581c16778d 100644
--- a/theories/Sets/Cpo.v
+++ b/theories/Sets/Cpo.v
@@ -92,6 +92,7 @@ Section Bounds.
       exists bsup : _, Lub X bsup) -> Conditionally_complete.
 End Bounds.
 
+#[global]
 Hint Resolve Totally_ordered_definition Upper_Bound_definition
   Lower_Bound_definition Lub_definition Glb_definition Bottom_definition
   Definition_of_Complete Definition_of_Complete
diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v
index fb33f7834c..96fb070071 100644
--- a/theories/Sets/Ensembles.v
+++ b/theories/Sets/Ensembles.v
@@ -92,8 +92,10 @@ Section Ensembles.
 
 End Ensembles.
 
+#[global]
 Hint Unfold In Included Same_set Strict_Included Add Setminus Subtract: sets.
 
+#[global]
 Hint Resolve Union_introl Union_intror Intersection_intro In_singleton
   Couple_l Couple_r Triple_l Triple_m Triple_r Disjoint_intro
   Extensionality_Ensembles: sets.
diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v
index e8e2a66e98..683979be74 100644
--- a/theories/Sets/Finite_sets.v
+++ b/theories/Sets/Finite_sets.v
@@ -45,7 +45,9 @@ Section Ensembles_finis.
 
 End Ensembles_finis.
 
+#[global]
 Hint Resolve Empty_is_finite Union_is_finite: sets.
+#[global]
 Hint Resolve card_empty card_add: sets.
 
 Require Import Constructive_sets.
diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v
index 023eeaac9d..e83ff223f3 100644
--- a/theories/Sets/Image.v
+++ b/theories/Sets/Image.v
@@ -202,4 +202,5 @@ Section Image.
 
 End Image.
 
+#[global]
 Hint Resolve Im_def image_empty finite_image: sets.
diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v
index b3d7ed0b7b..766f62af45 100644
--- a/theories/Sets/Infinite_sets.v
+++ b/theories/Sets/Infinite_sets.v
@@ -46,6 +46,7 @@ Section Approx.
     Defn_of_Approximant : Finite U X -> Included U X A -> Approximant A X.
 End Approx.
 
+#[global]
 Hint Resolve Defn_of_Approximant : core.
 
 Section Infinite_sets.
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index 4d0cd1174c..3f3cade37d 100644
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -187,7 +187,10 @@ End multiset_defs.
 
 Unset Implicit Arguments.
 
+#[global]
 Hint Unfold meq multiplicity: datatypes.
+#[global]
 Hint Resolve munion_empty_right munion_comm munion_ass meq_left meq_right
   munion_empty_left: datatypes.
+#[global]
 Hint Immediate meq_sym: datatypes.
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v
index 875afe3f44..879a7df608 100644
--- a/theories/Sets/Partial_Order.v
+++ b/theories/Sets/Partial_Order.v
@@ -53,7 +53,9 @@ Section Partial_orders.
 
 End Partial_orders.
 
+#[global]
 Hint Unfold Carrier_of Rel_of Strict_Rel_of: sets.
+#[global]
 Hint Resolve Definition_of_covers: sets.
 
 
diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v
index 96d04100b9..617836225c 100644
--- a/theories/Sets/Powerset.v
+++ b/theories/Sets/Powerset.v
@@ -38,12 +38,14 @@ Variable U : Type.
 Inductive Power_set (A:Ensemble U) : Ensemble (Ensemble U) :=
     Definition_of_Power_set :
       forall X:Ensemble U, Included U X A -> In (Ensemble U) (Power_set A) X.
+#[local]
 Hint Resolve Definition_of_Power_set : core.
 
 Theorem Empty_set_minimal : forall X:Ensemble U, Included U (Empty_set U) X.
 intro X; red.
 intros x H'; elim H'.
 Qed.
+#[local]
 Hint Resolve Empty_set_minimal : core.
 
 Theorem Power_set_Inhabited :
@@ -51,22 +53,26 @@ Theorem Power_set_Inhabited :
 intro X.
 apply Inhabited_intro with (Empty_set U); auto with sets.
 Qed.
+#[local]
 Hint Resolve Power_set_Inhabited : core.
 
 Theorem Inclusion_is_an_order : Order (Ensemble U) (Included U).
 auto 6 with sets.
 Qed.
+#[local]
 Hint Resolve Inclusion_is_an_order : core.
 
 Theorem Inclusion_is_transitive : Transitive (Ensemble U) (Included U).
 elim Inclusion_is_an_order; auto with sets.
 Qed.
+#[local]
 Hint Resolve Inclusion_is_transitive : core.
 
 Definition Power_set_PO : Ensemble U -> PO (Ensemble U).
 intro A; try assumption.
 apply Definition_of_PO with (Power_set A) (Included U); auto with sets.
 Defined.
+#[local]
 Hint Unfold Power_set_PO : core.
 
 Theorem Strict_Rel_is_Strict_Included :
@@ -74,6 +80,7 @@ Theorem Strict_Rel_is_Strict_Included :
    (Strict_Rel_of (Ensemble U) (Power_set_PO (Full_set U))).
 auto with sets.
 Qed.
+#[local]
 Hint Resolve Strict_Rel_Transitive Strict_Rel_is_Strict_Included : core.
 
 Lemma Strict_inclusion_is_transitive_with_inclusion :
@@ -109,6 +116,7 @@ Theorem Empty_set_is_Bottom :
  forall A:Ensemble U, Bottom (Ensemble U) (Power_set_PO A) (Empty_set U).
 intro A; apply Bottom_definition; simpl; auto with sets.
 Qed.
+#[local]
 Hint Resolve Empty_set_is_Bottom : core.
 
 Theorem Union_minimal :
@@ -117,6 +125,7 @@ Theorem Union_minimal :
 intros a b X H' H'0; red.
 intros x H'1; elim H'1; auto with sets.
 Qed.
+#[local]
 Hint Resolve Union_minimal : core.
 
 Theorem Intersection_maximal :
@@ -144,6 +153,7 @@ Theorem Intersection_decreases_r :
 intros a b; red.
 intros x H'; elim H'; auto with sets.
 Qed.
+#[local]
 Hint Resolve Union_increases_l Union_increases_r Intersection_decreases_l
   Intersection_decreases_r : core.
 
@@ -177,14 +187,25 @@ Qed.
 
 End The_power_set_partial_order.
 
+#[global]
 Hint Resolve Empty_set_minimal: sets.
+#[global]
 Hint Resolve Power_set_Inhabited: sets.
+#[global]
 Hint Resolve Inclusion_is_an_order: sets.
+#[global]
 Hint Resolve Inclusion_is_transitive: sets.
+#[global]
 Hint Resolve Union_minimal: sets.
+#[global]
 Hint Resolve Union_increases_l: sets.
+#[global]
 Hint Resolve Union_increases_r: sets.
+#[global]
 Hint Resolve Intersection_decreases_l: sets.
+#[global]
 Hint Resolve Intersection_decreases_r: sets.
+#[global]
 Hint Resolve Empty_set_is_Bottom: sets.
+#[global]
 Hint Resolve Strict_inclusion_is_transitive: sets.
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v
index b83485bbf3..0fe63c5b66 100644
--- a/theories/Sets/Powerset_Classical_facts.v
+++ b/theories/Sets/Powerset_Classical_facts.v
@@ -92,6 +92,7 @@ Section Sets_as_an_algebra.
     apply Subtract_intro; auto with sets.
     red; intro H'1; apply H'; rewrite H'1; auto with sets.
   Qed.
+  #[local]
   Hint Resolve incl_soustr_add_r: sets.
 
   Lemma add_soustr_2 :
@@ -330,9 +331,15 @@ Section Sets_as_an_algebra.
 
 End Sets_as_an_algebra.
 
+#[global]
 Hint Resolve incl_soustr_in: sets.
+#[global]
 Hint Resolve incl_soustr: sets.
+#[global]
 Hint Resolve incl_soustr_add_l: sets.
+#[global]
 Hint Resolve incl_soustr_add_r: sets.
+#[global]
 Hint Resolve add_soustr_1 add_soustr_2: sets.
+#[global]
 Hint Resolve add_soustr_xy: sets.
diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v
index 69b28f14e4..b21c48d305 100644
--- a/theories/Sets/Powerset_facts.v
+++ b/theories/Sets/Powerset_facts.v
@@ -348,6 +348,7 @@ Section Sets_as_an_algebra.
 
 End Sets_as_an_algebra.
 
+#[global]
 Hint Resolve Empty_set_zero Empty_set_zero' Union_associative Union_add
   singlx incl_add: sets.
 
diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v
index 42755b551f..1167ad36bf 100644
--- a/theories/Sets/Relations_1.v
+++ b/theories/Sets/Relations_1.v
@@ -61,7 +61,9 @@ Section Relations_1.
        Definition_of_PER : Symmetric -> Transitive -> PER.
 
 End Relations_1.
+#[global]
 Hint Unfold Reflexive Transitive Antisymmetric Symmetric contains
   same_relation: sets.
+#[global]
 Hint Resolve Definition_of_preorder Definition_of_order
   Definition_of_equivalence Definition_of_PER: sets.
diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v
index 21fc7ceaf2..6d7b837b63 100644
--- a/theories/Sets/Relations_1_facts.v
+++ b/theories/Sets/Relations_1_facts.v
@@ -52,6 +52,7 @@ apply Definition_of_equivalence.
   split; apply H'1 with y; auto 10 with sets.
 - red; intros x y h; elim h; intros H'3 H'4; auto 10 with sets.
 Qed.
+#[global]
 Hint Resolve Equiv_from_preorder : core.
 
 Theorem Equiv_from_order :
@@ -60,6 +61,7 @@ Theorem Equiv_from_order :
 Proof.
 intros U R H'; elim H'; auto 10 with sets.
 Qed.
+#[global]
 Hint Resolve Equiv_from_order : core.
 
 Theorem contains_is_preorder :
@@ -67,6 +69,7 @@ Theorem contains_is_preorder :
 Proof.
 auto 10 with sets.
 Qed.
+#[global]
 Hint Resolve contains_is_preorder : core.
 
 Theorem same_relation_is_equivalence :
@@ -74,6 +77,7 @@ Theorem same_relation_is_equivalence :
 Proof.
 unfold same_relation at 1; auto 10 with sets.
 Qed.
+#[global]
 Hint Resolve same_relation_is_equivalence : core.
 
 Theorem cong_reflexive_same_relation :
diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v
index 5e3206dd9b..e180798d1f 100644
--- a/theories/Sets/Relations_2.v
+++ b/theories/Sets/Relations_2.v
@@ -50,7 +50,11 @@ Definition Strongly_confluent : Prop :=
 
 End Relations_2.
 
+#[global]
 Hint Resolve Rstar_0: sets.
+#[global]
 Hint Resolve Rstar1_0: sets.
+#[global]
 Hint Resolve Rstar1_1: sets.
+#[global]
 Hint Resolve Rplus_0: sets.
diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v
index 9ebbba485c..d5c4040033 100644
--- a/theories/Sets/Relations_3.v
+++ b/theories/Sets/Relations_3.v
@@ -53,10 +53,16 @@ Section Relations_3.
    Definition Noetherian : Prop := forall x:U, noetherian x.
 
 End Relations_3.
+#[global]
 Hint Unfold coherent: sets.
+#[global]
 Hint Unfold locally_confluent: sets.
+#[global]
 Hint Unfold confluent: sets.
+#[global]
 Hint Unfold Confluent: sets.
+#[global]
 Hint Resolve definition_of_noetherian: sets.
+#[global]
 Hint Unfold Noetherian: sets.
 
diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v
index db51186ef1..9f4869a625 100644
--- a/theories/Sets/Relations_3_facts.v
+++ b/theories/Sets/Relations_3_facts.v
@@ -38,6 +38,7 @@ Proof.
 intros U R x y H'; red.
 exists y; auto with sets.
 Qed.
+#[global]
 Hint Resolve Rstar_imp_coherent : core.
 
 Theorem coherent_symmetric :
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
index 474b417e8e..d8fe7f6dbe 100644
--- a/theories/Sets/Uniset.v
+++ b/theories/Sets/Uniset.v
@@ -41,20 +41,24 @@ Definition Singleton (a:A) :=
        end).
 
 Definition In (s:uniset) (a:A) : Prop := charac s a = true.
+#[local]
 Hint Unfold In : core.
 
 (** uniset inclusion *)
 Definition incl (s1 s2:uniset) := forall a:A, Bool.le (charac s1 a) (charac s2 a).
+#[local]
 Hint Unfold incl : core.
 
 (** uniset equality *)
 Definition seq (s1 s2:uniset) := forall a:A, charac s1 a = charac s2 a.
+#[local]
 Hint Unfold seq : core.
 
 Lemma le_refl : forall b, Bool.le b b.
 Proof.
 destruct b; simpl; auto.
 Qed.
+#[local]
 Hint Resolve le_refl : core.
 
 Lemma incl_left : forall s1 s2:uniset, seq s1 s2 -> incl s1 s2.
@@ -71,6 +75,7 @@ Lemma seq_refl : forall x:uniset, seq x x.
 Proof.
 destruct x; unfold seq; auto.
 Qed.
+#[local]
 Hint Resolve seq_refl : core.
 
 Lemma seq_trans : forall x y z:uniset, seq x y -> seq y z -> seq x z.
@@ -94,6 +99,7 @@ Lemma union_empty_left : forall x:uniset, seq x (union Emptyset x).
 Proof.
 unfold seq; unfold union; simpl; auto.
 Qed.
+#[local]
 Hint Resolve union_empty_left : core.
 
 Lemma union_empty_right : forall x:uniset, seq x (union x Emptyset).
@@ -101,6 +107,7 @@ Proof.
 unfold seq; unfold union; simpl.
 intros x a; rewrite (orb_b_false (charac x a)); auto.
 Qed.
+#[local]
 Hint Resolve union_empty_right : core.
 
 Lemma union_comm : forall x y:uniset, seq (union x y) (union y x).
@@ -108,6 +115,7 @@ Proof.
 unfold seq; unfold charac; unfold union.
 destruct x; destruct y; auto with bool.
 Qed.
+#[local]
 Hint Resolve union_comm : core.
 
 Lemma union_ass :
@@ -116,6 +124,7 @@ Proof.
 unfold seq; unfold union; unfold charac.
 destruct x; destruct y; destruct z; auto with bool.
 Qed.
+#[local]
 Hint Resolve union_ass : core.
 
 Lemma seq_left : forall x y z:uniset, seq x y -> seq (union x z) (union y z).
@@ -124,6 +133,7 @@ unfold seq; unfold union; unfold charac.
 destruct x; destruct y; destruct z.
 intros; elim H; auto.
 Qed.
+#[local]
 Hint Resolve seq_left : core.
 
 Lemma seq_right : forall x y z:uniset, seq x y -> seq (union z x) (union z y).
@@ -132,6 +142,7 @@ unfold seq; unfold union; unfold charac.
 destruct x; destruct y; destruct z.
 intros; elim H; auto.
 Qed.
+#[local]
 Hint Resolve seq_right : core.
 
 
diff --git a/theories/Sorting/CPermutation.v b/theories/Sorting/CPermutation.v
index 31d9f7f0ed..cebb0c808c 100644
--- a/theories/Sorting/CPermutation.v
+++ b/theories/Sorting/CPermutation.v
@@ -96,6 +96,7 @@ Qed.
 
 End CPermutation.
 
+#[global]
 Hint Resolve CPermutation_refl : core.
 
 (* These hints do not reduce the size of the problem to solve and they
diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
index 1130c9dd76..05a21620b7 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -36,7 +36,9 @@ Section defs.
   Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z.
   Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y.
 
+  #[local]
   Hint Resolve leA_refl : core.
+  #[local]
   Hint Immediate eqA_dec leA_dec leA_antisym : core.
 
   Let emptyBag := EmptyBag A.
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index 2f445c341a..45fb48ad5d 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -76,6 +76,7 @@ Qed.
 
 End Permutation.
 
+#[global]
 Hint Resolve Permutation_refl perm_nil perm_skip : core.
 
 (* These hints do not reduce the size of the problem to solve and they
diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v
index 8cba461082..206eb606d2 100644
--- a/theories/Sorting/Sorted.v
+++ b/theories/Sorting/Sorted.v
@@ -137,7 +137,9 @@ Section defs.
 
 End defs.
 
+#[global]
 Hint Constructors HdRel : core.
+#[global]
 Hint Constructors Sorted : core.
 
 (* begin hide *)
diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v
index 0c3bd9393b..c923b503a7 100644
--- a/theories/Structures/DecidableType.v
+++ b/theories/Structures/DecidableType.v
@@ -38,7 +38,9 @@ Module KeyDecidableType(D:DecidableType).
   Definition eqke (p p':key*elt) :=
           eq (fst p) (fst p') /\ (snd p) = (snd p').
 
+  #[local]
   Hint Unfold eqk eqke : core.
+  #[local]
   Hint Extern 2 (eqke ?a ?b) => split : core.
 
    (* eqke is stricter than eqk *)
@@ -70,7 +72,9 @@ Module KeyDecidableType(D:DecidableType).
     unfold eqke; intuition; [ eauto | congruence ].
   Qed.
 
+  #[local]
   Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core.
+  #[local]
   Hint Immediate eqk_sym eqke_sym : core.
 
   Global Instance eqk_equiv : Equivalence eqk.
@@ -84,6 +88,7 @@ Module KeyDecidableType(D:DecidableType).
   Proof.
     unfold eqke; induction 1; intuition. 
   Qed.
+  #[local]
   Hint Resolve InA_eqke_eqk : core.
 
   Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m.
@@ -94,6 +99,7 @@ Module KeyDecidableType(D:DecidableType).
   Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
   Definition In k m := exists e:elt, MapsTo k e m.
 
+  #[local]
   Hint Unfold MapsTo In : core.
 
   (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *)
@@ -140,12 +146,19 @@ Module KeyDecidableType(D:DecidableType).
 
  End Elt.
 
+ #[global]
  Hint Unfold eqk eqke : core.
+ #[global]
  Hint Extern 2 (eqke ?a ?b) => split : core.
+ #[global]
  Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core.
+ #[global]
  Hint Immediate eqk_sym eqke_sym : core.
+ #[global]
  Hint Resolve InA_eqke_eqk : core.
+ #[global]
  Hint Unfold MapsTo In : core.
+ #[global]
  Hint Resolve In_inv_2 In_inv_3 : core.
 
 End KeyDecidableType.
diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v
index 914361d718..7cd5943a3f 100644
--- a/theories/Structures/Equalities.v
+++ b/theories/Structures/Equalities.v
@@ -53,7 +53,9 @@ Module Type IsEqOrig (Import E:Eq').
   Axiom eq_refl : forall x : t, x==x.
   Axiom eq_sym : forall x y : t, x==y -> y==x.
   Axiom eq_trans : forall x y z : t, x==y -> y==z -> x==z.
+  #[global]
   Hint Immediate eq_sym : core.
+  #[global]
   Hint Resolve eq_refl eq_trans : core.
 End IsEqOrig.
 
diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v
index fe9794de8a..523240065d 100644
--- a/theories/Structures/EqualitiesFacts.v
+++ b/theories/Structures/EqualitiesFacts.v
@@ -22,6 +22,7 @@ Module KeyDecidableType(D:DecidableType).
  Definition eqk {elt} : relation (key*elt) := D.eq @@1.
  Definition eqke {elt} : relation (key*elt) := D.eq * Logic.eq.
 
+ #[global]
  Hint Unfold eqk eqke : core.
 
  (** eqk, eqke are equalities *)
@@ -60,6 +61,7 @@ Module KeyDecidableType(D:DecidableType).
  Lemma eqk_1 {elt} k k' (e e':elt) : eqk (k,e) (k',e') -> D.eq k k'.
  Proof. trivial. Qed.
 
+ #[global]
  Hint Resolve eqke_1 eqke_2 eqk_1 : core.
 
  (* Additional facts *)
@@ -69,6 +71,7 @@ Module KeyDecidableType(D:DecidableType).
  Proof.
   induction 1; firstorder.
  Qed.
+ #[global]
  Hint Resolve InA_eqke_eqk : core.
 
  Lemma InA_eqk_eqke {elt} p (m:list (key*elt)) :
@@ -86,6 +89,7 @@ Module KeyDecidableType(D:DecidableType).
  Definition MapsTo {elt} (k:key)(e:elt):= InA eqke (k,e).
  Definition In {elt} k m := exists e:elt, MapsTo k e m.
 
+ #[global]
  Hint Unfold MapsTo In : core.
 
  (* Alternative formulations for [In k l] *)
@@ -167,8 +171,11 @@ Module KeyDecidableType(D:DecidableType).
   eauto with *.
  Qed.
 
+ #[global]
  Hint Extern 2 (eqke ?a ?b) => split : core.
+ #[global]
  Hint Resolve InA_eqke_eqk : core.
+ #[global]
  Hint Resolve In_inv_2 In_inv_3 : core.
 
 End KeyDecidableType.
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index ecf0706a4f..dc7a48cd6b 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -44,7 +44,9 @@ Module Type MiniOrderedType.
 
   Parameter compare : forall x y : t, Compare lt eq x y.
 
+  #[global]
   Hint Immediate eq_sym : ordered_type.
+  #[global]
   Hint Resolve eq_refl eq_trans lt_not_eq lt_trans : ordered_type.
 
 End MiniOrderedType.
@@ -144,8 +146,11 @@ Module OrderedTypeFacts (Import O: OrderedType).
   Lemma eq_not_gt x y : eq x y -> ~ lt y x. Proof. order. Qed.
   Lemma lt_not_gt x y : lt x y -> ~ lt y x. Proof. order. Qed.
 
+  #[global]
   Hint Resolve gt_not_eq eq_not_lt : ordered_type.
+  #[global]
   Hint Immediate eq_lt lt_eq le_eq eq_le neq_eq eq_neq : ordered_type.
+  #[global]
   Hint Resolve eq_not_gt lt_antirefl lt_not_gt : ordered_type.
 
   Lemma elim_compare_eq :
@@ -248,7 +253,9 @@ Proof. exact (SortA_NoDupA eq_equiv lt_strorder lt_compat). Qed.
 
 End ForNotations.
 
+#[global]
 Hint Resolve ListIn_In Sort_NoDup Inf_lt : ordered_type.
+#[global]
 Hint Immediate In_eq Inf_lt : ordered_type.
 
 End OrderedTypeFacts.
@@ -267,7 +274,9 @@ Module KeyOrderedType(O:OrderedType).
           eq (fst p) (fst p') /\ (snd p) = (snd p').
   Definition ltk (p p':key*elt) := lt (fst p) (fst p').
 
+  #[local]
   Hint Unfold eqk eqke ltk : ordered_type.
+  #[local]
   Hint Extern 2 (eqke ?a ?b) => split : ordered_type.
 
    (* eqke is stricter than eqk *)
@@ -284,6 +293,7 @@ Module KeyOrderedType(O:OrderedType).
 
    Lemma ltk_right_l : forall x k e e', ltk (k,e) x -> ltk (k,e') x.
    Proof. auto. Qed.
+  #[local]
    Hint Immediate ltk_right_r ltk_right_l : ordered_type.
 
   (* eqk, eqke are equalities, ltk is a strict order *)
@@ -320,8 +330,11 @@ Module KeyOrderedType(O:OrderedType).
     exact (lt_not_eq H H1).
   Qed.
 
+  #[local]
   Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : ordered_type.
+  #[local]
   Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : ordered_type.
+  #[local]
   Hint Immediate eqk_sym eqke_sym : ordered_type.
 
   Global Instance eqk_equiv : Equivalence eqk.
@@ -360,7 +373,9 @@ Module KeyOrderedType(O:OrderedType).
       intros (k,e) (k',e') (k'',e'').
       unfold ltk, eqk; simpl; eauto with ordered_type.
   Qed.
+  #[local]
   Hint Resolve eqk_not_ltk : ordered_type.
+  #[local]
   Hint Immediate ltk_eqk eqk_ltk : ordered_type.
 
   Lemma InA_eqke_eqk :
@@ -368,6 +383,7 @@ Module KeyOrderedType(O:OrderedType).
   Proof.
     unfold eqke; induction 1; intuition.
   Qed.
+  #[local]
   Hint Resolve InA_eqke_eqk : ordered_type.
 
   Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
@@ -375,6 +391,7 @@ Module KeyOrderedType(O:OrderedType).
   Notation Sort := (sort ltk).
   Notation Inf := (lelistA ltk).
 
+  #[local]
   Hint Unfold MapsTo In : ordered_type.
 
   (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *)
@@ -406,7 +423,9 @@ Module KeyOrderedType(O:OrderedType).
   Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l.
   Proof. exact (InfA_ltA ltk_strorder). Qed.
 
+  #[local]
   Hint Immediate Inf_eq : ordered_type.
+  #[local]
   Hint Resolve Inf_lt : ordered_type.
 
   Lemma Sort_Inf_In :
@@ -470,18 +489,31 @@ Module KeyOrderedType(O:OrderedType).
 
  End Elt.
 
+ #[global]
  Hint Unfold eqk eqke ltk : ordered_type.
+ #[global]
  Hint Extern 2 (eqke ?a ?b) => split : ordered_type.
+ #[global]
  Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : ordered_type.
+ #[global]
  Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : ordered_type.
+ #[global]
  Hint Immediate eqk_sym eqke_sym : ordered_type.
+ #[global]
  Hint Resolve eqk_not_ltk : ordered_type.
+ #[global]
  Hint Immediate ltk_eqk eqk_ltk : ordered_type.
+ #[global]
  Hint Resolve InA_eqke_eqk : ordered_type.
+ #[global]
  Hint Unfold MapsTo In : ordered_type.
+ #[global]
  Hint Immediate Inf_eq : ordered_type.
+ #[global]
  Hint Resolve Inf_lt : ordered_type.
+ #[global]
  Hint Resolve Sort_Inf_NotIn : ordered_type.
+ #[global]
  Hint Resolve In_inv_2 In_inv_3 : ordered_type.
 
 End KeyOrderedType.
diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v
index b3e3b6e853..b4ddd0b262 100644
--- a/theories/Structures/Orders.v
+++ b/theories/Structures/Orders.v
@@ -181,6 +181,7 @@ Module OTF_to_TotalOrder (O:OrderedTypeFull) <: TotalOrder
     we coerce [bool] into [Prop]. *)
 
 Local Coercion is_true : bool >-> Sortclass.
+#[global]
 Hint Unfold is_true : core.
 
 Module Type HasLeb (Import T:Typ).
diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v
index 3a5dbc2f88..bace70cbee 100644
--- a/theories/Structures/OrdersLists.v
+++ b/theories/Structures/OrdersLists.v
@@ -50,7 +50,9 @@ Proof. exact (InfA_alt O.eq_equiv O.lt_strorder O.lt_compat). Qed.
 Lemma Sort_NoDup : forall l, Sort l -> NoDup l.
 Proof. exact (SortA_NoDupA O.eq_equiv O.lt_strorder O.lt_compat) . Qed.
 
+#[global]
 Hint Resolve ListIn_In Sort_NoDup Inf_lt : core.
+#[global]
 Hint Immediate In_eq Inf_lt : core.
 
 End OrderedTypeLists.
@@ -66,6 +68,7 @@ Module KeyOrderedType(O:OrderedType).
 
  Definition ltk {elt} : relation (key*elt) := O.lt @@1.
 
+ #[global]
  Hint Unfold ltk : core.
 
  (* ltk is a strict order *)
@@ -109,7 +112,9 @@ Module KeyOrderedType(O:OrderedType).
   Lemma Inf_lt l x x' : ltk x x' -> Inf x' l -> Inf x l.
   Proof. apply InfA_ltA; auto with *. Qed.
 
+  #[local]
   Hint Immediate Inf_eq : core.
+  #[local]
   Hint Resolve Inf_lt : core.
 
   Lemma Sort_Inf_In l p q : Sort l -> Inf q l -> InA eqk p l -> ltk q p.
@@ -148,9 +153,13 @@ Module KeyOrderedType(O:OrderedType).
 
  End Elt.
 
+ #[global]
  Hint Resolve ltk_not_eqk ltk_not_eqke : core.
+ #[global]
  Hint Immediate Inf_eq : core.
+ #[global]
  Hint Resolve Inf_lt : core.
+ #[global]
  Hint Resolve Sort_Inf_NotIn : core.
 
 End KeyOrderedType.
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index a154a2b269..3799ffaca9 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -279,27 +279,32 @@ Section SCANNING.
 Inductive Forall {A} (P: A -> Prop): forall {n} (v: t A n), Prop :=
  |Forall_nil: Forall P []
  |Forall_cons {n} x (v: t A n): P x -> Forall P v -> Forall P (x::v).
+#[local]
 Hint Constructors Forall : core.
 
 Inductive Exists {A} (P:A->Prop): forall {n}, t A n -> Prop :=
  |Exists_cons_hd {m} x (v: t A m): P x -> Exists P (x::v)
  |Exists_cons_tl {m} x (v: t A m): Exists P v -> Exists P (x::v).
+#[local]
 Hint Constructors Exists : core.
 
 Inductive In {A} (a:A): forall {n}, t A n -> Prop :=
  |In_cons_hd {m} (v: t A m): In a (a::v)
  |In_cons_tl {m} x (v: t A m): In a v -> In a (x::v).
+#[local]
 Hint Constructors In : core.
 
 Inductive Forall2 {A B} (P:A->B->Prop): forall {n}, t A n -> t B n -> Prop :=
  |Forall2_nil: Forall2 P [] []
  |Forall2_cons {m} x1 x2 (v1:t A m) v2: P x1 x2 -> Forall2 P v1 v2 ->
     Forall2 P (x1::v1) (x2::v2).
+#[local]
 Hint Constructors Forall2 : core.
 
 Inductive Exists2 {A B} (P:A->B->Prop): forall {n}, t A n -> t B n -> Prop :=
  |Exists2_cons_hd {m} x1 x2 (v1: t A m) (v2: t B m): P x1 x2 -> Exists2 P (x1::v1) (x2::v2)
  |Exists2_cons_tl {m} x1 x2 (v1:t A m) v2: Exists2 P v1 v2 -> Exists2 P (x1::v1) (x2::v2).
+#[local]
 Hint Constructors Exists2 : core.
 
 End SCANNING.
diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v
index 474836d53d..cafa849b1b 100644
--- a/theories/Wellfounded/Inclusion.v
+++ b/theories/Wellfounded/Inclusion.v
@@ -22,6 +22,7 @@ Section WfInclusion.
     apply Acc_intro; auto with sets.
   Qed.
 
+  #[local]
   Hint Resolve Acc_incl : core.
 
   Theorem wf_incl : inclusion A R1 R2 -> well_founded R2 -> well_founded R1.
diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v
index 2d139504f3..49c2dd8602 100644
--- a/theories/Wellfounded/Transitive_Closure.v
+++ b/theories/Wellfounded/Transitive_Closure.v
@@ -31,6 +31,7 @@ Section Wf_Transitive_Closure.
     apply Acc_inv with y; auto with sets.
   Defined.
 
+  #[local]
   Hint Resolve Acc_clos_trans : core.
 
   Lemma Acc_inv_trans : forall x y:A, trans_clos y x -> Acc R x -> Acc R y.
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 52998c8b95..47137414dc 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1754,6 +1754,7 @@ Proof. congruence. Qed.
 Lemma Zpos_eq_iff : forall p q, p = q <-> Z.pos p = Z.pos q.
 Proof (fun p q => iff_sym (Pos2Z.inj_iff p q)).
 
+#[global]
 Hint Immediate Zsucc_pred: zarith.
 
 (* Not kept :
diff --git a/theories/ZArith/ZArith_base.v b/theories/ZArith/ZArith_base.v
index 26cd3e1e4d..cae918b4b6 100644
--- a/theories/ZArith/ZArith_base.v
+++ b/theories/ZArith/ZArith_base.v
@@ -30,6 +30,7 @@ Require Export Zbool.
 Require Export Zmisc.
 Require Export Wf_Z.
 
+#[global]
 Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l
   Z.add_0_r Z.mul_1_l Z.add_opp_diag_l Z.add_opp_diag_r Z.mul_add_distr_l
   Z.mul_add_distr_r: zarith.
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 2039dc0bee..13adda412d 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -75,6 +75,7 @@ Proof.
     + apply Pos2Z.neg_is_nonpos.
 Qed.
 
+#[global]
 Hint Unfold Remainder : core.
 
 (** Now comes the fully general result about Euclidean division. *)
@@ -203,6 +204,7 @@ Proof. intros a. zero_or_not a. apply Z.mod_1_r. Qed.
 Lemma Zdiv_1_r: forall a, a/1 = a.
 Proof. intros a. zero_or_not a. apply Z.div_1_r. Qed.
 
+#[global]
 Hint Resolve Zmod_0_l Zmod_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_1_r
  : zarith.
 
diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v
index 0448bcf41b..d3a9d7baac 100644
--- a/theories/ZArith/Zeven.v
+++ b/theories/ZArith/Zeven.v
@@ -130,6 +130,7 @@ Proof.
  boolify_even_odd. now rewrite Z.odd_pred.
 Qed.
 
+#[global]
 Hint Unfold Zeven Zodd: zarith.
 
 Notation Zeven_bool_succ := Z.even_succ (only parsing).
diff --git a/theories/ZArith/Zhints.v b/theories/ZArith/Zhints.v
index 95266186eb..80073bdbdf 100644
--- a/theories/ZArith/Zhints.v
+++ b/theories/ZArith/Zhints.v
@@ -40,6 +40,7 @@ Require Import Wf_Z.
 
 (** No subgoal or smaller subgoals                                     *)
 
+#[global]
 Hint Resolve
   (** ** Reversible simplification lemmas (no loss of information)      *)
   (** Should clearly be declared as hints                               *)
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index cad9454906..861c204ab8 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -65,8 +65,11 @@ Proof. apply Z.divide_abs_l. Qed.
 Theorem Zdivide_Zabs_inv_l a b : (a | b) -> (Z.abs a | b).
 Proof. apply Z.divide_abs_l. Qed.
 
+#[global]
 Hint Resolve Z.divide_refl Z.divide_1_l Z.divide_0_r: zarith.
+#[global]
 Hint Resolve Z.mul_divide_mono_l Z.mul_divide_mono_r: zarith.
+#[global]
 Hint Resolve Z.divide_add_r Zdivide_opp_r Zdivide_opp_r_rev Zdivide_opp_l
   Zdivide_opp_l_rev Z.divide_sub_r Z.divide_mul_l Z.divide_mul_r
   Z.divide_factor_l Z.divide_factor_r: zarith.
@@ -236,6 +239,7 @@ Proof.
   intros; apply Zis_gcd_opp; apply Zis_gcd_0; auto.
 Qed.
 
+#[global]
 Hint Resolve Zis_gcd_sym Zis_gcd_0 Zis_gcd_minus Zis_gcd_opp: zarith.
 
 Theorem Zis_gcd_unique: forall a b c d : Z,
@@ -646,6 +650,7 @@ Proof.
   - absurd (p | a); intuition.
 Qed.
 
+#[global]
 Hint Resolve prime_rel_prime: zarith.
 
 (** As a consequence, a prime number is relatively prime with smaller numbers *)
@@ -866,6 +871,7 @@ Notation Zgcd_Zabs := Z.gcd_abs_l (only parsing).
 Notation Zgcd_0 := Z.gcd_0_r (only parsing).
 Notation Zgcd_1 := Z.gcd_1_r (only parsing).
 
+#[global]
 Hint Resolve Z.gcd_0_r Z.gcd_1_r : zarith.
 
 Theorem Zgcd_1_rel_prime : forall a b,
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 949a01860f..4c533ac458 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -132,6 +132,7 @@ Register not_Zne as plugins.omega.not_Zne.
 
 Notation Zeq_le := Z.eq_le_incl (only parsing).
 
+#[global]
 Hint Resolve Z.le_refl: zarith.
 
 (** Antisymmetry *)
@@ -196,6 +197,7 @@ Proof.
   Z.swap_greater. Z.order.
 Qed.
 
+#[global]
 Hint Resolve Z.le_trans: zarith.
 
 (** * Compatibility of order and operations on Z *)
@@ -219,6 +221,7 @@ Proof.
   Z.swap_greater. apply Z.succ_lt_mono.
 Qed.
 
+#[global]
 Hint Resolve Zsucc_le_compat: zarith.
 
 (** Simplification of successor wrt to order *)
@@ -302,7 +305,9 @@ Proof.
   intros. now apply Z.lt_le_incl, Z.le_succ_l.
 Qed.
 
+#[global]
 Hint Resolve Z.le_succ_diag_r: zarith.
+#[global]
 Hint Resolve Z.le_le_succ_r: zarith.
 
 (** Relating order wrt successor and order wrt predecessor *)
@@ -357,6 +362,7 @@ Proof.
   intros n; induction n; simpl; intros. apply Z.le_refl. easy.
 Qed.
 
+#[global]
 Hint Immediate Z.eq_le_incl: zarith.
 
 (** Derived lemma *)
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v
index c36ddad823..b69af424b1 100644
--- a/theories/ZArith/Zpow_facts.v
+++ b/theories/ZArith/Zpow_facts.v
@@ -57,6 +57,7 @@ Proof. apply Z.pow_gt_1. Qed.
 Theorem Zmult_power p q r : 0 <= r -> (p*q)^r = p^r * q^r.
 Proof. intros. apply Z.pow_mul_l. Qed.
 
+#[global]
 Hint Resolve Z.pow_nonneg Z.pow_pos_nonneg : zarith.
 
 Theorem Zpower_le_monotone3 a b c :
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index ae12295ca4..6f464d89bb 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -79,7 +79,9 @@ Proof.
  now apply (Z.pow_add_r z (Zpos n) (Zpos m)).
 Qed.
 
+#[global]
 Hint Immediate Zpower_nat_is_exp Zpower_pos_is_exp : zarith.
+#[global]
 Hint Unfold Z.pow_pos Zpower_nat: zarith.
 
 Theorem Zpower_exp x n m :
@@ -226,7 +228,9 @@ Section Powers_of_2.
 
 End Powers_of_2.
 
+#[global]
 Hint Resolve two_p_gt_ZERO: zarith.
+#[global]
 Hint Immediate two_p_pred two_p_S: zarith.
 
 Section power_div_with_rest.
diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v
index f95831436a..943376ecfd 100644
--- a/theories/ZArith/Zquot.v
+++ b/theories/ZArith/Zquot.v
@@ -57,6 +57,7 @@ Proof. now destruct a. Qed.
 Lemma Zquot_0_l a : 0÷a = 0.
 Proof. now destruct a. Qed.
 
+#[global]
 Hint Resolve Zrem_0_l Zrem_0_r Zquot_0_l Zquot_0_r Z.quot_1_r Z.rem_1_r
  : zarith.
 
diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v
index 2ff6805c78..81d2a2d70d 100644
--- a/theories/ZArith/Zwf.v
+++ b/theories/ZArith/Zwf.v
@@ -57,6 +57,7 @@ Section wf_proof.
 
 End wf_proof.
 
+#[global]
 Hint Resolve Zwf_well_founded: datatypes.
 
 
@@ -87,4 +88,5 @@ Section wf_proof_up.
 
 End wf_proof_up.
 
+#[global]
 Hint Resolve Zwf_up_well_founded: datatypes.
diff --git a/theories/btauto/Algebra.v b/theories/btauto/Algebra.v
index 4a603f2c52..08bb49a449 100644
--- a/theories/btauto/Algebra.v
+++ b/theories/btauto/Algebra.v
@@ -10,6 +10,7 @@ end.
 
 Arguments decide P /H.
 
+#[global]
 Hint Extern 5 => progress bool : core.
 
 Ltac define t x H :=
@@ -147,6 +148,7 @@ Qed.
 
 (** * The core reflexive part. *)
 
+#[local]
 Hint Constructors valid : core.
 
 Fixpoint beq_poly pl pr :=
@@ -315,6 +317,7 @@ Section Validity.
 
 (* Decision procedure of validity *)
 
+#[local]
 Hint Constructors valid linear : core.
 
 Lemma valid_le_compat : forall k l p, valid k p -> (k <= l)%positive -> valid l p.
@@ -414,6 +417,7 @@ intros pl; induction pl; intros pr var; simpl.
     rewrite poly_add_compat, poly_mul_mon_compat, IHpl1, IHpl2; ring.
 Qed.
 
+#[local]
 Hint Extern 5 =>
 match goal with
 | [ |- (Pos.max ?x ?y <= ?z)%positive ] =>
@@ -426,8 +430,10 @@ match goal with
   apply Pos.max_case_strong; intros; lia
 | _ => lia
 end : core.
+#[local]
 Hint Resolve Pos.le_max_r Pos.le_max_l : core.
 
+#[local]
 Hint Constructors valid linear : core.
 
 (* Compatibility of validity w.r.t algebraic operations *)
diff --git a/theories/btauto/Reflect.v b/theories/btauto/Reflect.v
index 867fe69550..a653b94d1c 100644
--- a/theories/btauto/Reflect.v
+++ b/theories/btauto/Reflect.v
@@ -77,9 +77,11 @@ intros var f; induction f; simpl poly_of_formula; simpl formula_eval; auto.
   end.
 Qed.
 
+#[local]
 Hint Extern 5 => change 0 with (min 0 0) : core.
 Local Hint Resolve poly_add_valid_compat poly_mul_valid_compat : core.
 Local Hint Constructors valid : core.
+#[local]
 Hint Extern 5 => lia : core.
 
 (* Compatibility with validity *)
diff --git a/theories/micromega/Tauto.v b/theories/micromega/Tauto.v
index 99af214396..ce12b02359 100644
--- a/theories/micromega/Tauto.v
+++ b/theories/micromega/Tauto.v
@@ -1562,6 +1562,7 @@ Section S.
     auto.
   Qed.
 
+  #[local]
   Hint Resolve no_middle_eval_tt : tauto.
 
   Lemma or_clause_correct : forall cl cl' env,  eval_opt_clause env (or_clause cl cl') <-> eval_clause env cl \/ eval_clause env cl'.
@@ -1702,6 +1703,7 @@ Section S.
     intros k; destruct k ; simpl; auto.
   Qed.
 
+  #[local]
   Hint Resolve hold_eTT : tauto.
 
   Lemma hold_eFF : forall k,
@@ -1710,6 +1712,7 @@ Section S.
     intros k; destruct k ; simpl;auto.
   Qed.
 
+  #[local]
   Hint Resolve hold_eFF : tauto.
 
   Lemma hold_eAND : forall k r1 r2,
diff --git a/theories/micromega/ZArith_hints.v b/theories/micromega/ZArith_hints.v
index a6d3d92a99..3545e8b218 100644
--- a/theories/micromega/ZArith_hints.v
+++ b/theories/micromega/ZArith_hints.v
@@ -10,34 +10,56 @@
 Require Import Lia.
 Import ZArith_base.
 
+#[global]
 Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l
   Z.add_0_r Z.mul_1_l Z.add_opp_diag_l Z.add_opp_diag_r Z.mul_add_distr_r
   Z.mul_add_distr_l: zarith.
 
 Require Export Zhints.
 
+#[global]
 Hint Extern 10 (_ = _ :>nat) => abstract lia: zarith.
+#[global]
 Hint Extern 10 (_ <= _) => abstract lia: zarith.
+#[global]
 Hint Extern 10 (_ < _) => abstract lia: zarith.
+#[global]
 Hint Extern 10 (_ >= _) => abstract lia: zarith.
+#[global]
 Hint Extern 10 (_ > _) => abstract lia: zarith.
 
+#[global]
 Hint Extern 10 (_ <> _ :>nat) => abstract lia: zarith.
+#[global]
 Hint Extern 10 (~ _ <= _) => abstract lia: zarith.
+#[global]
 Hint Extern 10 (~ _ < _) => abstract lia: zarith.
+#[global]
 Hint Extern 10 (~ _ >= _) => abstract lia: zarith.
+#[global]
 Hint Extern 10 (~ _ > _) => abstract lia: zarith.
 
+#[global]
 Hint Extern 10 (_ = _ :>Z) => abstract lia: zarith.
+#[global]
 Hint Extern 10 (_ <= _)%Z => abstract lia: zarith.
+#[global]
 Hint Extern 10 (_ < _)%Z => abstract lia: zarith.
+#[global]
 Hint Extern 10 (_ >= _)%Z => abstract lia: zarith.
+#[global]
 Hint Extern 10 (_ > _)%Z => abstract lia: zarith.
 
+#[global]
 Hint Extern 10 (_ <> _ :>Z) => abstract lia: zarith.
+#[global]
 Hint Extern 10 (~ (_ <= _)%Z) => abstract lia: zarith.
+#[global]
 Hint Extern 10 (~ (_ < _)%Z) => abstract lia: zarith.
+#[global]
 Hint Extern 10 (~ (_ >= _)%Z) => abstract lia: zarith.
+#[global]
 Hint Extern 10 (~ (_ > _)%Z) => abstract lia: zarith.
 
+#[global]
 Hint Extern 10 False => abstract lia: zarith.
diff --git a/theories/nsatz/Nsatz.v b/theories/nsatz/Nsatz.v
index b684775bb4..21f0f30140 100644
--- a/theories/nsatz/Nsatz.v
+++ b/theories/nsatz/Nsatz.v
@@ -60,6 +60,7 @@ exact Rplus_opp_r.
 Defined.
 
 Class can_compute_Z (z : Z) := dummy_can_compute_Z : True.
+#[global]
 Hint Extern 0 (can_compute_Z ?v) =>
   match isZcst v with true => exact I end : typeclass_instances.
 Instance reify_IZR z lvar {_ : can_compute_Z z} : reify (PEc z) lvar (IZR z).
diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v
index e8a036bbb0..b205965ed1 100644
--- a/theories/ssr/ssrbool.v
+++ b/theories/ssr/ssrbool.v
@@ -487,6 +487,7 @@ Ltac prop_congr := apply: prop_congr.
 Lemma is_true_true : true.               Proof. by []. Qed.
 Lemma not_false_is_true : ~ false.       Proof. by []. Qed.
 Lemma is_true_locked_true : locked true. Proof. by unlock. Qed.
+#[global]
 Hint Resolve is_true_true not_false_is_true is_true_locked_true : core.
 
 (**  Shorter names.  **)
diff --git a/theories/ssr/ssreflect.v b/theories/ssr/ssreflect.v
index 175cae8415..d0508bef2e 100644
--- a/theories/ssr/ssreflect.v
+++ b/theories/ssr/ssreflect.v
@@ -543,8 +543,10 @@ Proof. by move=> /(_ P); apply. Qed.
 
 Require Export ssrunder.
 
+#[global]
 Hint Extern 0 (@Under_rel.Over_rel _ _ _ _) =>
   solve [ apply: Under_rel.over_rel_done ] : core.
+#[global]
 Hint Resolve Under_rel.over_rel_done : core.
 
 Register Under_rel.Under_rel as plugins.ssreflect.Under_rel.
diff --git a/theories/ssr/ssrfun.v b/theories/ssr/ssrfun.v
index 053e86dc34..e1442e1da2 100644
--- a/theories/ssr/ssrfun.v
+++ b/theories/ssr/ssrfun.v
@@ -450,6 +450,7 @@ End ExtensionalEquality.
 Typeclasses Opaque eqfun.
 Typeclasses Opaque eqrel.
 
+#[global]
 Hint Resolve frefl rrefl : core.
 
 Notation "f1 =1 f2" := (eqfun f1 f2) : fun_scope.