diff options
| -rw-r--r-- | doc/sphinx/changes.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 674adb2038..6facb0e207 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -35,7 +35,7 @@ The main changes include: multiple distinct patterns. - New warning for `Hint` commands outside sections without a locality attribute, whose goal is to eventually remove the fragile default - behavior of having hints be imported when using `Require` only. + behavior of importing hints only when using `Require`. The recommended fix is to declare hints as `export`, instead of the current default `global`, meaning that they are imported through `Require Import` only, not `Require`. |