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/rat.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

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

diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v
index 6015f33..14fde5a 100644
--- a/mathcomp/algebra/rat.v
+++ b/mathcomp/algebra/rat.v
@@ -56,7 +56,7 @@ Definition denq x := nosimpl ((valq x).2).
 
 Lemma denq_gt0  x : 0 < denq x.
 Proof. by rewrite /denq; case: x=> [[a b] /= /andP []]. Qed.
-Hint Resolve denq_gt0.
+Hint Resolve denq_gt0 : core.
 
 Definition denq_ge0 x := ltrW (denq_gt0 x).
 
@@ -64,7 +64,7 @@ Lemma denq_lt0  x : (denq x < 0) = false. Proof. by rewrite ltr_gtF. Qed.
 
 Lemma denq_neq0 x : denq x != 0.
 Proof. by rewrite /denq gtr_eqF ?denq_gt0. Qed.
-Hint Resolve denq_neq0.
+Hint Resolve denq_neq0 : core.
 
 Lemma denq_eq0 x : (denq x == 0) = false.
 Proof. exact: negPf (denq_neq0 _). Qed.
@@ -368,7 +368,7 @@ Qed.
 Notation "n %:Q" := ((n : int)%:~R : rat)
   (at level 2, left associativity, format "n %:Q")  : ring_scope.
 
-Hint Resolve denq_neq0 denq_gt0 denq_ge0.
+Hint Resolve denq_neq0 denq_gt0 denq_ge0 : core.
 
 Definition subq (x y : rat) : rat := (addq x (oppq y)).
 Definition divq (x y : rat) : rat := (mulq x (invq y)).
-- 
cgit v1.2.3