Document locality of Ltac2 Set

doc/sphinx/proof-engine/ltac2.rst

@@ -319,6 +319,12 @@ Ltac2 Definitions
    The previous value of the binding can be optionally accessed using the `as`
    binding syntax.
 
+   The effect of this command is limited to the current section or module.
+   When not in a section, importing the module containing this command
+   applies the redefinition again.
+   In other words it acts according to :attr:`local` in sections and
+   :attr:`export` otherwise (but explicit locality is not supported).
+
    .. example:: Dynamic nature of mutable cells
 
       .. coqtop:: all