From 85a4780bcb462a9fb5a86bb510929e036171d2fe Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 10 Jul 2020 19:01:43 +0200
Subject: Tweak the warning for arbitrary term hints.

Fixes #11970.
---
 vernac/comHints.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'vernac')

diff --git a/vernac/comHints.ml b/vernac/comHints.ml
index b05bf9a675..0e3e3c61a9 100644
--- a/vernac/comHints.ml
+++ b/vernac/comHints.ml
@@ -64,11 +64,11 @@ let project_hint ~poly pri l2r r =
   (info, false, true, Hints.PathAny, Hints.IsGlobRef (Names.GlobRef.ConstRef c))
 
 let warn_deprecated_hint_constr =
-  CWarnings.create ~name:"deprecated-hint-constr" ~category:"deprecated"
+  CWarnings.create ~name:"fragile-hint-constr" ~category:"automation"
     (fun () ->
       Pp.strbrk
-        "Declaring arbitrary terms as hints is deprecated; declare a global \
-         reference instead")
+        "Declaring arbitrary terms as hints is fragile; it is recommended to \
+         declare a toplevel constant instead")
 
 let interp_hints ~poly h =
   let env = Global.env () in
-- 
cgit v1.2.3