From eeb1d861551e25c6a92721334b3c9f36b7ebb012 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 13 Nov 2018 16:39:54 +0100
Subject: Deprecate hint declaration/removal with no specified database

Previously, hints added without a specified database where implicitly
put in the "core" database, which was discouraged by the user manual
(because of the lack of modularity of this approach).
---
 theories/Wellfounded/Inclusion.v          | 2 +-
 theories/Wellfounded/Transitive_Closure.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'theories/Wellfounded')

diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v
index ff233ef9c6..18c4bedd9a 100644
--- a/theories/Wellfounded/Inclusion.v
+++ b/theories/Wellfounded/Inclusion.v
@@ -22,7 +22,7 @@ Section WfInclusion.
     apply Acc_intro; auto with sets.
   Qed.
 
-  Hint Resolve Acc_incl.
+  Hint Resolve Acc_incl : core.
 
   Theorem wf_incl : inclusion A R1 R2 -> well_founded R2 -> well_founded R1.
   Proof.
diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v
index 59068623ae..0d56d88869 100644
--- a/theories/Wellfounded/Transitive_Closure.v
+++ b/theories/Wellfounded/Transitive_Closure.v
@@ -31,7 +31,7 @@ Section Wf_Transitive_Closure.
     apply Acc_inv with y; auto with sets.
   Defined.
 
-  Hint Resolve Acc_clos_trans.
+  Hint Resolve Acc_clos_trans : core.
 
   Lemma Acc_inv_trans : forall x y:A, trans_clos y x -> Acc R x -> Acc R y.
   Proof.
-- 
cgit v1.2.3