diff options
| author | Matthieu Sozeau | 2020-12-01 15:15:38 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2020-12-03 16:03:37 +0100 |
| commit | 002ab0b6bdf38c4dea0ce74e2a0df1e3d2bc238d (patch) | |
| tree | b746b68e7bc27566263322ed77512cc49f94f962 | |
| parent | f23ccddcf3bb72d190cfb05e7b48bee416eb8a42 (diff) | |
Update doc/sphinx/changes.rst
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
| -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`. |