Merge PR #9196: Document the deprecation of hint declaration withou database in refman.

1 files changed, 3 insertions, 1 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index ad80cb62e1..59602581c7 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3425,7 +3425,9 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
 
    .. cmdv:: Hint @hint_definition
 
-      No database name is given: the hint is registered in the core database.
+      No database name is given: the hint is registered in the ``core`` database.
+
+      .. deprecated:: 8.10
 
    .. cmdv:: Local Hint @hint_definition : {+ @ident}