Explicitly annotate all hint declarations of the standard library.

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

11 files changed, 67 insertions, 0 deletions

diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index ad0124db6d..bfa50d7fae 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -41,6 +41,7 @@ Local Open Scope Int_scope.
 Local Notation int := I.t.
 
 Definition key := X.t.
+#[global]
 Hint Transparent key : core.
 
 (** * Trees *)
@@ -495,7 +496,9 @@ Functional Scheme map2_opt_ind := Induction for map2_opt Sort Prop.
 
 (** * Automation and dedicated tactics. *)
 
+#[global]
 Hint Constructors tree MapsTo In bst : core.
+#[global]
 Hint Unfold lt_tree gt_tree : core.
 
 Tactic Notation "factornode" ident(l) ident(x) ident(d) ident(r) ident(h)
@@ -576,6 +579,7 @@ Lemma MapsTo_In : forall k e m, MapsTo k e m -> In k m.
 Proof.
  induction 1; auto.
 Qed.
+#[local]
 Hint Resolve MapsTo_In : core.
 
 Lemma In_MapsTo : forall k m, In k m -> exists e, MapsTo k e m.
@@ -595,6 +599,7 @@ Lemma MapsTo_1 :
 Proof.
  induction m; simpl; intuition_in; eauto with ordered_type.
 Qed.
+#[local]
 Hint Immediate MapsTo_1 : core.
 
 Lemma In_1 :
@@ -634,6 +639,7 @@ Proof.
  unfold gt_tree in *; intuition_in; order.
 Qed.
 
+#[local]
 Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node : core.
 
 Lemma lt_left : forall x y l r e h,
@@ -660,6 +666,7 @@ Proof.
  intuition_in.
 Qed.
 
+#[local]
 Hint Resolve lt_left lt_right gt_left gt_right : core.
 
 Lemma lt_tree_not_in :
@@ -686,6 +693,7 @@ Proof.
  eauto with ordered_type.
 Qed.
 
+#[local]
 Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans : core.
 
 (** * Empty map *)
@@ -818,6 +826,7 @@ Lemma create_bst :
 Proof.
  unfold create; auto.
 Qed.
+#[local]
 Hint Resolve create_bst : core.
 
 Lemma create_in :
@@ -835,6 +844,7 @@ Proof.
  (apply lt_tree_node || apply gt_tree_node); auto with ordered_type;
  (eapply lt_tree_trans || eapply gt_tree_trans); eauto with ordered_type.
 Qed.
+#[local]
 Hint Resolve bal_bst : core.
 
 Lemma bal_in : forall l x e r y,
@@ -876,6 +886,7 @@ Proof.
  apply MX.eq_lt with x; auto.
  apply MX.lt_eq with x; auto with ordered_type.
 Qed.
+#[local]
 Hint Resolve add_bst : core.
 
 Lemma add_1 : forall m x y e, X.eq x y -> MapsTo y e (add x e m).
@@ -956,6 +967,7 @@ Proof.
  destruct 1.
  apply H2; intuition.
 Qed.
+#[local]
 Hint Resolve remove_min_bst : core.
 
 Lemma remove_min_gt_tree : forall l x e r h,
@@ -975,6 +987,7 @@ Proof.
  assert (X.lt m#1 x) by order.
  decompose [or] H; order.
 Qed.
+#[local]
 Hint Resolve remove_min_gt_tree : core.
 
 Lemma remove_min_find : forall l x e r h y,
@@ -1127,6 +1140,7 @@ Proof.
  intuition; [ apply MX.lt_eq with x | ]; eauto with ordered_type.
  intuition; [ apply MX.eq_lt with x | ]; eauto with ordered_type.
 Qed.
+#[local]
 Hint Resolve join_bst : core.
 
 Lemma join_find : forall l x d r y,
@@ -1263,6 +1277,7 @@ Proof.
  rewrite remove_min_in, e1; simpl; auto with ordered_type.
  change (gt_tree (m2',xd)#2#1 (m2',xd)#1). rewrite <-e1; eauto.
 Qed.
+#[local]
 Hint Resolve concat_bst : core.
 
 Lemma concat_find : forall m1 m2 y, bst m1 -> bst m2 ->
@@ -1351,6 +1366,7 @@ Proof.
  intros; unfold elements; apply elements_aux_sort; auto.
  intros; inversion H0.
 Qed.
+#[local]
 Hint Resolve elements_sort : core.
 
 Lemma elements_nodup : forall s : t elt, bst s -> NoDupA eqk (elements s).
@@ -1620,6 +1636,7 @@ destruct (map_option_2 H) as (d0 & ? & ?).
 destruct (map_option_2 H') as (d0' & ? & ?).
 eapply X.lt_trans with x; eauto using MapsTo_In.
 Qed.
+#[local]
 Hint Resolve map_option_bst : core.
 
 Ltac nonify e :=
@@ -1719,6 +1736,7 @@ apply X.lt_trans with x1.
 destruct (map2_opt_2 H1 H6 Hy); intuition.
 destruct (map2_opt_2 H2 H7 Hy'); intuition.
 Qed.
+#[local]
 Hint Resolve map2_opt_bst : core.
 
 Ltac map2_aux :=
@@ -2075,6 +2093,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
   Proof.
    destruct c; simpl; intros; P.MX.elim_comp; auto with ordered_type.
   Qed.
+  #[global]
   Hint Resolve cons_Cmp : core.
 
   Lemma compare_end_Cmp :
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 2001201ec3..bb52166ca7 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -20,6 +20,7 @@ Require Export FMapInterface.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+#[global]
 Hint Extern 1 (Equivalence _) => constructor; congruence : core.
 
 (** * Facts about weak maps *)
@@ -371,6 +372,7 @@ Proof.
 intros. rewrite eq_option_alt. intro e'. rewrite <- 2 find_mapsto_iff.
 apply add_neq_mapsto_iff; auto.
 Qed.
+#[local]
 Hint Resolve add_neq_o : map.
 
 Lemma add_o : forall m x y e,
@@ -404,6 +406,7 @@ Proof.
 intros. rewrite eq_option_alt. intro e.
 rewrite <- find_mapsto_iff, remove_mapsto_iff; now intuition.
 Qed.
+#[local]
 Hint Resolve remove_eq_o : map.
 
 Lemma remove_neq_o : forall m x y,
@@ -412,6 +415,7 @@ Proof.
 intros. rewrite eq_option_alt. intro e.
 rewrite <- find_mapsto_iff, remove_neq_mapsto_iff; now intuition.
 Qed.
+#[local]
 Hint Resolve remove_neq_o : map.
 
 Lemma remove_o : forall m x y,
@@ -1100,6 +1104,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   contradict Hnotin; rewrite <- Hnotin; exists e0; auto.
   Qed.
 
+  #[local]
   Hint Resolve NoDupA_eqk_eqke NoDupA_rev elements_3w : map.
 
   Lemma fold_Equal : forall m1 m2 i, Equal m1 m2 ->
@@ -1232,6 +1237,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   Proof.
   intros; rewrite cardinal_Empty; auto.
   Qed.
+  #[local]
   Hint Resolve cardinal_inv_1 : map.
 
   Lemma cardinal_inv_2 :
@@ -1846,6 +1852,7 @@ Module OrdProperties (M:S).
    unfold leb; f_equal; apply gtb_compat; auto.
   Qed.
 
+  #[local]
   Hint Resolve gtb_compat leb_compat elements_3 : map.
 
   Lemma elements_split : forall p m,
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v
index 03e8d270e9..d26510ab9d 100644
--- a/theories/FSets/FMapFullAVL.v
+++ b/theories/FSets/FMapFullAVL.v
@@ -63,6 +63,7 @@ Inductive avl : t elt -> Prop :=
 
 (** * Automation and dedicated tactics about [avl]. *)
 
+#[local]
 Hint Constructors avl : core.
 
 Lemma height_non_negative : forall (s : t elt), avl s ->
@@ -100,6 +101,7 @@ Lemma avl_node : forall x e l r, avl l -> avl r ->
 Proof.
   intros; auto.
 Qed.
+#[local]
 Hint Resolve avl_node : core.
 
 (** Results about [height] *)
@@ -193,6 +195,7 @@ Lemma add_avl : forall m x e, avl m -> avl (add x e m).
 Proof.
  intros; generalize (add_avl_1 x e H); intuition.
 Qed.
+#[local]
 Hint Resolve add_avl : core.
 
 (** * Extraction of minimum binding *)
@@ -274,6 +277,7 @@ Lemma remove_avl : forall m x, avl m -> avl (remove x m).
 Proof.
  intros; generalize (remove_avl_1 x H); intuition.
 Qed.
+#[local]
 Hint Resolve remove_avl : core.
 
 
@@ -331,6 +335,7 @@ Lemma join_avl : forall l x d r, avl l -> avl r -> avl (join l x d r).
 Proof.
  intros; destruct (join_avl_1 x d H H0); auto.
 Qed.
+#[local]
 Hint Resolve join_avl : core.
 
 (** concat *)
@@ -341,6 +346,7 @@ Proof.
  intros; apply join_avl; auto.
  generalize (remove_min_avl H0); rewrite e1; simpl; auto.
 Qed.
+#[local]
 Hint Resolve concat_avl : core.
 
 (** split *)
@@ -355,6 +361,7 @@ Proof.
 Qed.
 
 End Elt.
+#[global]
 Hint Constructors avl : core.
 
 Section Map.
@@ -714,6 +721,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
   Proof.
    destruct c; simpl; intros; MX.elim_comp; auto with ordered_type.
   Qed.
+  #[global]
   Hint Resolve cons_Cmp : core.
 
   Lemma compare_aux_Cmp : forall e,
diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v
index ab87ba9722..77ce76721e 100644
--- a/theories/FSets/FMapInterface.v
+++ b/theories/FSets/FMapInterface.v
@@ -58,6 +58,7 @@ Definition Cmp (elt:Type)(cmp:elt->elt->bool) e1 e2 := cmp e1 e2 = true.
 Module Type WSfun (E : DecidableType).
 
   Definition key := E.t.
+  #[global]
   Hint Transparent key : core.
 
   Parameter t : Type -> Type.
@@ -243,9 +244,11 @@ Module Type WSfun (E : DecidableType).
 	(x:key)(f:option elt->option elt'->option elt''),
         In x (map2 f m m') -> In x m \/ In x m'.
 
+  #[global]
   Hint Immediate MapsTo_1 mem_2 is_empty_2
     map_2 mapi_2 add_3 remove_3 find_2
     : map.
+  #[global]
   Hint Resolve mem_1 is_empty_1 is_empty_2 add_1 add_2 remove_1
     remove_2 find_1 fold_1 map_1 mapi_1 mapi_2
     : map.
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index a5c00189c4..204e8d0199 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -51,6 +51,7 @@ Proof.
  intro abs.
  inversion abs.
 Qed.
+#[local]
 Hint Resolve empty_1 : core.
 
 Lemma empty_sorted : Sort empty.
@@ -216,6 +217,7 @@ Proof.
  compute in H0,H1.
  simpl; case (X.compare x x''); intuition.
 Qed.
+#[local]
 Hint Resolve add_Inf : core.
 
 Lemma add_sorted : forall m (Hm:Sort m) x e, Sort (add x e m).
@@ -302,6 +304,7 @@ Proof.
  inversion_clear Hm.
  apply Inf_lt with (x'',e''); auto.
 Qed.
+#[local]
 Hint Resolve remove_Inf : core.
 
 Lemma remove_sorted : forall m (Hm:Sort m) x, Sort (remove x m).
@@ -586,6 +589,7 @@ Proof.
  inversion_clear H; auto.
 Qed.
 
+#[local]
 Hint Resolve map_lelistA : core.
 
 Lemma map_sorted : forall (m: t elt)(Hm : sort (@ltk elt) m)(f:elt -> elt'),
@@ -655,6 +659,7 @@ Proof.
  inversion_clear H; auto.
 Qed.
 
+#[local]
 Hint Resolve mapi_lelistA : core.
 
 Lemma mapi_sorted : forall m (Hm : sort (@ltk elt) m)(f: key ->elt -> elt'),
@@ -782,6 +787,7 @@ Proof.
  inversion_clear H; auto.
  inversion_clear H0; auto.
 Qed.
+#[local]
 Hint Resolve combine_lelistA : core.
 
 Lemma combine_sorted :
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index c4bb67a52c..78e7ab69d8 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -49,6 +49,7 @@ Proof.
  inversion abs.
 Qed.
 
+#[local]
 Hint Resolve empty_1 : core.
 
 Lemma empty_NoDup : NoDupA empty.
@@ -621,6 +622,7 @@ Proof.
  inversion_clear 1.
  intros; apply add_NoDup; auto.
 Qed.
+#[local]
 Hint Resolve fold_right_pair_NoDup : core.
 
 Lemma combine_NoDup :
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index 73021a84a3..4917fcb5fd 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -137,6 +137,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
     generalize (E.eq_sym H0); case (Pdec x); case (Pdec y); firstorder.
   Qed.
 
+  #[global]
   Hint Resolve compat_P_aux : core.
 
   Definition filter :
@@ -467,6 +468,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
   Proof.
     intros; unfold elements; case (M.elements s); firstorder.
   Qed.
+  #[global]
   Hint Resolve elements_3 : core.
 
   Lemma elements_3w : forall s : t, NoDupA E.eq (elements s).
@@ -666,6 +668,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
       rewrite <- H1; firstorder.
   Qed.
 
+  #[global]
   Hint Resolve compat_P_aux : core.
 
   Definition filter (f : elt -> bool) (s : t) : t :=
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index 8a217a752a..d597c0404a 100644
--- a/theories/FSets/FSetDecide.v
+++ b/theories/FSets/FSetDecide.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 FSet_elt_Prop FSet_Prop : FSet_Prop.
     Ltac discard_nonFSet :=
       repeat (
@@ -518,6 +519,7 @@ the above form:
 
     (** The hint database [FSet_decidability] will be given to
         the [push_neg] tactic from the module [Negation]. *)
+    #[global]
     Hint Resolve dec_In dec_eq : FSet_decidability.
 
     (** ** Normalizing Propositions About Equality
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index ac08351ad9..7618880bd2 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -460,9 +460,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/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index dfe22b7831..848c27cba1 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -253,13 +253,16 @@ Module Type WSfun (E : DecidableType).
 
   End Spec.
 
+  #[global]
   Hint Transparent elt : core.
+  #[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
@@ -336,7 +339,9 @@ Module Type Sfun (E : OrderedType).
 
   End Spec.
 
+  #[global]
   Hint Resolve elements_3 : set.
+  #[global]
   Hint Immediate
     min_elt_1 min_elt_2 min_elt_3 max_elt_1 max_elt_2 max_elt_3 : set.
 
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 98b445580b..af034bbdd5 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -21,7 +21,9 @@ Require Import DecidableTypeEx FSetFacts FSetDecide.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+#[global]
 Hint Unfold transpose compat_op Proper respectful : fset.
+#[global]
 Hint Extern 1 (Equivalence _) => constructor; congruence : fset.
 
 (** First, a functor for Weak Sets in functorial version. *)
@@ -269,7 +271,9 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun 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
@@ -732,6 +736,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
   Proof.
   intros; rewrite cardinal_Empty; auto.
   Qed.
+  #[global]
   Hint Resolve cardinal_inv_1 : fset.
 
   Lemma cardinal_inv_2 :
@@ -769,6 +774,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
   exact Equal_cardinal.
   Qed.
 
+  #[global]
   Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal : fset.
 
   (** ** Cardinal and set operators *)
@@ -778,6 +784,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
   rewrite cardinal_fold; apply fold_1; auto with set fset.
   Qed.
 
+  #[global]
   Hint Immediate empty_cardinal cardinal_1 : set.
 
   Lemma singleton_cardinal : forall x, cardinal (singleton x) = 1.
@@ -788,6 +795,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
   apply cardinal_2 with x; auto with set.
   Qed.
 
+  #[global]
   Hint Resolve singleton_cardinal: set.
 
   Lemma diff_inter_cardinal :
@@ -887,6 +895,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
   auto with set fset.
   Qed.
 
+  #[global]
   Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2 : fset.
 
 End WProperties_fun.
@@ -952,6 +961,7 @@ Module OrdProperties (M:S).
    red; intros x a b H; unfold leb.
    f_equal; apply gtb_compat; auto.
   Qed.
+  #[global]
   Hint Resolve gtb_compat leb_compat : fset.
 
   Lemma elements_split : forall x s,