From 56578a246e6b13d539fd6b0f54f7e06c641fd847 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Thu, 21 Jan 2021 12:02:49 -0800
Subject: Improve wording for #13384

---
 doc/sphinx/changes.rst | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'doc/sphinx/changes.rst')

diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index d9e4e4f2b3..7db54987d6 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -531,11 +531,11 @@ Commands and options
   .. _813HintWarning:
 
 - **Deprecated:**
-  The default value for hint locality is currently :attr:`local` in a section and
-  :attr:`global` otherwise, but is scheduled to change in a future release. For the
-  time being, adding hints outside of sections without specifying an explicit
-  locality is therefore triggering a deprecation warning. It is recommended to
-  use :attr:`export` whenever possible
+  Hint locality currently defaults to :attr:`local` in a section and
+  :attr:`global` otherwise, but this will change in a future release.
+  Hints added outside of sections without an explicit
+  locality now generate a deprecation warning. We recommend
+  using :attr:`export` where possible
   (`#13384 <https://github.com/coq/coq/pull/13384>`_,
   by Pierre-Marie Pédrot).
 - **Deprecated:**
-- 
cgit v1.2.3