Support locality attributes for Hint Rewrite (including export)

We deprecate unspecified locality as was done for Hint.

Close #13724

8 files changed, 17 insertions, 17 deletions

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.