Explicitly annotate all hint declarations of the standard library.

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

4 files changed, 41 insertions, 0 deletions

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 4cc3597029..115c7cb365 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -163,6 +163,7 @@ Section Facts.
   Proof.
      auto using app_assoc.
   Qed.
+  #[local]
   Hint Resolve app_assoc_reverse : core.
   (* end hide *)
 
@@ -385,10 +386,15 @@ Section Facts.
 
 End Facts.
 
+#[global]
 Hint Resolve app_assoc app_assoc_reverse: datatypes.
+#[global]
 Hint Resolve app_comm_cons app_cons_not_nil: datatypes.
+#[global]
 Hint Immediate app_eq_nil: datatypes.
+#[global]
 Hint Resolve app_eq_unit app_inj_tail: datatypes.
+#[global]
 Hint Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app: datatypes.
 
 
@@ -1928,6 +1934,7 @@ Section length_order.
   Qed.
 End length_order.
 
+#[global]
 Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons:
   datatypes.
 
@@ -1941,6 +1948,7 @@ Section SetIncl.
   Variable A : Type.
 
   Definition incl (l m:list A) := forall a:A, In a l -> In a m.
+  #[local]
   Hint Unfold incl : core.
 
   Lemma incl_nil_l : forall l, incl nil l.
@@ -1959,12 +1967,14 @@ Section SetIncl.
   Proof.
     auto.
   Qed.
+  #[local]
   Hint Resolve incl_refl : core.
 
   Lemma incl_tl : forall (a:A) (l m:list A), incl l m -> incl l (a :: m).
   Proof.
     auto with datatypes.
   Qed.
+  #[local]
   Hint Immediate incl_tl : core.
 
   Lemma incl_tran : forall l m n:list A, incl l m -> incl m n -> incl l n.
@@ -1976,12 +1986,14 @@ Section SetIncl.
   Proof.
     auto with datatypes.
   Qed.
+  #[local]
   Hint Immediate incl_appl : core.
 
   Lemma incl_appr : forall l m n:list A, incl l n -> incl l (m ++ n).
   Proof.
     auto with datatypes.
   Qed.
+  #[local]
   Hint Immediate incl_appr : core.
 
   Lemma incl_cons :
@@ -1997,6 +2009,7 @@ Section SetIncl.
     now_show (In a0 l -> In a0 m).
     auto.
   Qed.
+  #[local]
   Hint Resolve incl_cons : core.
 
   Lemma incl_cons_inv : forall (a:A) (l m:list A),
@@ -2012,6 +2025,7 @@ Section SetIncl.
     now_show (In a n).
     elim (in_app_or _ _ _ H1); auto.
   Qed.
+  #[local]
   Hint Resolve incl_app : core.
 
   Lemma incl_app_app : forall l1 l2 m1 m2:list A,
@@ -2054,6 +2068,7 @@ Proof.
   apply in_map; intuition.
 Qed.
 
+#[global]
 Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons
   incl_app incl_map: datatypes.
 
@@ -2738,6 +2753,7 @@ Section Exists_Forall.
       | Exists_cons_hd : forall x l, P x -> Exists (x::l)
       | Exists_cons_tl : forall x l, Exists l -> Exists (x::l).
 
+    #[local]
     Hint Constructors Exists : core.
 
     Lemma Exists_exists (l:list A) :
@@ -2815,6 +2831,7 @@ Section Exists_Forall.
       | Forall_nil : Forall nil
       | Forall_cons : forall x l, P x -> Forall l -> Forall (x::l).
 
+    #[local]
     Hint Constructors Forall : core.
 
     Lemma Forall_forall (l:list A):
@@ -2999,7 +3016,9 @@ Section Exists_Forall.
 
 End Exists_Forall.
 
+#[global]
 Hint Constructors Exists : core.
+#[global]
 Hint Constructors Forall : core.
 
 Lemma exists_Forall A B : forall (P : A -> B -> Prop) l,
@@ -3064,6 +3083,7 @@ Section Forall2.
     | Forall2_cons : forall x y l l',
       R x y -> Forall2 l l' -> Forall2 (x::l) (y::l').
 
+  #[local]
   Hint Constructors Forall2 : core.
 
   Theorem Forall2_refl : Forall2 [] [].
@@ -3098,6 +3118,7 @@ Section Forall2.
   Qed.
 End Forall2.
 
+#[global]
 Hint Constructors Forall2 : core.
 
 Section ForallPairs.
@@ -3119,6 +3140,7 @@ Section ForallPairs.
     | FOP_cons : forall a l,
       Forall (R a) l -> ForallOrdPairs l -> ForallOrdPairs (a::l).
 
+  #[local]
   Hint Constructors ForallOrdPairs : core.
 
   Lemma ForallOrdPairs_In : forall l,
@@ -3344,6 +3366,7 @@ Notation rev_acc := rev_append (only parsing).
 Notation rev_acc_rev := rev_append_rev (only parsing).
 Notation AllS := Forall (only parsing). (* was formerly in TheoryList *)
 
+#[global]
 Hint Resolve app_nil_end : datatypes.
 (* end hide *)
 
diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index 7f5148d0dd..458d08ccb9 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -193,6 +193,7 @@ Section first_definitions.
      | auto with datatypes ].
   Qed.
 
+  #[local]
   Hint Resolve set_add_intro1 set_add_intro2 : core.
 
   Lemma set_add_intro :
@@ -224,6 +225,7 @@ Section first_definitions.
    case H1; trivial.
    Qed.
 
+  #[local]
   Hint Resolve set_add_intro set_add_elim set_add_elim2 : core.
 
   Lemma set_add_not_empty : forall (a:A) (x:set), set_add a x <> empty_set.
@@ -310,6 +312,7 @@ Section first_definitions.
     intros; elim H0; auto with datatypes.
   Qed.
 
+  #[local]
   Hint Resolve set_union_intro2 set_union_intro1 : core.
 
   Lemma set_union_intro :
@@ -393,6 +396,7 @@ Section first_definitions.
     eauto with datatypes.
   Qed.
 
+  #[local]
   Hint Resolve set_inter_elim1 set_inter_elim2 : core.
 
   Lemma set_inter_elim :
@@ -471,6 +475,7 @@ Section first_definitions.
   apply (set_diff_elim1 _ _ _ H).
   Qed.
 
+#[local]
 Hint Resolve set_diff_intro set_diff_trivial : core.
 
 
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index 48e9f992fd..826815410a 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -30,6 +30,7 @@ Inductive InA (x : A) : list A -> Prop :=
   | InA_cons_hd : forall y l, eqA x y -> InA x (y :: l)
   | InA_cons_tl : forall y l, InA x l -> InA x (y :: l).
 
+#[local]
 Hint Constructors InA : core.
 
 (** TODO: it would be nice to have a generic definition instead
@@ -62,6 +63,7 @@ Inductive NoDupA : list A -> Prop :=
   | NoDupA_nil : NoDupA nil
   | NoDupA_cons : forall x l, ~ InA x l -> NoDupA l -> NoDupA (x::l).
 
+#[local]
 Hint Constructors NoDupA : core.
 
 (** An alternative definition of [NoDupA] based on [ForallOrdPairs] *)
@@ -84,6 +86,7 @@ Definition equivlistA l l' := forall x, InA x l <-> InA x l'.
 
 Lemma incl_nil l : inclA nil l.
 Proof. intro. intros. inversion H. Qed.
+#[local]
 Hint Resolve incl_nil : list.
 
 (** lists with same elements modulo [eqA] at the same place *)
@@ -93,6 +96,7 @@ Inductive eqlistA : list A -> list A -> Prop :=
   | eqlistA_cons : forall x x' l l',
       eqA x x' -> eqlistA l l' -> eqlistA (x::l) (x'::l').
 
+#[local]
 Hint Constructors eqlistA : core.
 
 (** We could also have written [eqlistA = Forall2 eqA]. *)
@@ -107,7 +111,9 @@ Definition eqarefl := (@Equivalence_Reflexive _ _ eqA_equiv).
 Definition eqatrans := (@Equivalence_Transitive _ _ eqA_equiv).
 Definition eqasym := (@Equivalence_Symmetric _ _ eqA_equiv).
  
+#[local]
 Hint Resolve eqarefl eqatrans : core.
+#[local]
 Hint Immediate eqasym : core.
 
 Ltac inv := invlist InA; invlist sort; invlist lelistA; invlist NoDupA.
@@ -154,6 +160,7 @@ Lemma InA_eqA : forall l x y, eqA x y -> InA x l -> InA y l.
 Proof.
  intros l x y H H'. rewrite <- H. auto.
 Qed.
+#[local]
 Hint Immediate InA_eqA : core.
 
 Lemma In_InA : forall l x, In x l -> InA x l.
@@ -161,6 +168,7 @@ Proof.
  simple induction l; simpl; intuition.
  subst; auto.
 Qed.
+#[local]
 Hint Resolve In_InA : core.
 
 Lemma InA_split : forall l x, InA x l ->
@@ -786,11 +794,13 @@ Hypothesis ltA_compat : Proper (eqA==>eqA==>iff) ltA.
 
 Let sotrans := (@StrictOrder_Transitive _ _ ltA_strorder).
 
+#[local]
 Hint Resolve sotrans : core.
 
 Notation InfA:=(lelistA ltA).
 Notation SortA:=(sort ltA).
 
+#[local]
 Hint Constructors lelistA sort : core.
 
 Lemma InfA_ltA :
@@ -814,6 +824,7 @@ Lemma InfA_eqA l x y : eqA x y -> InfA y l -> InfA x l.
 Proof using eqA_equiv ltA_compat.
  intros H; now rewrite H.
 Qed.
+#[local]
 Hint Immediate InfA_ltA InfA_eqA : core.
 
 Lemma SortA_InfA_InA :
@@ -1005,6 +1016,7 @@ Qed.
 End Filter.
 End Type_with_equality.
 
+#[global]
 Hint Constructors InA eqlistA NoDupA sort lelistA : core.
 
 Arguments equivlistA_cons_nil {A} eqA {eqA_equiv} x l _.
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index 7a275a8231..f16d70a4c2 100644
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -54,6 +54,7 @@ Lemma tl_nth_tl :
 Proof.
   simple induction n; simpl; auto.
 Qed.
+#[local]
 Hint Resolve tl_nth_tl: datatypes.
 
 Lemma Str_nth_tl_plus :