Explicitly annotate all hint declarations of the standard library.

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

18 files changed, 72 insertions, 0 deletions

diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v
index 68d200e189..430f35eecb 100644
--- a/theories/Sets/Classical_sets.v
+++ b/theories/Sets/Classical_sets.v
@@ -77,6 +77,7 @@ Section Ensembles_classical.
   Proof.
     unfold Subtract at 1; auto with sets.
   Qed.
+  #[local]
   Hint Resolve Subtract_intro : sets.
 
   Lemma Subtract_inv :
@@ -123,5 +124,6 @@ Section Ensembles_classical.
 
 End Ensembles_classical.
 
+ #[global]
  Hint Resolve Strict_super_set_contains_new_element Subtract_intro
   not_SIncl_empty: sets.
diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v
index 5027679266..ae7cdc9a0f 100644
--- a/theories/Sets/Constructive_sets.v
+++ b/theories/Sets/Constructive_sets.v
@@ -140,6 +140,7 @@ Section Ensembles_facts.
 
 End Ensembles_facts.
 
+#[global]
 Hint Resolve Singleton_inv Singleton_intro Add_intro1 Add_intro2
   Intersection_inv Couple_inv Setminus_intro Strict_Included_intro
   Strict_Included_strict Noone_in_empty Inhabited_not_empty Add_not_Empty
diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v
index face010746..581c16778d 100644
--- a/theories/Sets/Cpo.v
+++ b/theories/Sets/Cpo.v
@@ -92,6 +92,7 @@ Section Bounds.
       exists bsup : _, Lub X bsup) -> Conditionally_complete.
 End Bounds.
 
+#[global]
 Hint Resolve Totally_ordered_definition Upper_Bound_definition
   Lower_Bound_definition Lub_definition Glb_definition Bottom_definition
   Definition_of_Complete Definition_of_Complete
diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v
index fb33f7834c..96fb070071 100644
--- a/theories/Sets/Ensembles.v
+++ b/theories/Sets/Ensembles.v
@@ -92,8 +92,10 @@ Section Ensembles.
 
 End Ensembles.
 
+#[global]
 Hint Unfold In Included Same_set Strict_Included Add Setminus Subtract: sets.
 
+#[global]
 Hint Resolve Union_introl Union_intror Intersection_intro In_singleton
   Couple_l Couple_r Triple_l Triple_m Triple_r Disjoint_intro
   Extensionality_Ensembles: sets.
diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v
index e8e2a66e98..683979be74 100644
--- a/theories/Sets/Finite_sets.v
+++ b/theories/Sets/Finite_sets.v
@@ -45,7 +45,9 @@ Section Ensembles_finis.
 
 End Ensembles_finis.
 
+#[global]
 Hint Resolve Empty_is_finite Union_is_finite: sets.
+#[global]
 Hint Resolve card_empty card_add: sets.
 
 Require Import Constructive_sets.
diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v
index 023eeaac9d..e83ff223f3 100644
--- a/theories/Sets/Image.v
+++ b/theories/Sets/Image.v
@@ -202,4 +202,5 @@ Section Image.
 
 End Image.
 
+#[global]
 Hint Resolve Im_def image_empty finite_image: sets.
diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v
index b3d7ed0b7b..766f62af45 100644
--- a/theories/Sets/Infinite_sets.v
+++ b/theories/Sets/Infinite_sets.v
@@ -46,6 +46,7 @@ Section Approx.
     Defn_of_Approximant : Finite U X -> Included U X A -> Approximant A X.
 End Approx.
 
+#[global]
 Hint Resolve Defn_of_Approximant : core.
 
 Section Infinite_sets.
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index 4d0cd1174c..3f3cade37d 100644
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -187,7 +187,10 @@ End multiset_defs.
 
 Unset Implicit Arguments.
 
+#[global]
 Hint Unfold meq multiplicity: datatypes.
+#[global]
 Hint Resolve munion_empty_right munion_comm munion_ass meq_left meq_right
   munion_empty_left: datatypes.
+#[global]
 Hint Immediate meq_sym: datatypes.
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v
index 875afe3f44..879a7df608 100644
--- a/theories/Sets/Partial_Order.v
+++ b/theories/Sets/Partial_Order.v
@@ -53,7 +53,9 @@ Section Partial_orders.
 
 End Partial_orders.
 
+#[global]
 Hint Unfold Carrier_of Rel_of Strict_Rel_of: sets.
+#[global]
 Hint Resolve Definition_of_covers: sets.
 
 
diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v
index 96d04100b9..617836225c 100644
--- a/theories/Sets/Powerset.v
+++ b/theories/Sets/Powerset.v
@@ -38,12 +38,14 @@ Variable U : Type.
 Inductive Power_set (A:Ensemble U) : Ensemble (Ensemble U) :=
     Definition_of_Power_set :
       forall X:Ensemble U, Included U X A -> In (Ensemble U) (Power_set A) X.
+#[local]
 Hint Resolve Definition_of_Power_set : core.
 
 Theorem Empty_set_minimal : forall X:Ensemble U, Included U (Empty_set U) X.
 intro X; red.
 intros x H'; elim H'.
 Qed.
+#[local]
 Hint Resolve Empty_set_minimal : core.
 
 Theorem Power_set_Inhabited :
@@ -51,22 +53,26 @@ Theorem Power_set_Inhabited :
 intro X.
 apply Inhabited_intro with (Empty_set U); auto with sets.
 Qed.
+#[local]
 Hint Resolve Power_set_Inhabited : core.
 
 Theorem Inclusion_is_an_order : Order (Ensemble U) (Included U).
 auto 6 with sets.
 Qed.
+#[local]
 Hint Resolve Inclusion_is_an_order : core.
 
 Theorem Inclusion_is_transitive : Transitive (Ensemble U) (Included U).
 elim Inclusion_is_an_order; auto with sets.
 Qed.
+#[local]
 Hint Resolve Inclusion_is_transitive : core.
 
 Definition Power_set_PO : Ensemble U -> PO (Ensemble U).
 intro A; try assumption.
 apply Definition_of_PO with (Power_set A) (Included U); auto with sets.
 Defined.
+#[local]
 Hint Unfold Power_set_PO : core.
 
 Theorem Strict_Rel_is_Strict_Included :
@@ -74,6 +80,7 @@ Theorem Strict_Rel_is_Strict_Included :
    (Strict_Rel_of (Ensemble U) (Power_set_PO (Full_set U))).
 auto with sets.
 Qed.
+#[local]
 Hint Resolve Strict_Rel_Transitive Strict_Rel_is_Strict_Included : core.
 
 Lemma Strict_inclusion_is_transitive_with_inclusion :
@@ -109,6 +116,7 @@ Theorem Empty_set_is_Bottom :
  forall A:Ensemble U, Bottom (Ensemble U) (Power_set_PO A) (Empty_set U).
 intro A; apply Bottom_definition; simpl; auto with sets.
 Qed.
+#[local]
 Hint Resolve Empty_set_is_Bottom : core.
 
 Theorem Union_minimal :
@@ -117,6 +125,7 @@ Theorem Union_minimal :
 intros a b X H' H'0; red.
 intros x H'1; elim H'1; auto with sets.
 Qed.
+#[local]
 Hint Resolve Union_minimal : core.
 
 Theorem Intersection_maximal :
@@ -144,6 +153,7 @@ Theorem Intersection_decreases_r :
 intros a b; red.
 intros x H'; elim H'; auto with sets.
 Qed.
+#[local]
 Hint Resolve Union_increases_l Union_increases_r Intersection_decreases_l
   Intersection_decreases_r : core.
 
@@ -177,14 +187,25 @@ Qed.
 
 End The_power_set_partial_order.
 
+#[global]
 Hint Resolve Empty_set_minimal: sets.
+#[global]
 Hint Resolve Power_set_Inhabited: sets.
+#[global]
 Hint Resolve Inclusion_is_an_order: sets.
+#[global]
 Hint Resolve Inclusion_is_transitive: sets.
+#[global]
 Hint Resolve Union_minimal: sets.
+#[global]
 Hint Resolve Union_increases_l: sets.
+#[global]
 Hint Resolve Union_increases_r: sets.
+#[global]
 Hint Resolve Intersection_decreases_l: sets.
+#[global]
 Hint Resolve Intersection_decreases_r: sets.
+#[global]
 Hint Resolve Empty_set_is_Bottom: sets.
+#[global]
 Hint Resolve Strict_inclusion_is_transitive: sets.
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v
index b83485bbf3..0fe63c5b66 100644
--- a/theories/Sets/Powerset_Classical_facts.v
+++ b/theories/Sets/Powerset_Classical_facts.v
@@ -92,6 +92,7 @@ Section Sets_as_an_algebra.
     apply Subtract_intro; auto with sets.
     red; intro H'1; apply H'; rewrite H'1; auto with sets.
   Qed.
+  #[local]
   Hint Resolve incl_soustr_add_r: sets.
 
   Lemma add_soustr_2 :
@@ -330,9 +331,15 @@ Section Sets_as_an_algebra.
 
 End Sets_as_an_algebra.
 
+#[global]
 Hint Resolve incl_soustr_in: sets.
+#[global]
 Hint Resolve incl_soustr: sets.
+#[global]
 Hint Resolve incl_soustr_add_l: sets.
+#[global]
 Hint Resolve incl_soustr_add_r: sets.
+#[global]
 Hint Resolve add_soustr_1 add_soustr_2: sets.
+#[global]
 Hint Resolve add_soustr_xy: sets.
diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v
index 69b28f14e4..b21c48d305 100644
--- a/theories/Sets/Powerset_facts.v
+++ b/theories/Sets/Powerset_facts.v
@@ -348,6 +348,7 @@ Section Sets_as_an_algebra.
 
 End Sets_as_an_algebra.
 
+#[global]
 Hint Resolve Empty_set_zero Empty_set_zero' Union_associative Union_add
   singlx incl_add: sets.
 
diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v
index 42755b551f..1167ad36bf 100644
--- a/theories/Sets/Relations_1.v
+++ b/theories/Sets/Relations_1.v
@@ -61,7 +61,9 @@ Section Relations_1.
        Definition_of_PER : Symmetric -> Transitive -> PER.
 
 End Relations_1.
+#[global]
 Hint Unfold Reflexive Transitive Antisymmetric Symmetric contains
   same_relation: sets.
+#[global]
 Hint Resolve Definition_of_preorder Definition_of_order
   Definition_of_equivalence Definition_of_PER: sets.
diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v
index 21fc7ceaf2..6d7b837b63 100644
--- a/theories/Sets/Relations_1_facts.v
+++ b/theories/Sets/Relations_1_facts.v
@@ -52,6 +52,7 @@ apply Definition_of_equivalence.
   split; apply H'1 with y; auto 10 with sets.
 - red; intros x y h; elim h; intros H'3 H'4; auto 10 with sets.
 Qed.
+#[global]
 Hint Resolve Equiv_from_preorder : core.
 
 Theorem Equiv_from_order :
@@ -60,6 +61,7 @@ Theorem Equiv_from_order :
 Proof.
 intros U R H'; elim H'; auto 10 with sets.
 Qed.
+#[global]
 Hint Resolve Equiv_from_order : core.
 
 Theorem contains_is_preorder :
@@ -67,6 +69,7 @@ Theorem contains_is_preorder :
 Proof.
 auto 10 with sets.
 Qed.
+#[global]
 Hint Resolve contains_is_preorder : core.
 
 Theorem same_relation_is_equivalence :
@@ -74,6 +77,7 @@ Theorem same_relation_is_equivalence :
 Proof.
 unfold same_relation at 1; auto 10 with sets.
 Qed.
+#[global]
 Hint Resolve same_relation_is_equivalence : core.
 
 Theorem cong_reflexive_same_relation :
diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v
index 5e3206dd9b..e180798d1f 100644
--- a/theories/Sets/Relations_2.v
+++ b/theories/Sets/Relations_2.v
@@ -50,7 +50,11 @@ Definition Strongly_confluent : Prop :=
 
 End Relations_2.
 
+#[global]
 Hint Resolve Rstar_0: sets.
+#[global]
 Hint Resolve Rstar1_0: sets.
+#[global]
 Hint Resolve Rstar1_1: sets.
+#[global]
 Hint Resolve Rplus_0: sets.
diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v
index 9ebbba485c..d5c4040033 100644
--- a/theories/Sets/Relations_3.v
+++ b/theories/Sets/Relations_3.v
@@ -53,10 +53,16 @@ Section Relations_3.
    Definition Noetherian : Prop := forall x:U, noetherian x.
 
 End Relations_3.
+#[global]
 Hint Unfold coherent: sets.
+#[global]
 Hint Unfold locally_confluent: sets.
+#[global]
 Hint Unfold confluent: sets.
+#[global]
 Hint Unfold Confluent: sets.
+#[global]
 Hint Resolve definition_of_noetherian: sets.
+#[global]
 Hint Unfold Noetherian: sets.
 
diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v
index db51186ef1..9f4869a625 100644
--- a/theories/Sets/Relations_3_facts.v
+++ b/theories/Sets/Relations_3_facts.v
@@ -38,6 +38,7 @@ Proof.
 intros U R x y H'; red.
 exists y; auto with sets.
 Qed.
+#[global]
 Hint Resolve Rstar_imp_coherent : core.
 
 Theorem coherent_symmetric :
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
index 474b417e8e..d8fe7f6dbe 100644
--- a/theories/Sets/Uniset.v
+++ b/theories/Sets/Uniset.v
@@ -41,20 +41,24 @@ Definition Singleton (a:A) :=
        end).
 
 Definition In (s:uniset) (a:A) : Prop := charac s a = true.
+#[local]
 Hint Unfold In : core.
 
 (** uniset inclusion *)
 Definition incl (s1 s2:uniset) := forall a:A, Bool.le (charac s1 a) (charac s2 a).
+#[local]
 Hint Unfold incl : core.
 
 (** uniset equality *)
 Definition seq (s1 s2:uniset) := forall a:A, charac s1 a = charac s2 a.
+#[local]
 Hint Unfold seq : core.
 
 Lemma le_refl : forall b, Bool.le b b.
 Proof.
 destruct b; simpl; auto.
 Qed.
+#[local]
 Hint Resolve le_refl : core.
 
 Lemma incl_left : forall s1 s2:uniset, seq s1 s2 -> incl s1 s2.
@@ -71,6 +75,7 @@ Lemma seq_refl : forall x:uniset, seq x x.
 Proof.
 destruct x; unfold seq; auto.
 Qed.
+#[local]
 Hint Resolve seq_refl : core.
 
 Lemma seq_trans : forall x y z:uniset, seq x y -> seq y z -> seq x z.
@@ -94,6 +99,7 @@ Lemma union_empty_left : forall x:uniset, seq x (union Emptyset x).
 Proof.
 unfold seq; unfold union; simpl; auto.
 Qed.
+#[local]
 Hint Resolve union_empty_left : core.
 
 Lemma union_empty_right : forall x:uniset, seq x (union x Emptyset).
@@ -101,6 +107,7 @@ Proof.
 unfold seq; unfold union; simpl.
 intros x a; rewrite (orb_b_false (charac x a)); auto.
 Qed.
+#[local]
 Hint Resolve union_empty_right : core.
 
 Lemma union_comm : forall x y:uniset, seq (union x y) (union y x).
@@ -108,6 +115,7 @@ Proof.
 unfold seq; unfold charac; unfold union.
 destruct x; destruct y; auto with bool.
 Qed.
+#[local]
 Hint Resolve union_comm : core.
 
 Lemma union_ass :
@@ -116,6 +124,7 @@ Proof.
 unfold seq; unfold union; unfold charac.
 destruct x; destruct y; destruct z; auto with bool.
 Qed.
+#[local]
 Hint Resolve union_ass : core.
 
 Lemma seq_left : forall x y z:uniset, seq x y -> seq (union x z) (union y z).
@@ -124,6 +133,7 @@ unfold seq; unfold union; unfold charac.
 destruct x; destruct y; destruct z.
 intros; elim H; auto.
 Qed.
+#[local]
 Hint Resolve seq_left : core.
 
 Lemma seq_right : forall x y z:uniset, seq x y -> seq (union z x) (union z y).
@@ -132,6 +142,7 @@ unfold seq; unfold union; unfold charac.
 destruct x; destruct y; destruct z.
 intros; elim H; auto.
 Qed.
+#[local]
 Hint Resolve seq_right : core.