From 7b124ee24aa6ebaf14c5f7019949a7c2a877dedb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 12 Mar 2020 16:24:27 +0100
Subject: Add documentation for the export hint.

---
 .../11812-export-hint-globality.rst                |  5 +++++
 doc/sphinx/proof-engine/tactics.rst                | 25 ++++++++++++++++------
 doc/sphinx/proof-engine/vernacular-commands.rst    |  6 ++++++
 3 files changed, 29 insertions(+), 7 deletions(-)
 create mode 100644 doc/changelog/07-commands-and-options/11812-export-hint-globality.rst

diff --git a/doc/changelog/07-commands-and-options/11812-export-hint-globality.rst b/doc/changelog/07-commands-and-options/11812-export-hint-globality.rst
new file mode 100644
index 0000000000..9341eebb58
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/11812-export-hint-globality.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  the :cmd:`Hint` commands now accept the :attr:`export` locality as
+  an attribute, allowing to make import-scoped hints
+  (`#11812 <https://github.com/coq/coq/pull/11812>`_,
+  by Pierre-Marie Pédrot).
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 4f2f74aae4..be185e885b 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3759,6 +3759,24 @@ automatically created.
 .. cmd:: Hint @hint_definition : {+ @ident}
 
    The general command to add a hint to some databases :n:`{+ @ident}`.
+
+   This command supports the :attr:`local`, :attr:`global` and :attr:`export`
+   locality attributes. When no locality is explictly given, the
+   command is :attr:`local` inside a section and :attr:`global` otherwise.
+
+   + :attr:`local` hints are never visible from other modules, even if they
+     require or import the current module. Inside a section, the :attr:`local`
+     attribute is useless since hints do not survive anyway to the closure of
+     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.
+
+   + :attr:`global` hints are made available by merely requiring the current
+     module.
+
    The various possible :production:`hint_definition`\s are given below.
 
    .. cmdv:: Hint @hint_definition
@@ -3767,13 +3785,6 @@ automatically created.
 
       .. deprecated:: 8.10
 
-   .. cmdv:: Local Hint @hint_definition : {+ @ident}
-
-      This is used to declare hints that must not be exported to the other modules
-      that require and import the current module. Inside a section, the flag
-      Local is useless since hints do not survive anyway to the closure of
-      sections.
-
    .. cmdv:: Hint Resolve @qualid {? | {? @num} {? @pattern}} : @ident
       :name: Hint Resolve
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index d1f3dcc309..4401f8fa2f 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1190,6 +1190,12 @@ Controlling the locality of commands
      occurs in a section.  The :cmd:`Set` and :cmd:`Unset` commands belong to this
      category.
 
+.. attr:: export
+
+  Some commands support an :attr:`export` attribute. The effect of the attribute
+  is to make the effect of the command available when the module containing it
+  is imported. The :cmd:`Hint` command accepts it for instance.
+
 .. _controlling-typing-flags:
 
 Controlling Typing Flags
-- 
cgit v1.2.3