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, 10 insertions, 0 deletions

diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v
index e5d364297d..b2b5985ff1 100644
--- a/theories/Logic/Classical_Prop.v
+++ b/theories/Logic/Classical_Prop.v
@@ -16,6 +16,7 @@
 
 Require Import ClassicalFacts.
 
+#[global]
 Hint Unfold not: core.
 
 Axiom classic : forall P:Prop, P \/ ~ P.
diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v
index 998497f13e..5fb6bb3907 100644
--- a/theories/Logic/Decidable.v
+++ b/theories/Logic/Decidable.v
@@ -206,6 +206,7 @@ Qed.
 (** With the following hint database, we can leverage [auto] to check
     decidability of propositions. *)
 
+#[global]
 Hint Resolve dec_True dec_False dec_or dec_and dec_imp dec_not dec_iff
  : decidable_prop.
 
diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v
index f2e15c9abb..934806de93 100644
--- a/theories/Logic/Eqdep.v
+++ b/theories/Logic/Eqdep.v
@@ -35,5 +35,7 @@ Export EqdepTheory.
 
 (** Exported hints *)
 
+#[global]
 Hint Resolve eq_dep_eq: eqdep.
+#[global]
 Hint Resolve inj_pair2 inj_pairT2: eqdep.
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index a918d1ecd7..6589e75289 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -65,6 +65,7 @@ Section Dependent_Equality.
 
   Inductive eq_dep (p:U) (x:P p) : forall q:U, P q -> Prop :=
     eq_dep_intro : eq_dep p x p x.
+  #[local]
   Hint Constructors eq_dep: core.
 
   Lemma eq_dep_refl : forall (p:U) (x:P p), eq_dep p x p x.
@@ -75,6 +76,7 @@ Section Dependent_Equality.
   Proof.
     destruct 1; auto.
   Qed.
+  #[local]
   Hint Immediate eq_dep_sym: core.
 
   Lemma eq_dep_trans :
@@ -221,7 +223,9 @@ Unset Implicit Arguments.
 
 (** Exported hints *)
 
+#[global]
 Hint Resolve eq_dep_intro: core.
+#[global]
 Hint Immediate eq_dep_sym: core.
 
 (************************************************************************)
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index ccd7db177c..7ee3a99d60 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -31,6 +31,7 @@ Arguments JMeq_refl {A x} , [A] x.
 Register JMeq as core.JMeq.type.
 Register JMeq_refl as core.JMeq.refl.
 
+#[global]
 Hint Resolve JMeq_refl : core.
 
 Definition JMeq_hom {A : Type} (x y : A) := JMeq x y.
@@ -42,6 +43,7 @@ Proof.
 intros; destruct H; trivial.
 Qed.
 
+#[global]
 Hint Immediate JMeq_sym : core.
 
 Register JMeq_sym as core.JMeq.sym.