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

(limited to 'theories/Numbers/Cyclic/ZModulo/ZModulo.v')

diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
index 784e81758c..4bcd22543f 100644
--- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v
+++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
@@ -60,7 +60,7 @@ Section ZModulo.
   apply Z.lt_gt.
   unfold wB, base; auto with zarith.
  Qed.
- Hint Resolve wB_pos.
+ Hint Resolve wB_pos : core.
 
  Lemma spec_to_Z_1 : forall x, 0 <= [|x|].
  Proof.
@@ -71,7 +71,7 @@ Section ZModulo.
  Proof.
   unfold to_Z; intros; destruct (Z_mod_lt x wB wB_pos); auto.
  Qed.
- Hint Resolve spec_to_Z_1 spec_to_Z_2.
+ Hint Resolve spec_to_Z_1 spec_to_Z_2 : core.
 
  Lemma spec_to_Z : forall x, 0 <= [|x|] < wB.
  Proof.
@@ -732,7 +732,7 @@ Section ZModulo.
  Proof.
  induction p; simpl; auto with zarith.
  Qed.
- Hint Resolve Ptail_pos.
+ Hint Resolve Ptail_pos : core.
 
  Lemma Ptail_bounded : forall p d, Zpos p < 2^(Zpos d) -> Ptail p < Zpos d.
  Proof.
-- 
cgit v1.2.3