1 files changed, 1 insertions, 1 deletions
diff --git a/lib/Intv.v b/lib/Intv.v
index 19943942..82d3c751 100644
--- a/lib/Intv.v
+++ b/lib/Intv.v
@@ -303,7 +303,7 @@ Qed.
 
 (** Hints *)
 
-Hint Resolve
+Global Hint Resolve
   notin_range range_notin
   is_notempty empty_notin in_notempty
   disjoint_sym empty_disjoint_r empty_disjoint_l