Support locality attributes for Hint Rewrite (including export)

We deprecate unspecified locality as was done for Hint.

Close #13724

19 files changed, 40 insertions, 40 deletions

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.