Explicitly annotate all hint declarations of the standard library.

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

11 files changed, 26 insertions, 0 deletions

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 52998c8b95..47137414dc 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1754,6 +1754,7 @@ Proof. congruence. Qed.
 Lemma Zpos_eq_iff : forall p q, p = q <-> Z.pos p = Z.pos q.
 Proof (fun p q => iff_sym (Pos2Z.inj_iff p q)).
 
+#[global]
 Hint Immediate Zsucc_pred: zarith.
 
 (* Not kept :
diff --git a/theories/ZArith/ZArith_base.v b/theories/ZArith/ZArith_base.v
index 26cd3e1e4d..cae918b4b6 100644
--- a/theories/ZArith/ZArith_base.v
+++ b/theories/ZArith/ZArith_base.v
@@ -30,6 +30,7 @@ Require Export Zbool.
 Require Export Zmisc.
 Require Export Wf_Z.
 
+#[global]
 Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l
   Z.add_0_r Z.mul_1_l Z.add_opp_diag_l Z.add_opp_diag_r Z.mul_add_distr_l
   Z.mul_add_distr_r: zarith.
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 2039dc0bee..13adda412d 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -75,6 +75,7 @@ Proof.
     + apply Pos2Z.neg_is_nonpos.
 Qed.
 
+#[global]
 Hint Unfold Remainder : core.
 
 (** Now comes the fully general result about Euclidean division. *)
@@ -203,6 +204,7 @@ Proof. intros a. zero_or_not a. apply Z.mod_1_r. Qed.
 Lemma Zdiv_1_r: forall a, a/1 = a.
 Proof. intros a. zero_or_not a. apply Z.div_1_r. Qed.
 
+#[global]
 Hint Resolve Zmod_0_l Zmod_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_1_r
  : zarith.
 
diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v
index 0448bcf41b..d3a9d7baac 100644
--- a/theories/ZArith/Zeven.v
+++ b/theories/ZArith/Zeven.v
@@ -130,6 +130,7 @@ Proof.
  boolify_even_odd. now rewrite Z.odd_pred.
 Qed.
 
+#[global]
 Hint Unfold Zeven Zodd: zarith.
 
 Notation Zeven_bool_succ := Z.even_succ (only parsing).
diff --git a/theories/ZArith/Zhints.v b/theories/ZArith/Zhints.v
index 95266186eb..80073bdbdf 100644
--- a/theories/ZArith/Zhints.v
+++ b/theories/ZArith/Zhints.v
@@ -40,6 +40,7 @@ Require Import Wf_Z.
 
 (** No subgoal or smaller subgoals                                     *)
 
+#[global]
 Hint Resolve
   (** ** Reversible simplification lemmas (no loss of information)      *)
   (** Should clearly be declared as hints                               *)
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index cad9454906..861c204ab8 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -65,8 +65,11 @@ Proof. apply Z.divide_abs_l. Qed.
 Theorem Zdivide_Zabs_inv_l a b : (a | b) -> (Z.abs a | b).
 Proof. apply Z.divide_abs_l. Qed.
 
+#[global]
 Hint Resolve Z.divide_refl Z.divide_1_l Z.divide_0_r: zarith.
+#[global]
 Hint Resolve Z.mul_divide_mono_l Z.mul_divide_mono_r: zarith.
+#[global]
 Hint Resolve Z.divide_add_r Zdivide_opp_r Zdivide_opp_r_rev Zdivide_opp_l
   Zdivide_opp_l_rev Z.divide_sub_r Z.divide_mul_l Z.divide_mul_r
   Z.divide_factor_l Z.divide_factor_r: zarith.
@@ -236,6 +239,7 @@ Proof.
   intros; apply Zis_gcd_opp; apply Zis_gcd_0; auto.
 Qed.
 
+#[global]
 Hint Resolve Zis_gcd_sym Zis_gcd_0 Zis_gcd_minus Zis_gcd_opp: zarith.
 
 Theorem Zis_gcd_unique: forall a b c d : Z,
@@ -646,6 +650,7 @@ Proof.
   - absurd (p | a); intuition.
 Qed.
 
+#[global]
 Hint Resolve prime_rel_prime: zarith.
 
 (** As a consequence, a prime number is relatively prime with smaller numbers *)
@@ -866,6 +871,7 @@ Notation Zgcd_Zabs := Z.gcd_abs_l (only parsing).
 Notation Zgcd_0 := Z.gcd_0_r (only parsing).
 Notation Zgcd_1 := Z.gcd_1_r (only parsing).
 
+#[global]
 Hint Resolve Z.gcd_0_r Z.gcd_1_r : zarith.
 
 Theorem Zgcd_1_rel_prime : forall a b,
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 949a01860f..4c533ac458 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -132,6 +132,7 @@ Register not_Zne as plugins.omega.not_Zne.
 
 Notation Zeq_le := Z.eq_le_incl (only parsing).
 
+#[global]
 Hint Resolve Z.le_refl: zarith.
 
 (** Antisymmetry *)
@@ -196,6 +197,7 @@ Proof.
   Z.swap_greater. Z.order.
 Qed.
 
+#[global]
 Hint Resolve Z.le_trans: zarith.
 
 (** * Compatibility of order and operations on Z *)
@@ -219,6 +221,7 @@ Proof.
   Z.swap_greater. apply Z.succ_lt_mono.
 Qed.
 
+#[global]
 Hint Resolve Zsucc_le_compat: zarith.
 
 (** Simplification of successor wrt to order *)
@@ -302,7 +305,9 @@ Proof.
   intros. now apply Z.lt_le_incl, Z.le_succ_l.
 Qed.
 
+#[global]
 Hint Resolve Z.le_succ_diag_r: zarith.
+#[global]
 Hint Resolve Z.le_le_succ_r: zarith.
 
 (** Relating order wrt successor and order wrt predecessor *)
@@ -357,6 +362,7 @@ Proof.
   intros n; induction n; simpl; intros. apply Z.le_refl. easy.
 Qed.
 
+#[global]
 Hint Immediate Z.eq_le_incl: zarith.
 
 (** Derived lemma *)
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v
index c36ddad823..b69af424b1 100644
--- a/theories/ZArith/Zpow_facts.v
+++ b/theories/ZArith/Zpow_facts.v
@@ -57,6 +57,7 @@ Proof. apply Z.pow_gt_1. Qed.
 Theorem Zmult_power p q r : 0 <= r -> (p*q)^r = p^r * q^r.
 Proof. intros. apply Z.pow_mul_l. Qed.
 
+#[global]
 Hint Resolve Z.pow_nonneg Z.pow_pos_nonneg : zarith.
 
 Theorem Zpower_le_monotone3 a b c :
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index ae12295ca4..6f464d89bb 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -79,7 +79,9 @@ Proof.
  now apply (Z.pow_add_r z (Zpos n) (Zpos m)).
 Qed.
 
+#[global]
 Hint Immediate Zpower_nat_is_exp Zpower_pos_is_exp : zarith.
+#[global]
 Hint Unfold Z.pow_pos Zpower_nat: zarith.
 
 Theorem Zpower_exp x n m :
@@ -226,7 +228,9 @@ Section Powers_of_2.
 
 End Powers_of_2.
 
+#[global]
 Hint Resolve two_p_gt_ZERO: zarith.
+#[global]
 Hint Immediate two_p_pred two_p_S: zarith.
 
 Section power_div_with_rest.
diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v
index f95831436a..943376ecfd 100644
--- a/theories/ZArith/Zquot.v
+++ b/theories/ZArith/Zquot.v
@@ -57,6 +57,7 @@ Proof. now destruct a. Qed.
 Lemma Zquot_0_l a : 0÷a = 0.
 Proof. now destruct a. Qed.
 
+#[global]
 Hint Resolve Zrem_0_l Zrem_0_r Zquot_0_l Zquot_0_r Z.quot_1_r Z.rem_1_r
  : zarith.
 
diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v
index 2ff6805c78..81d2a2d70d 100644
--- a/theories/ZArith/Zwf.v
+++ b/theories/ZArith/Zwf.v
@@ -57,6 +57,7 @@ Section wf_proof.
 
 End wf_proof.
 
+#[global]
 Hint Resolve Zwf_well_founded: datatypes.
 
 
@@ -87,4 +88,5 @@ Section wf_proof_up.
 
 End wf_proof_up.
 
+#[global]
 Hint Resolve Zwf_up_well_founded: datatypes.