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

diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v
index 0c3bd9393b..c923b503a7 100644
--- a/theories/Structures/DecidableType.v
+++ b/theories/Structures/DecidableType.v
@@ -38,7 +38,9 @@ Module KeyDecidableType(D:DecidableType).
   Definition eqke (p p':key*elt) :=
           eq (fst p) (fst p') /\ (snd p) = (snd p').
 
+  #[local]
   Hint Unfold eqk eqke : core.
+  #[local]
   Hint Extern 2 (eqke ?a ?b) => split : core.
 
    (* eqke is stricter than eqk *)
@@ -70,7 +72,9 @@ Module KeyDecidableType(D:DecidableType).
     unfold eqke; intuition; [ eauto | congruence ].
   Qed.
 
+  #[local]
   Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core.
+  #[local]
   Hint Immediate eqk_sym eqke_sym : core.
 
   Global Instance eqk_equiv : Equivalence eqk.
@@ -84,6 +88,7 @@ Module KeyDecidableType(D:DecidableType).
   Proof.
     unfold eqke; induction 1; intuition. 
   Qed.
+  #[local]
   Hint Resolve InA_eqke_eqk : core.
 
   Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m.
@@ -94,6 +99,7 @@ Module KeyDecidableType(D:DecidableType).
   Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
   Definition In k m := exists e:elt, MapsTo k e m.
 
+  #[local]
   Hint Unfold MapsTo In : core.
 
   (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *)
@@ -140,12 +146,19 @@ Module KeyDecidableType(D:DecidableType).
 
  End Elt.
 
+ #[global]
  Hint Unfold eqk eqke : core.
+ #[global]
  Hint Extern 2 (eqke ?a ?b) => split : core.
+ #[global]
  Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core.
+ #[global]
  Hint Immediate eqk_sym eqke_sym : core.
+ #[global]
  Hint Resolve InA_eqke_eqk : core.
+ #[global]
  Hint Unfold MapsTo In : core.
+ #[global]
  Hint Resolve In_inv_2 In_inv_3 : core.
 
 End KeyDecidableType.
diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v
index 914361d718..7cd5943a3f 100644
--- a/theories/Structures/Equalities.v
+++ b/theories/Structures/Equalities.v
@@ -53,7 +53,9 @@ Module Type IsEqOrig (Import E:Eq').
   Axiom eq_refl : forall x : t, x==x.
   Axiom eq_sym : forall x y : t, x==y -> y==x.
   Axiom eq_trans : forall x y z : t, x==y -> y==z -> x==z.
+  #[global]
   Hint Immediate eq_sym : core.
+  #[global]
   Hint Resolve eq_refl eq_trans : core.
 End IsEqOrig.
 
diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v
index fe9794de8a..523240065d 100644
--- a/theories/Structures/EqualitiesFacts.v
+++ b/theories/Structures/EqualitiesFacts.v
@@ -22,6 +22,7 @@ Module KeyDecidableType(D:DecidableType).
  Definition eqk {elt} : relation (key*elt) := D.eq @@1.
  Definition eqke {elt} : relation (key*elt) := D.eq * Logic.eq.
 
+ #[global]
  Hint Unfold eqk eqke : core.
 
  (** eqk, eqke are equalities *)
@@ -60,6 +61,7 @@ Module KeyDecidableType(D:DecidableType).
  Lemma eqk_1 {elt} k k' (e e':elt) : eqk (k,e) (k',e') -> D.eq k k'.
  Proof. trivial. Qed.
 
+ #[global]
  Hint Resolve eqke_1 eqke_2 eqk_1 : core.
 
  (* Additional facts *)
@@ -69,6 +71,7 @@ Module KeyDecidableType(D:DecidableType).
  Proof.
   induction 1; firstorder.
  Qed.
+ #[global]
  Hint Resolve InA_eqke_eqk : core.
 
  Lemma InA_eqk_eqke {elt} p (m:list (key*elt)) :
@@ -86,6 +89,7 @@ Module KeyDecidableType(D:DecidableType).
  Definition MapsTo {elt} (k:key)(e:elt):= InA eqke (k,e).
  Definition In {elt} k m := exists e:elt, MapsTo k e m.
 
+ #[global]
  Hint Unfold MapsTo In : core.
 
  (* Alternative formulations for [In k l] *)
@@ -167,8 +171,11 @@ Module KeyDecidableType(D:DecidableType).
   eauto with *.
  Qed.
 
+ #[global]
  Hint Extern 2 (eqke ?a ?b) => split : core.
+ #[global]
  Hint Resolve InA_eqke_eqk : core.
+ #[global]
  Hint Resolve In_inv_2 In_inv_3 : core.
 
 End KeyDecidableType.
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index ecf0706a4f..dc7a48cd6b 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -44,7 +44,9 @@ Module Type MiniOrderedType.
 
   Parameter compare : forall x y : t, Compare lt eq x y.
 
+  #[global]
   Hint Immediate eq_sym : ordered_type.
+  #[global]
   Hint Resolve eq_refl eq_trans lt_not_eq lt_trans : ordered_type.
 
 End MiniOrderedType.
@@ -144,8 +146,11 @@ Module OrderedTypeFacts (Import O: OrderedType).
   Lemma eq_not_gt x y : eq x y -> ~ lt y x. Proof. order. Qed.
   Lemma lt_not_gt x y : lt x y -> ~ lt y x. Proof. order. Qed.
 
+  #[global]
   Hint Resolve gt_not_eq eq_not_lt : ordered_type.
+  #[global]
   Hint Immediate eq_lt lt_eq le_eq eq_le neq_eq eq_neq : ordered_type.
+  #[global]
   Hint Resolve eq_not_gt lt_antirefl lt_not_gt : ordered_type.
 
   Lemma elim_compare_eq :
@@ -248,7 +253,9 @@ Proof. exact (SortA_NoDupA eq_equiv lt_strorder lt_compat). Qed.
 
 End ForNotations.
 
+#[global]
 Hint Resolve ListIn_In Sort_NoDup Inf_lt : ordered_type.
+#[global]
 Hint Immediate In_eq Inf_lt : ordered_type.
 
 End OrderedTypeFacts.
@@ -267,7 +274,9 @@ Module KeyOrderedType(O:OrderedType).
           eq (fst p) (fst p') /\ (snd p) = (snd p').
   Definition ltk (p p':key*elt) := lt (fst p) (fst p').
 
+  #[local]
   Hint Unfold eqk eqke ltk : ordered_type.
+  #[local]
   Hint Extern 2 (eqke ?a ?b) => split : ordered_type.
 
    (* eqke is stricter than eqk *)
@@ -284,6 +293,7 @@ Module KeyOrderedType(O:OrderedType).
 
    Lemma ltk_right_l : forall x k e e', ltk (k,e) x -> ltk (k,e') x.
    Proof. auto. Qed.
+  #[local]
    Hint Immediate ltk_right_r ltk_right_l : ordered_type.
 
   (* eqk, eqke are equalities, ltk is a strict order *)
@@ -320,8 +330,11 @@ Module KeyOrderedType(O:OrderedType).
     exact (lt_not_eq H H1).
   Qed.
 
+  #[local]
   Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : ordered_type.
+  #[local]
   Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : ordered_type.
+  #[local]
   Hint Immediate eqk_sym eqke_sym : ordered_type.
 
   Global Instance eqk_equiv : Equivalence eqk.
@@ -360,7 +373,9 @@ Module KeyOrderedType(O:OrderedType).
       intros (k,e) (k',e') (k'',e'').
       unfold ltk, eqk; simpl; eauto with ordered_type.
   Qed.
+  #[local]
   Hint Resolve eqk_not_ltk : ordered_type.
+  #[local]
   Hint Immediate ltk_eqk eqk_ltk : ordered_type.
 
   Lemma InA_eqke_eqk :
@@ -368,6 +383,7 @@ Module KeyOrderedType(O:OrderedType).
   Proof.
     unfold eqke; induction 1; intuition.
   Qed.
+  #[local]
   Hint Resolve InA_eqke_eqk : ordered_type.
 
   Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
@@ -375,6 +391,7 @@ Module KeyOrderedType(O:OrderedType).
   Notation Sort := (sort ltk).
   Notation Inf := (lelistA ltk).
 
+  #[local]
   Hint Unfold MapsTo In : ordered_type.
 
   (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *)
@@ -406,7 +423,9 @@ Module KeyOrderedType(O:OrderedType).
   Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l.
   Proof. exact (InfA_ltA ltk_strorder). Qed.
 
+  #[local]
   Hint Immediate Inf_eq : ordered_type.
+  #[local]
   Hint Resolve Inf_lt : ordered_type.
 
   Lemma Sort_Inf_In :
@@ -470,18 +489,31 @@ Module KeyOrderedType(O:OrderedType).
 
  End Elt.
 
+ #[global]
  Hint Unfold eqk eqke ltk : ordered_type.
+ #[global]
  Hint Extern 2 (eqke ?a ?b) => split : ordered_type.
+ #[global]
  Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : ordered_type.
+ #[global]
  Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : ordered_type.
+ #[global]
  Hint Immediate eqk_sym eqke_sym : ordered_type.
+ #[global]
  Hint Resolve eqk_not_ltk : ordered_type.
+ #[global]
  Hint Immediate ltk_eqk eqk_ltk : ordered_type.
+ #[global]
  Hint Resolve InA_eqke_eqk : ordered_type.
+ #[global]
  Hint Unfold MapsTo In : ordered_type.
+ #[global]
  Hint Immediate Inf_eq : ordered_type.
+ #[global]
  Hint Resolve Inf_lt : ordered_type.
+ #[global]
  Hint Resolve Sort_Inf_NotIn : ordered_type.
+ #[global]
  Hint Resolve In_inv_2 In_inv_3 : ordered_type.
 
 End KeyOrderedType.
diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v
index b3e3b6e853..b4ddd0b262 100644
--- a/theories/Structures/Orders.v
+++ b/theories/Structures/Orders.v
@@ -181,6 +181,7 @@ Module OTF_to_TotalOrder (O:OrderedTypeFull) <: TotalOrder
     we coerce [bool] into [Prop]. *)
 
 Local Coercion is_true : bool >-> Sortclass.
+#[global]
 Hint Unfold is_true : core.
 
 Module Type HasLeb (Import T:Typ).
diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v
index 3a5dbc2f88..bace70cbee 100644
--- a/theories/Structures/OrdersLists.v
+++ b/theories/Structures/OrdersLists.v
@@ -50,7 +50,9 @@ Proof. exact (InfA_alt O.eq_equiv O.lt_strorder O.lt_compat). Qed.
 Lemma Sort_NoDup : forall l, Sort l -> NoDup l.
 Proof. exact (SortA_NoDupA O.eq_equiv O.lt_strorder O.lt_compat) . Qed.
 
+#[global]
 Hint Resolve ListIn_In Sort_NoDup Inf_lt : core.
+#[global]
 Hint Immediate In_eq Inf_lt : core.
 
 End OrderedTypeLists.
@@ -66,6 +68,7 @@ Module KeyOrderedType(O:OrderedType).
 
  Definition ltk {elt} : relation (key*elt) := O.lt @@1.
 
+ #[global]
  Hint Unfold ltk : core.
 
  (* ltk is a strict order *)
@@ -109,7 +112,9 @@ Module KeyOrderedType(O:OrderedType).
   Lemma Inf_lt l x x' : ltk x x' -> Inf x' l -> Inf x l.
   Proof. apply InfA_ltA; auto with *. Qed.
 
+  #[local]
   Hint Immediate Inf_eq : core.
+  #[local]
   Hint Resolve Inf_lt : core.
 
   Lemma Sort_Inf_In l p q : Sort l -> Inf q l -> InA eqk p l -> ltk q p.
@@ -148,9 +153,13 @@ Module KeyOrderedType(O:OrderedType).
 
  End Elt.
 
+ #[global]
  Hint Resolve ltk_not_eqk ltk_not_eqke : core.
+ #[global]
  Hint Immediate Inf_eq : core.
+ #[global]
  Hint Resolve Inf_lt : core.
+ #[global]
  Hint Resolve Sort_Inf_NotIn : core.
 
 End KeyOrderedType.