diff options
| author | Pierre-Marie Pédrot | 2020-11-15 15:30:28 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-15 16:05:56 +0100 |
| commit | 7e55f4813d5173d659482a6899c3f97c5346a682 (patch) | |
| tree | 78fe06570c6a16cd4c9fba36846ae972818c8c08 | |
| parent | 46d0d39c9b0b448b040bbfbddea5e5a91b1d96d1 (diff) | |
Document the new export locality for the remaining hint commands.
| -rw-r--r-- | doc/changelog/07-commands-and-options/13388-export-locality-for-all-hint-commands.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/proofs/automatic-tactics/auto.rst | 4 |
2 files changed, 7 insertions, 3 deletions
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 <https://github.com/coq/coq/pull/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. |