Add missing hint localities

Silences warnings in Coq >=v8.13
coq-community · Aug 20, 2021 · da101d6 · da101d6
1 parent 30fe1f7
commit da101d6
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 5 deletions.
diff --git a/theories/Topology/Homeomorphisms.v b/theories/Topology/Homeomorphisms.v
@@ -87,4 +87,4 @@ Definition topological_property (P : TopologicalSpace -> Prop) :=
   forall X Y (f : point_set X -> point_set Y),
     homeomorphism f -> P X -> P Y.
 
-Hint Unfold topological_property : homeo.
+Global Hint Unfold topological_property : homeo.
diff --git a/theories/Topology/TopologicalSpaces.v b/theories/Topology/TopologicalSpaces.v
@@ -200,8 +200,8 @@ rewrite Complement_IndexedUnion.
 apply open_finite_indexed_intersection; trivial.
 Qed.
 
-Hint Unfold closed : topology.
-Hint Resolve open_family_union open_intersection2 open_full
+Global Hint Unfold closed : topology.
+Global Hint Resolve open_family_union open_intersection2 open_full
   open_empty open_union2 open_indexed_union
   open_finite_indexed_intersection closed_complement_open
   closed_union2 closed_intersection2 closed_family_intersection

diff --git a/theories/ZornsLemma/InverseImage.v b/theories/ZornsLemma/InverseImage.v
@@ -6,7 +6,7 @@ From ZornsLemma Require Import IndexedFamilies.
 
 Definition inverse_image {X Y:Type} (f:X->Y) (T:Ensemble Y) : Ensemble X :=
   [ x:X | In T (f x) ].
-Hint Unfold inverse_image : sets.
+Global Hint Unfold inverse_image : sets.
 
 Lemma inverse_image_increasing: forall {X Y:Type} (f:X->Y)
   (T1 T2:Ensemble Y), Included T1 T2 ->
@@ -94,7 +94,7 @@ apply Extensionality_Ensembles; split; red; intros.
   constructor; trivial.
 Qed.
 
-Hint Resolve @inverse_image_increasing : sets.
+Global Hint Resolve @inverse_image_increasing : sets.
 Hint Rewrite @inverse_image_empty @inverse_image_full
   @inverse_image_intersection @inverse_image_union
   @inverse_image_complement @inverse_image_composition : sets.