diff --git a/theories/Topology/Homeomorphisms.v b/theories/Topology/Homeomorphisms.v index 98d0a8f4..36fb001e 100644 --- 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 index 6788ea7a..7c79a1b8 100644 --- 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 index 3492e1b9..23126194 100644 --- 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.