1 files changed, 12 insertions, 0 deletions
diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index 74d1e391c4..71c8f10755 100644
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.v
@@ -24,6 +24,7 @@ Section Between.
     | bet_emp : between k k
     | bet_S : forall l, between k l -> P l -> between k (S l).
 
+  #[local]
   Hint Constructors between: arith.
 
   Lemma bet_eq : forall k l, l = k -> between k l.
@@ -31,18 +32,21 @@ Section Between.
     intros * ->; auto with arith.
   Qed.
 
+  #[local]
   Hint Resolve bet_eq: arith.
 
   Lemma between_le : forall k l, between k l -> k <= l.
   Proof.
     induction 1; auto with arith.
   Qed.
+  #[local]
   Hint Immediate between_le: arith.
 
   Lemma between_Sk_l : forall k l, between k l -> S k <= l -> between (S k) l.
   Proof.
     induction 1 as [|* [|]]; auto with arith.
   Qed.
+  #[local]
   Hint Resolve between_Sk_l: arith.
 
   Lemma between_restr :
@@ -57,6 +61,7 @@ Section Between.
     | exists_S : forall l, exists_between k l -> exists_between k (S l)
     | exists_le : forall l, k <= l -> Q l -> exists_between k (S l).
 
+  #[local]
   Hint Constructors exists_between: arith.
 
   Lemma exists_le_S : forall k l, exists_between k l -> S k <= l.
@@ -66,12 +71,14 @@ Section Between.
 
   Lemma exists_lt : forall k l, exists_between k l -> k < l.
   Proof exists_le_S.
+  #[local]
   Hint Immediate exists_le_S exists_lt: arith.
 
   Lemma exists_S_le : forall k l, exists_between k (S l) -> k <= l.
   Proof.
     intros; apply le_S_n; auto with arith.
   Qed.
+  #[local]
   Hint Immediate exists_S_le: arith.
 
   Definition in_int p q r := p <= r /\ r < q.
@@ -80,6 +87,7 @@ Section Between.
   Proof.
     split; assumption.
   Qed.
+  #[local]
   Hint Resolve in_int_intro: arith.
 
   Lemma in_int_lt : forall p q r, in_int p q r -> p < q.
@@ -99,12 +107,14 @@ Section Between.
   Proof.
     intros * []; auto with arith.
   Qed.
+  #[local]
   Hint Resolve in_int_S: arith.
 
   Lemma in_int_Sp_q : forall p q r, in_int (S p) q r -> in_int p q r.
   Proof.
     intros * []; auto with arith.
   Qed.
+  #[local]
   Hint Immediate in_int_Sp_q: arith.
 
   Lemma between_in_int :
@@ -188,6 +198,8 @@ Section Between.
 
 End Between.
 
+#[global]
 Hint Resolve nth_O bet_S bet_emp bet_eq between_Sk_l exists_S exists_le
   in_int_S in_int_intro: arith.
+#[global]
 Hint Immediate in_int_Sp_q exists_le_S exists_S_le: arith.