Explicitly annotate all hint declarations of the standard library.

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

6 files changed, 38 insertions, 0 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 9984bff0c2..f013c857ea 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -83,6 +83,7 @@ Lemma andb_prop (a b:bool) : andb a b = true -> a = true /\ b = true.
 Proof.
   destruct a, b; repeat split; assumption.
 Qed.
+#[global]
 Hint Resolve andb_prop: bool.
 
 Register andb_prop as core.bool.andb_prop.
@@ -92,6 +93,7 @@ Lemma andb_true_intro (b1 b2:bool) :
 Proof.
   destruct b1; destruct b2; simpl; intros [? ?]; assumption.
 Qed.
+#[global]
 Hint Resolve andb_true_intro: bool.
 
 Register andb_true_intro as core.bool.andb_true_intro.
@@ -100,6 +102,7 @@ Register andb_true_intro as core.bool.andb_true_intro.
 
 Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.
 
+#[global]
 Hint Constructors eq_true : eq_true.
 
 Register eq_true as core.eq_true.type.
@@ -142,6 +145,7 @@ Defined.
 Inductive BoolSpec (P Q : Prop) : bool -> Prop :=
   | BoolSpecT : P -> BoolSpec P Q true
   | BoolSpecF : Q -> BoolSpec P Q false.
+#[global]
 Hint Constructors BoolSpec : core.
 
 Register BoolSpec as core.BoolSpec.type.
@@ -243,6 +247,7 @@ Section projections.
 
 End projections.
 
+#[global]
 Hint Resolve pair inl inr: core.
 
 Lemma surjective_pairing (A B:Type) (p:A * B) : p = (fst p, snd p).
@@ -380,6 +385,7 @@ Inductive CompareSpec (Peq Plt Pgt : Prop) : comparison -> Prop :=
  | CompEq : Peq -> CompareSpec Peq Plt Pgt Eq
  | CompLt : Plt -> CompareSpec Peq Plt Pgt Lt
  | CompGt : Pgt -> CompareSpec Peq Plt Pgt Gt.
+#[global]
 Hint Constructors CompareSpec : core.
 
 Register CompareSpec as core.CompareSpec.type.
@@ -395,6 +401,7 @@ Inductive CompareSpecT (Peq Plt Pgt : Prop) : comparison -> Type :=
  | CompEqT : Peq -> CompareSpecT Peq Plt Pgt Eq
  | CompLtT : Plt -> CompareSpecT Peq Plt Pgt Lt
  | CompGtT : Pgt -> CompareSpecT Peq Plt Pgt Gt.
+#[global]
 Hint Constructors CompareSpecT : core.
 
 Register CompareSpecT as core.CompareSpecT.type.
@@ -417,6 +424,7 @@ Definition CompSpec {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Prop :=
 
 Definition CompSpecT {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Type :=
  CompareSpecT (eq x y) (lt x y) (lt y x).
+#[global]
 Hint Unfold CompSpec CompSpecT : core.
 
 Lemma CompSpec2Type : forall A (eq lt:A->A->Prop) x y c,
@@ -435,6 +443,7 @@ Proof. intros. apply CompareSpec2Type; assumption. Defined.
 
 Inductive identity (A:Type) (a:A) : A -> Type :=
   identity_refl : identity a a.
+#[global]
 Hint Resolve identity_refl: core.
 
 Arguments identity_ind [A] a P f y i.
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 8012235143..023705e169 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -41,9 +41,12 @@ Register not as core.not.type.
   variables and constants explicitly. *)
 
 Create HintDb core.
+#[global]
 Hint Variables Opaque : core.
+#[global]
 Hint Constants Opaque : core.
 
+#[global]
 Hint Unfold not: core.
 
   (** [and A B], written [A /\ B], is the conjunction of [A] and [B]
@@ -119,6 +122,7 @@ Theorem iff_sym : forall A B:Prop, (A <-> B) -> (B <-> A).
 
 End Equivalence.
 
+#[global]
 Hint Unfold iff: extcore.
 
 (** Backward direction of the equivalences above does not need assumptions *)
@@ -364,8 +368,11 @@ Notation "x = y" := (eq x y) : type_scope.
 Notation "x <> y  :> T" := (~ x = y :>T) : type_scope.
 Notation "x <> y" := (~ (x = y)) : type_scope.
 
+#[global]
 Hint Resolve I conj or_introl or_intror : core.
+#[global]
 Hint Resolve eq_refl: core.
+#[global]
 Hint Resolve ex_intro ex_intro2: core.
 
 Register eq as core.eq.type.
@@ -733,6 +740,7 @@ Notation sym_equal := eq_sym (only parsing).
 Notation trans_equal := eq_trans (only parsing).
 Notation sym_not_equal := not_eq_sym (only parsing).
 
+#[global]
 Hint Immediate eq_sym not_eq_sym: core.
 
 (** Basic definitions about relations and properties *)
@@ -801,6 +809,7 @@ Qed.
 
 Inductive inhabited (A:Type) : Prop := inhabits : A -> inhabited A.
 
+#[global]
 Hint Resolve inhabits: core.
 
 Lemma exists_inhabited : forall (A:Type) (P:A->Prop),
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index 3d9937ae89..f8869615cd 100644
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -72,6 +72,7 @@ Definition identity_rect_r :
  intros A x P H y H0; case identity_sym with (1 := H0); trivial.
 Defined.
 
+#[global]
 Hint Immediate identity_sym not_identity_sym: core.
 
 Notation refl_id := identity_refl (only parsing).
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 98fd52f351..fb2a7a57fe 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -37,6 +37,7 @@ Local Notation "0" := O.
 Definition eq_S := f_equal S.
 Definition f_equal_nat := f_equal (A:=nat).
 
+#[global]
 Hint Resolve f_equal_nat: core.
 
 (** The predecessor function *)
@@ -53,12 +54,14 @@ Qed.
 (** Injectivity of successor *)
 
 Definition eq_add_S n m (H: S n = S m): n = m := f_equal pred H.
+#[global]
 Hint Immediate eq_add_S: core.
 
 Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m.
 Proof.
   red; auto.
 Qed.
+#[global]
 Hint Resolve not_eq_S: core.
 
 Definition IsSucc (n:nat) : Prop :=
@@ -73,12 +76,14 @@ Theorem O_S : forall n:nat, 0 <> S n.
 Proof.
   discriminate.
 Qed.
+#[global]
 Hint Resolve O_S: core.
 
 Theorem n_Sn : forall n:nat, n <> S n.
 Proof.
   intro n; induction n; auto.
 Qed.
+#[global]
 Hint Resolve n_Sn: core.
 
 (** Addition *)
@@ -88,6 +93,7 @@ Infix "+" := Nat.add : nat_scope.
 
 Definition f_equal2_plus := f_equal2 plus.
 Definition f_equal2_nat := f_equal2 (A1:=nat) (A2:=nat). 
+#[global]
 Hint Resolve f_equal2_nat: core.
 
 Lemma plus_n_O : forall n:nat, n = n + 0.
@@ -95,7 +101,9 @@ Proof.
   intro n; induction n; simpl; auto.
 Qed.
 
+#[global]
 Remove Hints eq_refl : core.
+#[global]
 Hint Resolve plus_n_O eq_refl: core.  (* We want eq_refl to have higher priority than plus_n_O *)
 
 Lemma plus_O_n : forall n:nat, 0 + n = n.
@@ -107,6 +115,7 @@ Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m.
 Proof.
   intros n m; induction n; simpl; auto.
 Qed.
+#[global]
 Hint Resolve plus_n_Sm: core.
 
 Lemma plus_Sn_m : forall n m:nat, S n + m = S (n + m).
@@ -125,12 +134,14 @@ Notation mult := Nat.mul (only parsing).
 Infix "*" := Nat.mul : nat_scope.
 
 Definition f_equal2_mult := f_equal2 mult.
+#[global]
 Hint Resolve f_equal2_mult: core.
 
 Lemma mult_n_O : forall n:nat, 0 = n * 0.
 Proof.
   intro n; induction n; simpl; auto.
 Qed.
+#[global]
 Hint Resolve mult_n_O: core.
 
 Lemma mult_n_Sm : forall n m:nat, n * m + n = n * S m.
@@ -139,6 +150,7 @@ Proof.
   destruct H; rewrite <- plus_n_Sm; apply eq_S.
   pattern m at 1 3; elim m; simpl; auto.
 Qed.
+#[global]
 Hint Resolve mult_n_Sm: core.
 
 (** Standard associated names *)
@@ -162,20 +174,24 @@ where "n <= m" := (le n m) : nat_scope.
 
 Register le_n as num.nat.le_n.
 
+#[global]
 Hint Constructors le: core.
 (*i equivalent to : "Hints Resolve le_n le_S : core." i*)
 
 Definition lt (n m:nat) := S n <= m.
+#[global]
 Hint Unfold lt: core.
 
 Infix "<" := lt : nat_scope.
 
 Definition ge (n m:nat) := m <= n.
+#[global]
 Hint Unfold ge: core.
 
 Infix ">=" := ge : nat_scope.
 
 Definition gt (n m:nat) := m < n.
+#[global]
 Hint Unfold gt: core.
 
 Infix ">" := gt : nat_scope.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 1fb6dabe6f..5d759f3234 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -797,5 +797,7 @@ Proof.
   apply (h2 h1).
 Defined.
 
+#[global]
 Hint Resolve left right inleft inright: core.
+#[global]
 Hint Resolve exist exist2 existT existT2: core.
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 35bab1021e..8721b7c797 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -339,5 +339,6 @@ Tactic Notation "assert_fails" tactic3(tac) :=
   assert_fails tac.
 
 Create HintDb rewrite discriminated.
+#[global]
 Hint Variables Opaque : rewrite.
 Create HintDb typeclass_instances discriminated.