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/Program/Basics.v | 2 +-
 theories/Program/Wf.v     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'theories/Program')

diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index c2316689fc..d86112abc0 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -26,7 +26,7 @@ Arguments id {A} x.
 Definition compose {A B C} (g : B -> C) (f : A -> B) :=
   fun x : A => g (f x).
 
-Hint Unfold compose.
+Hint Unfold compose : core.
 
 Declare Scope program_scope.
 
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 8479b9a2bb..f9d23e3cf6 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -110,7 +110,7 @@ Section Measure_well_founded.
 
 End Measure_well_founded.
 
-Hint Resolve measure_wf.
+Hint Resolve measure_wf : core.
 
 Section Fix_rects.
 
-- 
cgit v1.2.3