diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index e42af2fb211b2..8fe864e3e2001 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/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