diff options
Diffstat (limited to 'doc/changelog')
| -rw-r--r-- | doc/changelog/07-commands-and-options/13384-warn-unqualified-hint.rst | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/doc/changelog/07-commands-and-options/13384-warn-unqualified-hint.rst b/doc/changelog/07-commands-and-options/13384-warn-unqualified-hint.rst new file mode 100644 index 0000000000..8ec7198b72 --- /dev/null +++ b/doc/changelog/07-commands-and-options/13384-warn-unqualified-hint.rst @@ -0,0 +1,8 @@ +- **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 + (`#13384 <https://github.com/coq/coq/pull/13384>`_, + by Pierre-Marie Pédrot). |