From 7e55f4813d5173d659482a6899c3f97c5346a682 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 15 Nov 2020 15:30:28 +0100 Subject: Document the new export locality for the remaining hint commands. --- .../13388-export-locality-for-all-hint-commands.rst | 6 ++++++ doc/sphinx/proofs/automatic-tactics/auto.rst | 4 +--- 2 files changed, 7 insertions(+), 3 deletions(-) create mode 100644 doc/changelog/07-commands-and-options/13388-export-locality-for-all-hint-commands.rst (limited to 'doc') diff --git a/doc/changelog/07-commands-and-options/13388-export-locality-for-all-hint-commands.rst b/doc/changelog/07-commands-and-options/13388-export-locality-for-all-hint-commands.rst new file mode 100644 index 0000000000..df2bdfeabb --- /dev/null +++ b/doc/changelog/07-commands-and-options/13388-export-locality-for-all-hint-commands.rst @@ -0,0 +1,6 @@ +- **Changed:** + The :attr:`export` locality can now be used for all Hint commands, + including Hint Cut, Hint Mode, Hint Transparent / Opaque and + Remove Hints + (`#13388 `_, + by Pierre-Marie Pédrot). diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst index e6dc6f6c51..485b92342d 100644 --- a/doc/sphinx/proofs/automatic-tactics/auto.rst +++ b/doc/sphinx/proofs/automatic-tactics/auto.rst @@ -280,9 +280,7 @@ automatically created. sections. + :attr:`export` are visible from other modules when they import the current - module. Requiring it is not enough. This attribute is only effective for - the :cmd:`Hint Resolve`, :cmd:`Hint Immediate`, :cmd:`Hint Unfold` and - :cmd:`Hint Extern` variants of the command. + module. Requiring it is not enough. + :attr:`global` hints are made available by merely requiring the current module. -- cgit v1.2.3