diff options
| author | coqbot-app[bot] | 2020-11-16 11:27:08 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-16 11:27:08 +0000 |
| commit | 57fb6f106f24d2fa1e66a8ac813525f804a7ced7 (patch) | |
| tree | cda92a9bb323790a506ced2759b39684942bdc2a /doc/sphinx | |
| parent | 4775fd7724840205b345420507bdd1c7065059b0 (diff) | |
| parent | 7e55f4813d5173d659482a6899c3f97c5346a682 (diff) | |
Merge PR #13388: Export locality for all hint commands
Reviewed-by: silene
Reviewed-by: gares
Reviewed-by: Zimmi48
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/proofs/automatic-tactics/auto.rst | 4 |
1 files changed, 1 insertions, 3 deletions
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. |