From 2e6e0001f8215e3c42f2557df42e0d6486035c07 Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Mon, 26 Nov 2018 14:48:50 +0100
Subject: Fix some new warnings emitted by Coq 8.10:

```
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
```
---
 mathcomp/algebra/interval.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'mathcomp/algebra/interval.v')

diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v
index 1ca3414..b5d58cb 100644
--- a/mathcomp/algebra/interval.v
+++ b/mathcomp/algebra/interval.v
@@ -187,12 +187,12 @@ Proof. by move: bl br => [[] a|] [[] b|]. Qed.
 Lemma le_boundr_refl : reflexive le_boundr.
 Proof. by move=> [[] b|]; rewrite /le_boundr /= ?lerr. Qed.
 
-Hint Resolve le_boundr_refl.
+Hint Resolve le_boundr_refl : core.
 
 Lemma le_boundl_refl : reflexive le_boundl.
 Proof. by move=> [[] b|]; rewrite /le_boundl /= ?lerr. Qed.
 
-Hint Resolve le_boundl_refl.
+Hint Resolve le_boundl_refl : core.
 
 Lemma le_boundl_bb x b1 b2 :
   le_boundl (BOpen_if b1 x) (BOpen_if b2 x) = (b1 ==> b2).
@@ -242,7 +242,7 @@ move=> x [[[] a|] [[] b|]]; move/itv_dec=> //= [hl hu]; do ?[split=> //;
     | by apply: negbTE; rewrite ltr_geF // (@ler_lt_trans _ x)].
 Qed.
 
-Hint Rewrite intP.
+Hint Rewrite intP : core.
 Arguments itvP [x i].
 
 Definition subitv (i1 i2 : interval R) :=
-- 
cgit v1.2.3