Explicitly annotate all hint declarations of the standard library.

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

14 files changed, 82 insertions, 0 deletions

diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index 74d1e391c4..71c8f10755 100644
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.v
@@ -24,6 +24,7 @@ Section Between.
     | bet_emp : between k k
     | bet_S : forall l, between k l -> P l -> between k (S l).
 
+  #[local]
   Hint Constructors between: arith.
 
   Lemma bet_eq : forall k l, l = k -> between k l.
@@ -31,18 +32,21 @@ Section Between.
     intros * ->; auto with arith.
   Qed.
 
+  #[local]
   Hint Resolve bet_eq: arith.
 
   Lemma between_le : forall k l, between k l -> k <= l.
   Proof.
     induction 1; auto with arith.
   Qed.
+  #[local]
   Hint Immediate between_le: arith.
 
   Lemma between_Sk_l : forall k l, between k l -> S k <= l -> between (S k) l.
   Proof.
     induction 1 as [|* [|]]; auto with arith.
   Qed.
+  #[local]
   Hint Resolve between_Sk_l: arith.
 
   Lemma between_restr :
@@ -57,6 +61,7 @@ Section Between.
     | exists_S : forall l, exists_between k l -> exists_between k (S l)
     | exists_le : forall l, k <= l -> Q l -> exists_between k (S l).
 
+  #[local]
   Hint Constructors exists_between: arith.
 
   Lemma exists_le_S : forall k l, exists_between k l -> S k <= l.
@@ -66,12 +71,14 @@ Section Between.
 
   Lemma exists_lt : forall k l, exists_between k l -> k < l.
   Proof exists_le_S.
+  #[local]
   Hint Immediate exists_le_S exists_lt: arith.
 
   Lemma exists_S_le : forall k l, exists_between k (S l) -> k <= l.
   Proof.
     intros; apply le_S_n; auto with arith.
   Qed.
+  #[local]
   Hint Immediate exists_S_le: arith.
 
   Definition in_int p q r := p <= r /\ r < q.
@@ -80,6 +87,7 @@ Section Between.
   Proof.
     split; assumption.
   Qed.
+  #[local]
   Hint Resolve in_int_intro: arith.
 
   Lemma in_int_lt : forall p q r, in_int p q r -> p < q.
@@ -99,12 +107,14 @@ Section Between.
   Proof.
     intros * []; auto with arith.
   Qed.
+  #[local]
   Hint Resolve in_int_S: arith.
 
   Lemma in_int_Sp_q : forall p q r, in_int (S p) q r -> in_int p q r.
   Proof.
     intros * []; auto with arith.
   Qed.
+  #[local]
   Hint Immediate in_int_Sp_q: arith.
 
   Lemma between_in_int :
@@ -188,6 +198,8 @@ Section Between.
 
 End Between.
 
+#[global]
 Hint Resolve nth_O bet_S bet_emp bet_eq between_Sk_l exists_S exists_le
   in_int_S in_int_intro: arith.
+#[global]
 Hint Immediate in_int_Sp_q exists_le_S exists_S_le: arith.
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 2d34412908..c52edf9994 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -42,6 +42,7 @@ Qed.
 Lemma lt_div2 n : 0 < n -> div2 n < n.
 Proof. apply Nat.lt_div2. Qed.
 
+#[global]
 Hint Resolve lt_div2: arith.
 
 (** Properties related to the parity *)
@@ -73,6 +74,7 @@ Proof.
  symmetry in Ev'. elim (n_Sn _ Ev').
 Qed.
 
+#[global]
 Hint Resolve even_div2 div2_even odd_div2 div2_odd: arith.
 
 Lemma even_odd_div2 n :
@@ -88,6 +90,7 @@ Qed.
 
 Notation double := Nat.double (only parsing).
 
+#[global]
 Hint Unfold double Nat.double: arith.
 
 Lemma double_S n : double (S n) = S (S (double n)).
@@ -100,6 +103,7 @@ Proof.
   apply Nat.add_shuffle1.
 Qed.
 
+#[global]
 Hint Resolve double_S: arith.
 
 Lemma even_odd_double n :
@@ -133,6 +137,7 @@ Proof proj1 (proj2 (even_odd_double n)).
 Lemma double_odd n : n = S (double (div2 n)) -> odd n.
 Proof proj2 (proj2 (even_odd_double n)).
 
+#[global]
 Hint Resolve even_double double_even odd_double double_odd: arith.
 
 (** Application:
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index 593d8c5934..66678b24f8 100644
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -27,6 +27,7 @@ Theorem eq_nat_refl n : eq_nat n n.
 Proof.
   induction n; simpl; auto.
 Qed.
+#[global]
 Hint Resolve eq_nat_refl: arith.
 
 (** [eq] restricted to [nat] and [eq_nat] are equivalent *)
@@ -48,6 +49,7 @@ Proof.
  apply eq_nat_is_eq.
 Qed.
 
+#[global]
 Hint Immediate eq_eq_nat eq_nat_eq: arith.
 
 Theorem eq_nat_elim :
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index 3422596818..87d6a6ee64 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -31,7 +31,9 @@ Inductive even : nat -> Prop :=
 with odd : nat -> Prop :=
     odd_S : forall n, even n -> odd (S n).
 
+#[global]
 Hint Constructors even: arith.
+#[global]
 Hint Constructors odd: arith.
 
 (** * Equivalence with predicates [Nat.Even] and [Nat.odd] *)
@@ -178,6 +180,7 @@ Proof. parity_binop. Qed.
 Lemma odd_mult_inv_r n m : odd (n * m) -> odd m.
 Proof. parity_binop. Qed.
 
+#[global]
 Hint Resolve
  even_even_plus odd_even_plus odd_plus_l odd_plus_r
  even_mult_l even_mult_r even_mult_l even_mult_r odd_mult : arith.
diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v
index 05d585b9a2..492aeba66b 100644
--- a/theories/Arith/Gt.v
+++ b/theories/Arith/Gt.v
@@ -135,13 +135,21 @@ Qed.
 
 (** * Hints *)
 
+#[global]
 Hint Resolve gt_Sn_O gt_Sn_n gt_n_S : arith.
+#[global]
 Hint Immediate gt_S_n gt_pred : arith.
+#[global]
 Hint Resolve gt_irrefl gt_asym : arith.
+#[global]
 Hint Resolve le_not_gt gt_not_le : arith.
+#[global]
 Hint Immediate le_S_gt gt_S_le : arith.
+#[global]
 Hint Resolve gt_le_S le_gt_S : arith.
+#[global]
 Hint Resolve gt_trans_S le_gt_trans gt_le_trans: arith.
+#[global]
 Hint Resolve plus_gt_compat_l: arith.
 
 (* begin hide *)
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index 4e71465452..3d176fb644 100644
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -32,7 +32,9 @@ Notation le_refl := Nat.le_refl (only parsing).
 Notation le_trans := Nat.le_trans (only parsing).
 Notation le_antisym := Nat.le_antisymm (only parsing).
 
+#[global]
 Hint Resolve le_trans: arith.
+#[global]
 Hint Immediate le_antisym: arith.
 
 (** * Properties of [le] w.r.t 0 *)
@@ -61,8 +63,11 @@ Notation le_Sn_n := Nat.nle_succ_diag_l (only parsing). (* ~ S n <= n *)
 Theorem le_Sn_le : forall n m, S n <= m -> n <= m.
 Proof Nat.lt_le_incl.
 
+#[global]
 Hint Resolve le_0_n le_Sn_0: arith.
+#[global]
 Hint Resolve le_n_S le_n_Sn le_Sn_n : arith.
+#[global]
 Hint Immediate le_n_0_eq le_Sn_le le_S_n : arith.
 
 (** * Properties of [le] w.r.t predecessor *)
@@ -70,6 +75,7 @@ Hint Immediate le_n_0_eq le_Sn_le le_S_n : arith.
 Notation le_pred_n := Nat.le_pred_l (only parsing). (* pred n <= n *)
 Notation le_pred := Nat.pred_le_mono (only parsing). (* n<=m -> pred n <= pred m *)
 
+#[global]
 Hint Resolve le_pred_n: arith.
 
 (** * A different elimination principle for the order on natural numbers *)
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index 60cc361e35..467420afb3 100644
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -27,6 +27,7 @@ Local Open Scope nat_scope.
 
 Notation lt_irrefl := Nat.lt_irrefl (only parsing). (* ~ x < x *)
 
+#[global]
 Hint Resolve lt_irrefl: arith.
 
 (** * Relationship between [le] and [lt] *)
@@ -50,8 +51,11 @@ Qed.
 
 Register le_lt_n_Sm as num.nat.le_lt_n_Sm.
 
+#[global]
 Hint Immediate lt_le_S: arith.
+#[global]
 Hint Immediate lt_n_Sm_le: arith.
+#[global]
 Hint Immediate le_lt_n_Sm: arith.
 
 Theorem le_not_lt n m : n <= m -> ~ m < n.
@@ -64,6 +68,7 @@ Proof.
  apply Nat.lt_nge.
 Qed.
 
+#[global]
 Hint Immediate le_not_lt lt_not_le: arith.
 
 (** * Asymmetry *)
@@ -85,7 +90,9 @@ Proof.
  intros. now apply Nat.neq_sym, Nat.neq_0_lt_0.
 Qed.
 
+#[global]
 Hint Resolve lt_0_Sn lt_n_0 : arith.
+#[global]
 Hint Immediate neq_0_lt lt_0_neq: arith.
 
 (** * Order and successor *)
@@ -105,7 +112,9 @@ Qed.
 
 Register lt_S_n as num.nat.lt_S_n.
 
+#[global]
 Hint Resolve lt_n_Sn lt_S lt_n_S : arith.
+#[global]
 Hint Immediate lt_S_n : arith.
 
 (** * Predecessor *)
@@ -130,7 +139,9 @@ Proof.
  intros. now apply Nat.lt_pred_l, Nat.neq_0_lt_0.
 Qed.
 
+#[global]
 Hint Immediate lt_pred: arith.
+#[global]
 Hint Resolve lt_pred_n_n: arith.
 
 (** * Transitivity properties *)
@@ -141,6 +152,7 @@ Notation le_lt_trans := Nat.le_lt_trans (only parsing).
 
 Register le_lt_trans as num.nat.le_lt_trans.
 
+#[global]
 Hint Resolve lt_trans lt_le_trans le_lt_trans: arith.
 
 (** * Large = strict or equal *)
@@ -154,6 +166,7 @@ Qed.
 
 Notation lt_le_weak := Nat.lt_le_incl (only parsing).
 
+#[global]
 Hint Immediate lt_le_weak: arith.
 
 (** * Dichotomy *)
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index 28fe51f9af..863b02ef2e 100644
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -43,8 +43,10 @@ Notation max_case2 := max_case (only parsing).
 Notation max_SS := Nat.succ_max_distr (only parsing).
 (* end hide *)
 
+#[global]
 Hint Resolve
  Nat.max_l Nat.max_r Nat.le_max_l Nat.le_max_r : arith.
 
+#[global]
 Hint Resolve
  Nat.min_l Nat.min_r Nat.le_min_l Nat.le_min_r : arith.
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index b8c7ac147a..6cbba63e1a 100644
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -111,13 +111,23 @@ Qed.
 
 (** * Hints *)
 
+#[global]
 Hint Resolve minus_n_O: arith.
+#[global]
 Hint Resolve minus_Sn_m: arith.
+#[global]
 Hint Resolve minus_diag_reverse: arith.
+#[global]
 Hint Resolve minus_plus_simpl_l_reverse: arith.
+#[global]
 Hint Immediate plus_minus: arith.
+#[global]
 Hint Resolve minus_plus: arith.
+#[global]
 Hint Resolve le_plus_minus: arith.
+#[global]
 Hint Resolve le_plus_minus_r: arith.
+#[global]
 Hint Resolve lt_minus: arith.
+#[global]
 Hint Immediate lt_O_minus_lt: arith.
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index d7f703e6e4..584b282f4d 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -33,12 +33,14 @@ Notation mult_0_r := Nat.mul_0_r (only parsing). (* n * 0 = 0 *)
 Notation mult_1_l := Nat.mul_1_l (only parsing). (* 1 * n = n *)
 Notation mult_1_r := Nat.mul_1_r (only parsing). (* n * 1 = n *)
 
+#[global]
 Hint Resolve mult_1_l mult_1_r: arith.
 
 (** ** Commutativity *)
 
 Notation mult_comm := Nat.mul_comm (only parsing). (* n * m = m * n *)
 
+#[global]
 Hint Resolve mult_comm: arith.
 
 (** ** Distributivity *)
@@ -55,8 +57,11 @@ Notation mult_minus_distr_r :=
 Notation mult_minus_distr_l :=
   Nat.mul_sub_distr_l (only parsing). (* n*(m-p) = n*m - n*p *)
 
+#[global]
 Hint Resolve mult_plus_distr_r: arith.
+#[global]
 Hint Resolve mult_minus_distr_r: arith.
+#[global]
 Hint Resolve mult_minus_distr_l: arith.
 
 (** ** Associativity *)
@@ -68,7 +73,9 @@ Proof.
  symmetry. apply Nat.mul_assoc.
 Qed.
 
+#[global]
 Hint Resolve mult_assoc_reverse: arith.
+#[global]
 Hint Resolve mult_assoc: arith.
 
 (** ** Inversion lemmas *)
@@ -94,12 +101,14 @@ Lemma mult_O_le n m : m = 0 \/ n <= m * n.
 Proof.
  destruct m; [left|right]; simpl; trivial using Nat.le_add_r.
 Qed.
+#[global]
 Hint Resolve mult_O_le: arith.
 
 Lemma mult_le_compat_l n m p : n <= m -> p * n <= p * m.
 Proof.
  apply Nat.mul_le_mono_nonneg_l, Nat.le_0_l. (* TODO : get rid of 0<=n hyp *)
 Qed.
+#[global]
 Hint Resolve mult_le_compat_l: arith.
 
 Lemma mult_le_compat_r n m p : n <= m -> n * p <= m * p.
@@ -117,6 +126,7 @@ Proof.
   apply Nat.mul_lt_mono_pos_l, Nat.lt_0_succ.
 Qed.
 
+#[global]
 Hint Resolve mult_S_lt_compat_l: arith.
 
 Lemma mult_lt_compat_l n m p : n < m -> 0 < p -> p * n < p * m.
diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v
index 37704704a0..8d3b1b318a 100644
--- a/theories/Arith/PeanoNat.v
+++ b/theories/Arith/PeanoNat.v
@@ -765,7 +765,9 @@ Infix "?=" := Nat.compare (at level 70) : nat_scope.
 Infix "/" := Nat.div : nat_scope.
 Infix "mod" := Nat.modulo (at level 40, no associativity) : nat_scope.
 
+#[global]
 Hint Unfold Nat.le : core.
+#[global]
 Hint Unfold Nat.lt : core.
 
 Register Nat.le_trans as num.nat.le_trans.
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index 9a7a397023..2fc44ba592 100644
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -23,6 +23,7 @@ Defined.
 
 Notation eq_nat_dec := Nat.eq_dec (only parsing).
 
+#[global]
 Hint Resolve O_or_S eq_nat_dec: arith.
 
 Theorem dec_eq_nat n m : decidable (n = m).
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 5da7738adc..49e242276e 100644
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -179,11 +179,17 @@ Proof (succ_plus_discr n 3).
 
 (** * Compatibility Hints *)
 
+#[global]
 Hint Immediate plus_comm : arith.
+#[global]
 Hint Resolve plus_assoc plus_assoc_reverse : arith.
+#[global]
 Hint Resolve plus_le_compat_l plus_le_compat_r : arith.
+#[global]
 Hint Resolve le_plus_l le_plus_r le_plus_trans : arith.
+#[global]
 Hint Immediate lt_plus_trans : arith.
+#[global]
 Hint Resolve plus_lt_compat_l plus_lt_compat_r : arith.
 
 (** For compatibility, we "Require" the same files as before *)
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index ebd909c1dc..a87eeba9b1 100644
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -197,7 +197,9 @@ Proof.
   intros n H q; pattern q; apply lt_wf_ind; auto with arith.
 Qed.
 
+#[global]
 Hint Resolve lt_wf: arith.
+#[global]
 Hint Resolve well_founded_lt_compat: arith.
 
 Section LT_WF_REL.