Merge PR #13725: Support locality attributes for Hint Rewrite (including export)

Ack-by: Zimmi48
Ack-by: gares
Reviewed-by: ppedrot

30 files changed, 122 insertions, 90 deletions

diff --git a/dev/ci/user-overlays/13725-SkySkimmer-hint-rw-local.sh b/dev/ci/user-overlays/13725-SkySkimmer-hint-rw-local.sh
new file mode 100644
index 0000000000..69bd038b78
--- /dev/null
+++ b/dev/ci/user-overlays/13725-SkySkimmer-hint-rw-local.sh
@@ -0,0 +1 @@
+overlay equations https://github.com/SkySkimmer/Coq-Equations hint-rw-local 13725
diff --git a/doc/changelog/07-vernac-commands-and-options/13725-hint-rw-local.rst b/doc/changelog/07-vernac-commands-and-options/13725-hint-rw-local.rst
new file mode 100644
index 0000000000..653e9cd0cd
--- /dev/null
+++ b/doc/changelog/07-vernac-commands-and-options/13725-hint-rw-local.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+  :cmd:`Hint Rewrite` now supports locality attributes (including :attr:`export`) like other :ref:`Hint <creating_hints>` commands
+  (`#13725 <https://github.com/coq/coq/pull/13725>`_,
+  fixes `#13724 <https://github.com/coq/coq/issues/13724>`_,
+  by Gaëtan Gilbert).
diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
index b63ae32311..2046788ef3 100644
--- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst
+++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
@@ -339,7 +339,7 @@ the optional tactic of the ``Hint Rewrite`` command.
 
    .. coqtop:: in
 
-      Hint Rewrite Ack0 Ack1 Ack2 : base0.
+      Global Hint Rewrite Ack0 Ack1 Ack2 : base0.
 
    .. coqtop:: all
 
@@ -367,7 +367,7 @@ the optional tactic of the ``Hint Rewrite`` command.
 
    .. coqtop:: in
 
-      Hint Rewrite g0 g1 g2 using lia : base1.
+      Global Hint Rewrite g0 g1 g2 using lia : base1.
 
    .. coqtop:: in
 
diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst
index d7228a3907..d2e88261ae 100644
--- a/doc/sphinx/proofs/automatic-tactics/auto.rst
+++ b/doc/sphinx/proofs/automatic-tactics/auto.rst
@@ -273,12 +273,15 @@ Creating Hints
      :cmd:`Import` or :cmd:`Require` the current module.
 
    + :attr:`export` hints are visible from other modules when they :cmd:`Import` the current
-     module, but not when they only :cmd:`Require` it. This attribute is supported by
-     all `Hint` commands except for :cmd:`Hint Rewrite`.
+     module, but not when they only :cmd:`Require` it.
 
    + :attr:`global` hints are visible from other modules when they :cmd:`Import` or
      :cmd:`Require` the current module.
 
+   .. versionadded:: 8.14
+
+      The :cmd:`Hint Rewrite` now supports locality attributes like other `Hint` commands.
+
    .. deprecated:: 8.13
 
      The default value for hint locality will change in a future
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 90c366ed63..d9da47134d 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -299,7 +299,7 @@ TACTIC EXTEND rewrite_star
 
 {
 
-let add_rewrite_hint ~poly bases ort t lcsr =
+let add_rewrite_hint ~locality ~poly bases ort t lcsr =
   let env = Global.env() in
   let sigma = Evd.from_env env in
   let f ce =
@@ -315,7 +315,7 @@ let add_rewrite_hint ~poly bases ort t lcsr =
     in
       CAst.make ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in
   let eqs = List.map f lcsr in
-  let add_hints base = add_rew_rules base eqs in
+  let add_hints base = add_rew_rules ~locality base eqs in
   List.iter add_hints bases
 
 let classify_hint _ = VtSideff ([], VtLater)
@@ -323,15 +323,15 @@ let classify_hint _ = VtSideff ([], VtLater)
 }
 
 VERNAC COMMAND EXTEND HintRewrite CLASSIFIED BY { classify_hint }
-| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] ->
-  { add_rewrite_hint ~poly:polymorphic bl o None l }
-| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
+| #[ polymorphic; locality = option_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] ->
+  { add_rewrite_hint ~locality ~poly:polymorphic bl o None l }
+| #[ polymorphic; locality = option_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
     ":" preident_list(bl) ] ->
-  { add_rewrite_hint ~poly:polymorphic bl o (Some t) l }
-| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] ->
-  { add_rewrite_hint ~poly:polymorphic ["core"] o None l }
-| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] ->
-  { add_rewrite_hint ~poly:polymorphic ["core"] o (Some t) l }
+  { add_rewrite_hint ~locality ~poly:polymorphic bl o (Some t) l }
+| #[ polymorphic; locality = option_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] ->
+  { add_rewrite_hint ~locality ~poly:polymorphic ["core"] o None l }
+| #[ polymorphic; locality = option_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] ->
+  { add_rewrite_hint ~locality ~poly:polymorphic ["core"] o (Some t) l }
 END
 
 (**********************************************************************)
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index cc56de066d..1d876537ef 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -206,9 +206,15 @@ let subst_hintrewrite (subst,(rbase,list as node)) =
       (rbase,list')
 
 (* Declaration of the Hint Rewrite library object *)
-let inHintRewrite : string * HintDN.t -> Libobject.obj =
+let inGlobalHintRewrite : string * HintDN.t -> Libobject.obj =
   let open Libobject in
-  declare_object @@ superglobal_object_nodischarge "HINT_REWRITE"
+  declare_object @@ superglobal_object_nodischarge "HINT_REWRITE_GLOBAL"
+    ~cache:cache_hintrewrite
+    ~subst:(Some subst_hintrewrite)
+
+let inExportHintRewrite : string * HintDN.t -> Libobject.obj =
+  let open Libobject in
+  declare_object @@ global_object_nodischarge "HINT_REWRITE_EXPORT"
     ~cache:cache_hintrewrite
     ~subst:(Some subst_hintrewrite)
 
@@ -250,7 +256,8 @@ let find_applied_relation ?loc env sigma c left2right =
                        spc () ++ str"of this term does not end with an applied relation.")
 
 (* To add rewriting rules to a base *)
-let add_rew_rules base lrul =
+let add_rew_rules ~locality base lrul =
+  let () = Hints.check_hint_locality locality in
   let counter = ref 0 in
   let env = Global.env () in
   let sigma = Evd.from_env env in
@@ -267,5 +274,9 @@ let add_rew_rules base lrul =
                     rew_tac = Option.map intern t}
         in incr counter;
           HintDN.add pat (!counter, rul) dn) HintDN.empty lrul
-  in Lib.add_anonymous_leaf (inHintRewrite (base,lrul))
-
+  in
+  let open Goptions in
+  match locality with
+  | OptLocal -> cache_hintrewrite ((),(base,lrul))
+  | OptDefault | OptGlobal -> Lib.add_anonymous_leaf (inGlobalHintRewrite (base,lrul))
+  | OptExport -> Lib.add_anonymous_leaf (inExportHintRewrite (base,lrul))
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index 974aef8e8f..dec6cc5ef4 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -17,7 +17,7 @@ open Equality
 type raw_rew_rule = (constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option) CAst.t
 
 (** To add rewriting rules to a base *)
-val add_rew_rules : string -> raw_rew_rule list -> unit
+val add_rew_rules : locality:Goptions.option_locality -> string -> raw_rew_rule list -> unit
 
 (** The AutoRewrite tactic.
    The optional conditions tell rewrite how to handle matching and side-condition solving.
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 0cc8becd8f..058602acfd 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1187,6 +1187,28 @@ let create_hint_db l n st b =
   let hint = make_hint ~local:l n (CreateDB (b, st)) in
   Lib.add_anonymous_leaf (inAutoHint hint)
 
+let warn_deprecated_hint_without_locality =
+  CWarnings.create ~name:"deprecated-hint-without-locality" ~category:"deprecated"
+    (fun () -> strbrk "The default value for hint locality is currently \
+    \"local\" in a section and \"global\" otherwise, but is scheduled to change \
+    in a future release. For the time being, adding hints outside of sections \
+    without specifying an explicit locality is therefore deprecated. It is \
+    recommended to use \"export\" whenever possible.")
+
+let check_hint_locality = let open Goptions in function
+| OptGlobal ->
+  if Global.sections_are_opened () then
+  CErrors.user_err Pp.(str
+    "This command does not support the global attribute in sections.");
+| OptExport ->
+  if Global.sections_are_opened () then
+  CErrors.user_err Pp.(str
+    "This command does not support the export attribute in sections.");
+| OptDefault ->
+  if not @@ Global.sections_are_opened () then
+    warn_deprecated_hint_without_locality ()
+| OptLocal -> ()
+
 let interp_locality = function
 | Goptions.OptDefault | Goptions.OptGlobal -> false, true
 | Goptions.OptExport -> false, false
diff --git a/tactics/hints.mli b/tactics/hints.mli
index f5947bb946..381c7a1951 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -182,6 +182,8 @@ val searchtable_map : hint_db_name -> hint_db
 
 val searchtable_add : (hint_db_name * hint_db) -> unit
 
+val check_hint_locality : Goptions.option_locality -> unit
+
 (** [create_hint_db local name st use_dn].
    [st] is a transparency state for unification using this db
    [use_dn] switches the use of the discrimination net for all hints
diff --git a/test-suite/success/autorewrite.v b/test-suite/success/autorewrite.v
index 71d333d439..0ac62fcdc9 100644
--- a/test-suite/success/autorewrite.v
+++ b/test-suite/success/autorewrite.v
@@ -4,25 +4,35 @@ Axiom Ack0 : forall m : nat, Ack 0 m = S m.
 Axiom Ack1 : forall n : nat, Ack (S n) 0 = Ack n 1.
 Axiom Ack2 : forall n m : nat, Ack (S n) (S m) = Ack n (Ack (S n) m).
 
-Hint Rewrite Ack0 Ack1 Ack2 : base0.
+Module M.
+  #[export] Hint Rewrite Ack0 Ack1 Ack2 : base0.
 
-Lemma ResAck0 : (Ack 2 2 = 7 -> False) -> False.
+  Lemma ResAck0 : (Ack 2 2 = 7 -> False) -> False.
+  Proof.
+    intros.
+    autorewrite with base0 in H using try (apply H; reflexivity).
+  Qed.
+End M.
+
+Lemma ResAck1 : forall H:(Ack 2 2 = 7 -> False), True -> False.
 Proof.
   intros.
-  autorewrite with base0 in H using try (apply H; reflexivity).
-Qed.
+  Fail autorewrite with base0 in *.
+Abort.
+
+Import M.
 
 Lemma ResAck1 : forall H:(Ack 2 2 = 7 -> False), True -> False.
 Proof.
   intros.
   autorewrite with base0 in *.
-    apply H;reflexivity.
+ apply H;reflexivity.
 Qed.
 
 (* Check autorewrite does not solve existing evars *)
 (* See discussion started by A. Chargueraud in Oct 2010 on coqdev *)
 
-Hint Rewrite <- plus_n_O : base1.
+Global Hint Rewrite <- plus_n_O : base1.
 Goal forall y, exists x, y+x = y.
 eexists. autorewrite with base1.
 Fail reflexivity.
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index d597c0404a..5fe2cade3b 100644
--- a/theories/FSets/FSetDecide.v
+++ b/theories/FSets/FSetDecide.v
@@ -489,7 +489,7 @@ the above form:
         variables.  We are going to use them with [autorewrite].
         *)
 
-    Hint Rewrite
+    Global Hint Rewrite
       F.empty_iff F.singleton_iff F.add_iff F.remove_iff
       F.union_iff F.inter_iff F.diff_iff
     : set_simpl.
@@ -499,7 +499,7 @@ the above form:
      now split.
     Qed.
 
-    Hint Rewrite eq_refl_iff : set_eq_simpl.
+    Global Hint Rewrite eq_refl_iff : set_eq_simpl.
 
     (** ** Decidability of FSet Propositions *)
 
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 115c7cb365..d6277b3bb5 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -3327,7 +3327,7 @@ Ltac invlist f :=
 (** * Exporting hints and tactics *)
 
 
-Hint Rewrite
+Global Hint Rewrite
   rev_involutive (* rev (rev l) = l *)
   rev_unit (* rev (l ++ a :: nil) = a :: rev l *)
   map_nth (* nth n (map f l) (f d) = f (nth n l d) *)
diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v
index aa0c419f0e..579e5e9630 100644
--- a/theories/MSets/MSetDecide.v
+++ b/theories/MSets/MSetDecide.v
@@ -489,7 +489,7 @@ the above form:
         variables.  We are going to use them with [autorewrite].
         *)
 
-    Hint Rewrite
+    Global Hint Rewrite
       F.empty_iff F.singleton_iff F.add_iff F.remove_iff
       F.union_iff F.inter_iff F.diff_iff
     : set_simpl.
@@ -499,7 +499,7 @@ the above form:
      now split.
     Qed.
 
-    Hint Rewrite eq_refl_iff : set_eq_simpl.
+    Global Hint Rewrite eq_refl_iff : set_eq_simpl.
 
     (** ** Decidability of MSet Propositions *)
 
diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v
index f80929e320..2d210e24a6 100644
--- a/theories/MSets/MSetRBT.v
+++ b/theories/MSets/MSetRBT.v
@@ -651,7 +651,7 @@ Proof.
  destruct (rbal'_match l x r); ok.
 Qed.
 
-Hint Rewrite In_node_iff In_leaf_iff
+Global Hint Rewrite In_node_iff In_leaf_iff
  makeRed_spec makeBlack_spec lbal_spec rbal_spec rbal'_spec : rb.
 
 Ltac descolor := destruct_all Color.t.
@@ -670,7 +670,7 @@ Proof.
  - descolor; autorew; rewrite IHl; intuition_in.
  - descolor; autorew; rewrite IHr; intuition_in.
 Qed.
-Hint Rewrite ins_spec : rb.
+Global Hint Rewrite ins_spec : rb.
 
 Instance ins_ok s x `{Ok s} : Ok (ins x s).
 Proof.
@@ -685,7 +685,7 @@ Proof.
  unfold add. now autorew.
 Qed.
 
-Hint Rewrite add_spec' : rb.
+Global Hint Rewrite add_spec' : rb.
 
 Lemma add_spec s x y `{Ok s} :
  InT y (add x s) <-> X.eq y x \/ InT y s.
@@ -754,7 +754,7 @@ Proof.
    * ok. apply lbal_ok; ok.
 Qed.
 
-Hint Rewrite lbalS_spec rbalS_spec : rb.
+Global Hint Rewrite lbalS_spec rbalS_spec : rb.
 
 (** ** Append for deletion *)
 
@@ -807,7 +807,7 @@ Proof.
     [intros a y b | intros t Ht]; autorew; tauto.
 Qed.
 
-Hint Rewrite append_spec : rb.
+Global Hint Rewrite append_spec : rb.
 
 Lemma append_ok : forall x l r `{Ok l, Ok r},
  lt_tree x l -> gt_tree x r -> Ok (append l r).
@@ -861,7 +861,7 @@ induct s x.
   rewrite ?IHr by trivial; intuition_in; order.
 Qed.
 
-Hint Rewrite del_spec : rb.
+Global Hint Rewrite del_spec : rb.
 
 Instance del_ok s x `{Ok s} : Ok (del x s).
 Proof.
@@ -882,7 +882,7 @@ Proof.
 unfold remove. now autorew.
 Qed.
 
-Hint Rewrite remove_spec : rb.
+Global Hint Rewrite remove_spec : rb.
 
 Instance remove_ok s x `{Ok s} : Ok (remove x s).
 Proof.
diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v
index 48df5fe884..420c17c9a4 100644
--- a/theories/NArith/Nnat.v
+++ b/theories/NArith/Nnat.v
@@ -127,7 +127,7 @@ Qed.
 
 End N2Nat.
 
-Hint Rewrite N2Nat.inj_double N2Nat.inj_succ_double
+Global Hint Rewrite N2Nat.inj_double N2Nat.inj_succ_double
  N2Nat.inj_succ N2Nat.inj_add N2Nat.inj_mul N2Nat.inj_sub
  N2Nat.inj_pred N2Nat.inj_div2 N2Nat.inj_max N2Nat.inj_min
  N2Nat.id
@@ -147,7 +147,7 @@ Proof.
  induction n; simpl; trivial. apply SuccNat2Pos.id_succ.
 Qed.
 
-Hint Rewrite id : Nnat.
+Global Hint Rewrite id : Nnat.
 Ltac nat2N := apply N2Nat.inj; now autorewrite with Nnat.
 
 (** [N.of_nat] is hence injective *)
@@ -206,7 +206,7 @@ Proof. now rewrite N2Nat.inj_iter, !id. Qed.
 
 End Nat2N.
 
-Hint Rewrite Nat2N.id : Nnat.
+Global Hint Rewrite Nat2N.id : Nnat.
 
 (** Compatibility notations *)
 
diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index e3e8f532b3..374af6de63 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -348,7 +348,7 @@ Local Notation "- x" := (ZnZ.opp x).
 Local Infix "*" := ZnZ.mul.
 Local Notation wB := (base ZnZ.digits).
 
-Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_add ZnZ.spec_mul
+Global Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_add ZnZ.spec_mul
  ZnZ.spec_opp ZnZ.spec_sub
  : cyclic.
 
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index 7c5b43096a..f74a78e876 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -51,7 +51,7 @@ Local Infix "+" := add.
 Local Infix "-" := sub.
 Local Infix "*" := mul.
 
-Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_succ ZnZ.spec_pred
+Global Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_succ ZnZ.spec_pred
  ZnZ.spec_add ZnZ.spec_mul ZnZ.spec_sub : cyclic.
 Ltac zify :=
  unfold eq, zero, one, two, succ, pred, add, sub, mul in *;
diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v
index 0c097b6773..9d9244eefb 100644
--- a/theories/Numbers/Integer/Abstract/ZAdd.v
+++ b/theories/Numbers/Integer/Abstract/ZAdd.v
@@ -18,7 +18,7 @@ Include ZBaseProp Z.
 (** Theorems that are either not valid on N or have different proofs
     on N and Z *)
 
-Hint Rewrite opp_0 : nz.
+Global Hint Rewrite opp_0 : nz.
 
 Theorem add_pred_l n m : P n + m == P (n + m).
 Proof.
diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v
index 4d2361689d..832931e5ef 100644
--- a/theories/Numbers/Integer/Abstract/ZBits.v
+++ b/theories/Numbers/Integer/Abstract/ZBits.v
@@ -26,7 +26,7 @@ Include BoolEqualityFacts A.
 
 Ltac order_nz := try apply pow_nonzero; order'.
 Ltac order_pos' := try apply abs_nonneg; order_pos.
-Hint Rewrite div_0_l mod_0_l div_1_r mod_1_r : nz.
+Global Hint Rewrite div_0_l mod_0_l div_1_r mod_1_r : nz.
 
 (** Some properties of power and division *)
 
@@ -566,7 +566,7 @@ Tactic Notation "bitwise" "as" simple_intropattern(m) simple_intropattern(Hm)
 
 Ltac bitwise := bitwise as ?m ?Hm.
 
-Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise.
+Global Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise.
 
 (** The streams of bits that correspond to a numbers are
   exactly the ones which are stationary after some point. *)
diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v
index 66cbba9e08..2ad8dfcedb 100644
--- a/theories/Numbers/NatInt/NZAdd.v
+++ b/theories/Numbers/NatInt/NZAdd.v
@@ -14,9 +14,9 @@ Require Import NZAxioms NZBase.
 
 Module Type NZAddProp (Import NZ : NZAxiomsSig')(Import NZBase : NZBaseProp NZ).
 
-Hint Rewrite
+Global Hint Rewrite
  pred_succ add_0_l add_succ_l mul_0_l mul_succ_l sub_0_r sub_succ_r : nz.
-Hint Rewrite one_succ two_succ : nz'.
+Global Hint Rewrite one_succ two_succ : nz'.
 Ltac nzsimpl := autorewrite with nz.
 Ltac nzsimpl' := autorewrite with nz nz'.
 
@@ -39,7 +39,7 @@ Proof.
 intros n m. now rewrite add_succ_r, add_succ_l.
 Qed.
 
-Hint Rewrite add_0_r add_succ_r : nz.
+Global Hint Rewrite add_0_r add_succ_r : nz.
 
 Theorem add_comm : forall n m, n + m == m + n.
 Proof.
@@ -58,7 +58,7 @@ Proof.
 intro n; now nzsimpl'.
 Qed.
 
-Hint Rewrite add_1_l add_1_r : nz.
+Global Hint Rewrite add_1_l add_1_r : nz.
 
 Theorem add_assoc : forall n m p, n + (m + p) == (n + m) + p.
 Proof.
@@ -104,6 +104,6 @@ Proof.
 intro n; now nzsimpl'.
 Qed.
 
-Hint Rewrite sub_1_r : nz.
+Global Hint Rewrite sub_1_r : nz.
 
 End NZAddProp.
diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v
index 3d6465191d..14728eaf40 100644
--- a/theories/Numbers/NatInt/NZMul.v
+++ b/theories/Numbers/NatInt/NZMul.v
@@ -28,7 +28,7 @@ Proof.
     now rewrite add_cancel_r.
 Qed.
 
-Hint Rewrite mul_0_r mul_succ_r : nz.
+Global Hint Rewrite mul_0_r mul_succ_r : nz.
 
 Theorem mul_comm : forall n m, n * m == m * n.
 Proof.
@@ -69,7 +69,7 @@ Proof.
 intro n. now nzsimpl'.
 Qed.
 
-Hint Rewrite mul_1_l mul_1_r : nz.
+Global Hint Rewrite mul_1_l mul_1_r : nz.
 
 Theorem mul_shuffle0 : forall n m p, n*m*p == n*p*m.
 Proof.
diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v
index 3b2a496229..00edcd641f 100644
--- a/theories/Numbers/NatInt/NZPow.v
+++ b/theories/Numbers/NatInt/NZPow.v
@@ -45,7 +45,7 @@ Module Type NZPowProp
  (Import B : NZPow' A)
  (Import C : NZMulOrderProp A).
 
-Hint Rewrite pow_0_r pow_succ_r : nz.
+Global Hint Rewrite pow_0_r pow_succ_r : nz.
 
 (** Power and basic constants *)
 
@@ -76,14 +76,14 @@ Proof.
   - now nzsimpl.
 Qed.
 
-Hint Rewrite pow_1_r pow_1_l : nz.
+Global Hint Rewrite pow_1_r pow_1_l : nz.
 
 Lemma pow_2_r : forall a, a^2 == a*a.
 Proof.
  intros. rewrite two_succ. nzsimpl; order'.
 Qed.
 
-Hint Rewrite pow_2_r : nz.
+Global Hint Rewrite pow_2_r : nz.
 
 (** Power and nullity *)
 
diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v
index 313b9adfd1..427a18d4ae 100644
--- a/theories/Numbers/Natural/Abstract/NBits.v
+++ b/theories/Numbers/Natural/Abstract/NBits.v
@@ -23,7 +23,7 @@ Module Type NBitsProp
 Include BoolEqualityFacts A.
 
 Ltac order_nz := try apply pow_nonzero; order'.
-Hint Rewrite div_0_l mod_0_l div_1_r mod_1_r : nz.
+Global Hint Rewrite div_0_l mod_0_l div_1_r mod_1_r : nz.
 
 (** Some properties of power and division *)
 
@@ -368,7 +368,7 @@ Proof.
  split. apply bits_inj. intros EQ; now rewrite EQ.
 Qed.
 
-Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise.
+Global Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise.
 
 Tactic Notation "bitwise" "as" simple_intropattern(m)
   := apply bits_inj; intros m; autorewrite with bitwise.
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index e97f2dc748..7d50bdacad 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -876,7 +876,7 @@ Lemma compare_xO_xI p q :
  (p~0 ?= q~1) = switch_Eq Lt (p ?= q).
 Proof. exact (compare_cont_spec p q Lt). Qed.
 
-Hint Rewrite compare_xO_xO compare_xI_xI compare_xI_xO compare_xO_xI : compare.
+Global Hint Rewrite compare_xO_xO compare_xI_xI compare_xI_xO compare_xO_xI : compare.
 
 Ltac simpl_compare := autorewrite with compare.
 Ltac simpl_compare_in H := autorewrite with compare in H.
diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v
index 8813131d7b..18e55aefc6 100644
--- a/theories/Program/Combinators.v
+++ b/theories/Program/Combinators.v
@@ -40,8 +40,8 @@ Proof.
   reflexivity.
 Qed.
 
-Hint Rewrite @compose_id_left @compose_id_right : core.
-Hint Rewrite <- @compose_assoc : core.
+Global Hint Rewrite @compose_id_left @compose_id_right : core.
+Global Hint Rewrite <- @compose_assoc : core.
 
 (** [flip] is involutive. *)
 
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 25af2d5ffb..090322054e 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -162,7 +162,7 @@ Ltac pi_eq_proofs := repeat pi_eq_proof.
 Ltac clear_eq_proofs :=
   abstract_eq_proofs ; pi_eq_proofs.
 
-Hint Rewrite <- eq_rect_eq : refl_id.
+Global Hint Rewrite <- eq_rect_eq : refl_id.
 
 (** The [refl_id] database should be populated with lemmas of the form
    [coerce_* t eq_refl = t]. *)
@@ -178,7 +178,7 @@ Lemma inj_pairT2_refl A (x : A) (P : A -> Type) (p : P x) :
   Eqdep.EqdepTheory.inj_pairT2 A P x p p eq_refl = eq_refl.
 Proof. apply UIP_refl. Qed.
 
-Hint Rewrite @JMeq_eq_refl @UIP_refl_refl @inj_pairT2_refl : refl_id.
+Global Hint Rewrite @JMeq_eq_refl @UIP_refl_refl @inj_pairT2_refl : refl_id.
 
 Ltac rewrite_refl_id := autorewrite with refl_id.
 
diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v
index 5a23a20811..620ed6b5b7 100644
--- a/theories/QArith/Qreals.v
+++ b/theories/QArith/Qreals.v
@@ -180,4 +180,4 @@ intros; rewrite Q2R_mult.
 rewrite Q2R_inv; auto.
 Qed.
 
-Hint Rewrite Q2R_plus Q2R_mult Q2R_opp Q2R_minus Q2R_inv Q2R_div : q2r_simpl.
+Global Hint Rewrite Q2R_plus Q2R_mult Q2R_opp Q2R_minus Q2R_inv Q2R_div : q2r_simpl.
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
index 4ac54d280a..c3e67b9d5a 100644
--- a/theories/Structures/OrdersFacts.v
+++ b/theories/Structures/OrdersFacts.v
@@ -53,7 +53,7 @@ Module Type CompareFacts (Import O:DecStrOrder').
  rewrite compare_gt_iff; intuition.
  Qed.
 
- Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order.
+ Global Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order.
 
  Instance compare_compat : Proper (eq==>eq==>Logic.eq) compare.
  Proof.
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index abf7f681b0..c709149109 100644
--- a/theories/ZArith/Int.v
+++ b/theories/ZArith/Int.v
@@ -146,7 +146,7 @@ Module MoreInt (Import I:Int).
   (** A magic (but costly) tactic that goes from [int] back to the [Z]
       friendly world ... *)
 
-  Hint Rewrite ->
+  Global Hint Rewrite ->
     i2z_0 i2z_1 i2z_2 i2z_3 i2z_add i2z_opp i2z_sub i2z_mul i2z_max
     i2z_eqb i2z_ltb i2z_leb : i2z.
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4f3fc46c12..1c774a35bf 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1401,31 +1401,9 @@ let warn_implicit_core_hint_db =
          (fun () -> strbrk "Adding and removing hints in the core database implicitly is deprecated. "
              ++ strbrk"Please specify a hint database.")
 
-let warn_deprecated_hint_without_locality =
-  CWarnings.create ~name:"deprecated-hint-without-locality" ~category:"deprecated"
-    (fun () -> strbrk "The default value for hint locality is currently \
-    \"local\" in a section and \"global\" otherwise, but is scheduled to change \
-    in a future release. For the time being, adding hints outside of sections \
-    without specifying an explicit locality is therefore deprecated. It is \
-    recommended to use \"export\" whenever possible.")
-
-let check_hint_locality = function
-| OptGlobal ->
-  if Global.sections_are_opened () then
-  CErrors.user_err Pp.(str
-    "This command does not support the global attribute in sections.");
-| OptExport ->
-  if Global.sections_are_opened () then
-  CErrors.user_err Pp.(str
-    "This command does not support the export attribute in sections.");
-| OptDefault ->
-  if not @@ Global.sections_are_opened () then
-    warn_deprecated_hint_without_locality ()
-| OptLocal -> ()
-
 let vernac_remove_hints ~atts dbnames ids =
   let locality = Attributes.(parse option_locality atts) in
-  let () = check_hint_locality locality in
+  let () = Hints.check_hint_locality locality in
   let dbnames =
     if List.is_empty dbnames then
       (warn_implicit_core_hint_db (); ["core"])
@@ -1440,7 +1418,7 @@ let vernac_hints ~atts dbnames h =
     else dbnames
   in
   let locality, poly = Attributes.(parse Notations.(option_locality ++ polymorphic) atts) in
-  let () = check_hint_locality locality in
+  let () = Hints.check_hint_locality locality in
   Hints.add_hints ~locality dbnames (ComHints.interp_hints ~poly h)
 
 let vernac_syntactic_definition ~atts lid x only_parsing =