Add documentation for the export hint.

2 files changed, 24 insertions, 7 deletions

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