From bd308dab655e37275afc3fd33ed80cb73647a9ae Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Mon, 25 Nov 2019 00:50:35 +0900
Subject: Fix hint declarations to specify the database explicitly

---
 mathcomp/ssreflect/finset.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index 5c2ad4c..6f7c5b5 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -2257,7 +2257,7 @@ suff iter_big k : k <= n.+1 -> k <= #|iter k F set0|.
 elim: k => [|k IHk] k_lt //=; apply: (leq_ltn_trans (IHk (ltnW k_lt))).
 by rewrite proper_card// properEneq// subset_iterS neq_iter.
 Qed.
-Hint Resolve fixsetK.
+Hint Resolve fixsetK : core.
 
 Lemma minset_fix : minset [pred X | F X == X] fixset.
 Proof.
@@ -2338,7 +2338,7 @@ Hypothesis (F_mono : {homo F : X Y / X \subset Y}).
 Definition funsetC X := ~: (F (~: X)).
 Lemma funsetC_mono : {homo funsetC : X Y / X \subset Y}.
 Proof. by move=> *; rewrite subCset setCK F_mono// subCset setCK. Qed.
-Hint Resolve funsetC_mono.
+Hint Resolve funsetC_mono : core.
 
 Definition cofixset := ~: fixset funsetC.
 
-- 
cgit v1.2.3