Support locality attributes for Hint Rewrite (including export)

We deprecate unspecified locality as was done for Hint.

Close #13724

2 files changed, 9 insertions, 9 deletions

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.