Explicitly annotate all hint declarations of the standard library.

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

5 files changed, 18 insertions, 0 deletions

diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index fa4f9134cc..b008c6c2aa 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -95,7 +95,9 @@ Proof.
 symmetry. apply Z.ge_le_iff.
 Qed.
 
+#[global]
 Hint Unfold Qeq Qlt Qle : qarith.
+#[global]
 Hint Extern 5 (?X1 <> ?X2) => intro; discriminate: qarith.
 
 Lemma Qcompare_antisym x y : CompOpp (x ?= y) = (y ?= x).
@@ -127,7 +129,9 @@ apply Z.mul_reg_r with (QDen y); [auto with qarith|].
 now rewrite Z.mul_shuffle0, XY, Z.mul_shuffle0, YZ, Z.mul_shuffle0.
 Qed.
 
+#[global]
 Hint Immediate Qeq_sym : qarith.
+#[global]
 Hint Resolve Qeq_refl Qeq_trans : qarith.
 
 (** In a word, [Qeq] is a setoid equality. *)
@@ -203,6 +207,7 @@ Proof.
   rewrite !Qeq_bool_iff; apply Qeq_trans.
 Qed.
 
+#[global]
 Hint Resolve Qnot_eq_sym : qarith.
 
 (** * Addition, multiplication and opposite *)
@@ -783,6 +788,7 @@ Proof.
   Close Scope Z_scope.
 Qed.
 
+#[global]
 Hint Resolve Qle_trans : qarith.
 
 Lemma Qlt_irrefl x : ~x<x.
@@ -863,6 +869,7 @@ Proof.
   unfold Qle, Qlt, Qeq; intros; now apply Z.lt_eq_cases.
 Qed.
 
+#[global]
 Hint Resolve Qle_not_lt Qlt_not_le Qnot_le_lt Qnot_lt_le
  Qlt_le_weak Qlt_not_eq Qle_antisym Qle_refl: qarith.
 
@@ -904,6 +911,7 @@ Proof.
 Qed.
 
 
+#[global]
 Hint Resolve Qopp_le_compat : qarith.
 
 Lemma Qle_minus_iff : forall p q, p <= q <-> 0 <= q+-p.
diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v
index 13e88fc093..d1ff1fc794 100644
--- a/theories/QArith/Qabs.v
+++ b/theories/QArith/Qabs.v
@@ -11,6 +11,7 @@
 Require Export QArith.
 Require Export Qreduction.
 
+#[global]
 Hint Resolve Qlt_le_weak : qarith.
 
 Definition Qabs (x:Q) := let (n,d):=x in (Z.abs n#d).
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index 63b0a5afb7..bd43f901bb 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -66,6 +66,7 @@ Proof.
   rewrite hq, hq' in H'. subst q'. f_equal.
   apply eq_proofs_unicity. intros.  repeat decide equality.
 Qed.
+#[global]
 Hint Resolve Qc_is_canon : core.
 
 Theorem Qc_decomp: forall q q': Qc, (q:Q) = q' -> q = q'.
diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v
index 20b5cb236b..5a23a20811 100644
--- a/theories/QArith/Qreals.v
+++ b/theories/QArith/Qreals.v
@@ -19,6 +19,7 @@ intros.
 now apply not_O_IZR.
 Qed.
 
+#[global]
 Hint Resolve IZR_nz Rmult_integral_contrapositive : core.
 
 Lemma eqR_Qeq : forall x y : Q, Q2R x = Q2R y -> x==y.
diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v
index 8fd342ab15..06f4ca02d1 100644
--- a/theories/QArith/Qround.v
+++ b/theories/QArith/Qround.v
@@ -18,6 +18,7 @@ rewrite !Z.mul_opp_l.
 apply Z.opp_lt_mono.
 Qed.
 
+#[global]
 Hint Resolve Qopp_lt_compat : qarith.
 
 (************)
@@ -54,6 +55,7 @@ rewrite Z.mul_comm.
 now apply Z.mul_div_le.
 Qed.
 
+#[global]
 Hint Resolve Qfloor_le : qarith.
 
 Lemma Qle_ceiling : forall x, x <= Qceiling x.
@@ -66,6 +68,7 @@ change (Qceiling x:Q) with (-(Qfloor(-x))).
 auto with *.
 Qed.
 
+#[global]
 Hint Resolve Qle_ceiling : qarith.
 
 Lemma Qle_floor_ceiling : forall x, Qfloor x <= Qceiling x.
@@ -88,6 +91,7 @@ rewrite <- Z.lt_add_lt_sub_r.
 destruct (Z_mod_lt n (Zpos d)); auto with *.
 Qed.
 
+#[global]
 Hint Resolve Qlt_floor : qarith.
 
 Lemma Qceiling_lt : forall x, (Qceiling x-1)%Z < x.
@@ -101,6 +105,7 @@ rewrite Qopp_involutive.
 auto with *.
 Qed.
 
+#[global]
 Hint Resolve Qceiling_lt : qarith.
 
 Lemma Qfloor_resp_le : forall x y, x <= y -> (Qfloor x <= Qfloor y)%Z.
@@ -114,6 +119,7 @@ rewrite (Z.mul_comm (Zpos yd) (Zpos xd)).
 apply Z_div_le; auto with *.
 Qed.
 
+#[global]
 Hint Resolve Qfloor_resp_le : qarith.
 
 Lemma Qceiling_resp_le : forall x y, x <= y -> (Qceiling x <= Qceiling y)%Z.
@@ -123,6 +129,7 @@ unfold Qceiling.
 rewrite <- Z.opp_le_mono; auto with qarith.
 Qed.
 
+#[global]
 Hint Resolve Qceiling_resp_le : qarith.
 
 Add Morphism Qfloor with signature Qeq ==> eq as Qfloor_comp.