Explicitly annotate all hint declarations of the standard library.

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

4 files changed, 6 insertions, 0 deletions

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.