Clarify locality rules for some commands in refman

Here are the modified entries:
- Definition
- Axiom
- Notation (abbreviation)
- Canonical Structure
- Set

doc/sphinx/language/core/assumptions.rst

@@ -175,6 +175,10 @@ has type :n:`@type`.
 
    :cmd:`Axiom`, :cmd:`Conjecture`, :cmd:`Parameter` and their plural forms
    are equivalent.  They can take the :attr:`local` :term:`attribute`,
+   which makes the declared :n:`@ident` accessible only through their fully
+   qualified names, even if :cmd:`Import` or its variants has been used on the
+   current module.
+
    which makes the defined :n:`@ident`\s accessible by :cmd:`Import` and its variants
    only through their fully qualified names.
 

doc/sphinx/language/core/basic.rst

@@ -632,11 +632,17 @@ The :cmd:`Set` and :cmd:`Unset` commands support the mutually
 exclusive :attr:`local`, :attr:`export` and :attr:`global` locality
 attributes.
 
-If no attribute is specified, the original value of the flag or option
-is restored at the end of the current module but it is *not* restored
-at the end of the current section.
-
-Newly opened modules and sections inherit the current settings.
+* If no attribute is specified, the original value of the flag or option
+  is restored at the end of the current module but it is *not* restored
+  at the end of the current section.
+* The :attr:`local` attribute makes the setting local to the current
+  :cmd:`Section` (if applicable) or :cmd:`Module`.
+* The :attr:`export` attribute makes the setting local to the current
+  :cmd:`Module`, unless :cmd:`Import` (or one of its variants) is used
+  on the :cmd:`Module`.
+* The :attr:`global` attribute makes the setting persist outside the current
+  :cmd:`Module` in the current file, or whenever :cmd:`Require` is used on the
+  current file.
 
 .. note::
 

doc/sphinx/language/core/definitions.rst

@@ -94,8 +94,9 @@ Section :ref:`typing-rules`.
 
    These commands bind :n:`@term` to the name :n:`@ident` in the global environment,
    provided that :n:`@term` is well-typed.  They can take the :attr:`local` :term:`attribute`,
-   which makes the defined :n:`@ident` accessible by :cmd:`Import` and its variants
-   only through their fully qualified names.
+   which makes the defined :n:`@ident` accessible only through their fully
+   qualified names, even if :cmd:`Import` or its variants has been used on the
+   current :cmd:`Module`.
    If :n:`@reduce` is present then :n:`@ident` is bound to the result of the specified
    computation on :n:`@term`.
 

doc/sphinx/language/extensions/canonical.rst

@@ -41,6 +41,10 @@ in :ref:`canonicalstructures`; here only a simple example is given.
    This command supports the :attr:`local` attribute.  When used, the
    structure is canonical only within the :cmd:`Section` containing it.
 
+   Outside a :cmd:`Section`, the structure is canonical as soon as
+   :cmd:`Import` (or one of its variants) has been used on the :cmd:`Module`
+   in which it is defined, regardless of its locality attribute, if any.
+
    :token:`qualid` (in :token:`reference`) denotes an object :n:`(Build_struct c__1 … c__n)` in the
    structure :g:`struct` for which the fields are :n:`x__1, …, x__n`.
    Then, each time an equation of the form :n:`(x__i _)` |eq_beta_delta_iota_zeta| :n:`c__i` has to be

doc/sphinx/user-extensions/syntax-extensions.rst

@@ -1892,6 +1892,11 @@ Abbreviations
    This command supports the :attr:`local` attribute, which limits the notation to the
    current module.
 
+   Unlike a :cmd:`Notation`, an abbreviation defined with the default locality
+   is available (with a fully qualified name) outside the current module even
+   when :cmd:`Import` (or one of its variants) has not been used on the current
+   :cmd:`Module`.
+
    An *abbreviation* is a name, possibly applied to arguments, that
    denotes a (presumably) more complex expression. Here are examples: