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/changelog | |
| 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/changelog')
| -rw-r--r-- | doc/changelog/07-commands-and-options/13388-export-locality-for-all-hint-commands.rst | 6 |
1 files changed, 6 insertions, 0 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). |