From 002ab0b6bdf38c4dea0ce74e2a0df1e3d2bc238d Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 1 Dec 2020 15:15:38 +0100 Subject: Update doc/sphinx/changes.rst Co-authored-by: Jim Fehrle --- doc/sphinx/changes.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/sphinx') 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`. -- cgit v1.2.3