Qualify `Hint` as `Global Hint` where appropriate

This avoids a new warning of Coq 8.13.

Eventually these `Global Hint` should become `#[export] Hint`,
with a cleaner but different meaning than `Global Hint`.

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