Explicitly annotate all hint declarations of the standard library.

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

8 files changed, 36 insertions, 0 deletions

diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v
index 0f62a9419b..aa0c419f0e 100644
--- a/theories/MSets/MSetDecide.v
+++ b/theories/MSets/MSetDecide.v
@@ -466,6 +466,7 @@ the above form:
     (** Here is the tactic that will throw away hypotheses that
         are not useful (for the intended scope of the [fsetdec]
         tactic). *)
+    #[global]
     Hint Constructors MSet_elt_Prop MSet_Prop : MSet_Prop.
     Ltac discard_nonMSet :=
       repeat (
@@ -518,6 +519,7 @@ the above form:
 
     (** The hint database [MSet_decidability] will be given to
         the [push_neg] tactic from the module [Negation]. *)
+    #[global]
     Hint Resolve dec_In dec_eq : MSet_decidability.
 
     (** ** Normalizing Propositions About Equality
diff --git a/theories/MSets/MSetEqProperties.v b/theories/MSets/MSetEqProperties.v
index dc22af4948..b439be9b3f 100644
--- a/theories/MSets/MSetEqProperties.v
+++ b/theories/MSets/MSetEqProperties.v
@@ -462,9 +462,11 @@ Qed.
 
 End BasicProperties.
 
+#[global]
 Hint Immediate empty_mem is_empty_equal_empty add_mem_1
    remove_mem_1 singleton_equal_add union_mem inter_mem
    diff_mem equal_sym add_remove remove_add : set.
+#[global]
 Hint Resolve equal_mem_1 subset_mem_1 choose_mem_1
    choose_mem_2 add_mem_2 remove_mem_2 equal_refl equal_equal
    subset_refl subset_equal subset_antisym
diff --git a/theories/MSets/MSetFacts.v b/theories/MSets/MSetFacts.v
index 7dbb658e46..ea86c7a4d7 100644
--- a/theories/MSets/MSetFacts.v
+++ b/theories/MSets/MSetFacts.v
@@ -139,12 +139,14 @@ Notation choose_1 := choose_spec1 (only parsing).
 Notation choose_2 := choose_spec2 (only parsing).
 Notation elements_3w := elements_spec2w (only parsing).
 
+#[global]
 Hint Resolve mem_1 equal_1 subset_1 empty_1
     is_empty_1 choose_1 choose_2 add_1 add_2 remove_1
     remove_2 singleton_2 union_1 union_2 union_3
     inter_3 diff_3 fold_1 filter_3 for_all_1 exists_1
     partition_1 partition_2 elements_1 elements_3w
     : set.
+#[global]
 Hint Immediate In_1 mem_2 equal_2 subset_2 is_empty_2 add_3
     remove_3 singleton_1 inter_1 inter_2 diff_1 diff_2
     filter_1 filter_2 for_all_2 exists_2 elements_2
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v
index 58656b666e..37d20bffad 100644
--- a/theories/MSets/MSetGenTree.v
+++ b/theories/MSets/MSetGenTree.v
@@ -46,6 +46,7 @@ End InfoTyp.
 Module Type Ops (X:OrderedType)(Info:InfoTyp).
 
 Definition elt := X.t.
+#[global]
 Hint Transparent elt : core.
 
 Inductive tree  : Type :=
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index fe5d721ffa..c0567f9ef1 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -442,6 +442,7 @@ Module WRaw2SetsOn (E:DecidableType)(M:WRawSets E) <: WSetsOn E.
  Record t_ := Mkt {this :> M.t; is_ok : M.Ok this}.
  Definition t := t_.
  Arguments Mkt this {is_ok}.
+ #[global]
  Hint Resolve is_ok : typeclass_instances.
 
  Definition In (x : elt)(s : t) := M.In x (this s).
@@ -884,9 +885,11 @@ Module MakeListOrdering (O:OrderedType).
         O.lt x y -> lt_list (x :: s) (y :: s')
     | lt_cons_eq : forall x y s s',
         O.eq x y -> lt_list s s' -> lt_list (x :: s) (y :: s').
+ #[global]
  Hint Constructors lt_list : core.
 
  Definition lt := lt_list.
+ #[global]
  Hint Unfold lt : core.
 
  Instance lt_strorder : StrictOrder lt.
@@ -933,6 +936,7 @@ Module MakeListOrdering (O:OrderedType).
   left; MO.order. right; rewrite <- E12; auto.
   left; MO.order. right; rewrite E12; auto.
  Qed.
+ #[global]
  Hint Resolve eq_cons : core.
 
  Lemma cons_CompSpec : forall c x1 x2 l1 l2, O.eq x1 x2 ->
@@ -940,6 +944,7 @@ Module MakeListOrdering (O:OrderedType).
  Proof.
   destruct c; simpl; inversion_clear 2; auto with relations.
  Qed.
+ #[global]
  Hint Resolve cons_CompSpec : core.
 
 End MakeListOrdering.
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index d2878b4710..84cf620474 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -231,13 +231,16 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Notation In := (InA X.eq).
 
   Existing Instance X.eq_equiv.
+  #[local]
   Hint Extern 20 => solve [order] : core.
 
   Definition IsOk s := Sort s.
 
   Class Ok (s:t) : Prop := ok : Sort s.
 
+  #[local]
   Hint Resolve ok : core.
+  #[local]
   Hint Unfold Ok : core.
 
   Instance Sort_Ok s `(Hs : Sort s) : Ok s := { ok := Hs }.
@@ -276,6 +279,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
     destruct H; constructor; tauto.
   Qed.
 
+  #[local]
   Hint Extern 1 (Ok _) => rewrite <- isok_iff : core.
 
   Ltac inv_ok := match goal with
@@ -326,6 +330,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   intuition.
   intros; elim_compare x a; inv; intuition.
   Qed.
+  #[local]
   Hint Resolve add_inf : core.
 
   Global Instance add_ok s x : forall `(Ok s), Ok (add x s).
@@ -353,6 +358,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   intros; elim_compare x a; inv; auto.
   apply Inf_lt with a; auto.
   Qed.
+  #[local]
   Hint Resolve remove_inf : core.
 
   Global Instance remove_ok s x : forall `(Ok s), Ok (remove x s).
@@ -396,6 +402,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Proof.
   induction2.
   Qed.
+  #[local]
   Hint Resolve union_inf : core.
 
   Global Instance union_ok s s' : forall `(Ok s, Ok s'), Ok (union s s').
@@ -422,6 +429,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   apply Hrec'; auto.
   apply Inf_lt with x'; auto.
   Qed.
+  #[local]
   Hint Resolve inter_inf : core.
 
   Global Instance inter_ok s s' : forall `(Ok s, Ok s'), Ok (inter s s').
@@ -452,6 +460,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   apply Hrec'; auto.
   apply Inf_lt with x'; auto.
   Qed.
+  #[local]
   Hint Resolve diff_inf : core.
 
   Global Instance diff_ok s s' : forall `(Ok s, Ok s'), Ok (diff s s').
diff --git a/theories/MSets/MSetProperties.v b/theories/MSets/MSetProperties.v
index 51807e5cda..b49a91ed14 100644
--- a/theories/MSets/MSetProperties.v
+++ b/theories/MSets/MSetProperties.v
@@ -21,6 +21,7 @@ Require Import DecidableTypeEx OrdersLists MSetFacts MSetDecide.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+#[global]
 Hint Unfold transpose : core.
 
 (** First, a functor for Weak Sets in functorial version. *)
@@ -268,7 +269,9 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
 
   End BasicProperties.
 
+  #[global]
   Hint Immediate equal_sym add_remove remove_add union_sym inter_sym: set.
+  #[global]
   Hint Resolve equal_refl equal_trans subset_refl subset_equal subset_antisym
     subset_trans subset_empty subset_remove_3 subset_diff subset_add_3
     subset_add_2 in_subset empty_is_empty_1 empty_is_empty_2 add_equal
@@ -735,6 +738,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
   Proof.
   intros; rewrite cardinal_Empty; auto.
   Qed.
+  #[global]
   Hint Resolve cardinal_inv_1 : core.
 
   Lemma cardinal_inv_2 :
@@ -774,6 +778,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
   exact Equal_cardinal.
   Qed.
 
+  #[global]
   Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal : core.
 
   (** ** Cardinal and set operators *)
@@ -783,6 +788,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
   rewrite cardinal_fold; apply fold_1; auto with *.
   Qed.
 
+  #[global]
   Hint Immediate empty_cardinal cardinal_1 : set.
 
   Lemma singleton_cardinal : forall x, cardinal (singleton x) = 1.
@@ -793,6 +799,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
   apply cardinal_2 with x; auto with set.
   Qed.
 
+  #[global]
   Hint Resolve singleton_cardinal: set.
 
   Lemma diff_inter_cardinal :
@@ -898,6 +905,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
   auto with set.
   Qed.
 
+  #[global]
   Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2 : core.
 
 End WPropertiesOn.
@@ -922,7 +930,9 @@ Module OrdProperties (M:Sets).
   Import M.E.
   Import M.
 
+  #[global]
   Hint Resolve elements_spec2 : core.
+  #[global]
   Hint Immediate
     min_elt_spec1 min_elt_spec2 min_elt_spec3
     max_elt_spec1 max_elt_spec2 max_elt_spec3 : set.
@@ -961,6 +971,7 @@ Module OrdProperties (M:Sets).
   Proof.
    intros a b H; unfold leb. rewrite H; auto.
   Qed.
+  #[global]
   Hint Resolve gtb_compat leb_compat : core.
 
   Lemma elements_split : forall x s,
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v
index 2498d82889..8a5ba2d80f 100644
--- a/theories/MSets/MSetWeakList.v
+++ b/theories/MSets/MSetWeakList.v
@@ -123,14 +123,18 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
   Let eqr:= (@Equivalence_Reflexive _ _ X.eq_equiv).
   Let eqsym:= (@Equivalence_Symmetric _ _ X.eq_equiv).
   Let eqtrans:= (@Equivalence_Transitive _ _ X.eq_equiv).
+  #[local]
   Hint Resolve eqr eqtrans : core.
+  #[local]
   Hint Immediate eqsym : core.
 
   Definition IsOk := NoDup.
 
   Class Ok (s:t) : Prop := ok : NoDup s.
 
+  #[local]
   Hint Unfold Ok : core.
+  #[local]
   Hint Resolve ok : core.
 
   Instance NoDup_Ok s (nd : NoDup s) : Ok s := { ok := nd }.