From c1b6cf4ecff5bc8916723fb84c7d49744a0e82ad Mon Sep 17 00:00:00 2001 From: Pierre Rousselin Date: Tue, 6 Aug 2024 10:00:14 +0200 Subject: [PATCH] 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 | 4 ++++ doc/sphinx/language/core/basic.rst | 16 +++++++++++----- doc/sphinx/language/core/definitions.rst | 5 +++-- doc/sphinx/language/extensions/canonical.rst | 4 ++++ doc/sphinx/user-extensions/syntax-extensions.rst | 5 +++++ 5 files changed, 27 insertions(+), 7 deletions(-) diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst index ff9758497d7e..ee057b7a1153 100644 --- a/doc/sphinx/language/core/assumptions.rst +++ b/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. diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index e6d019cf4b53..2bfe4d7a3fc0 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/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:: diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index 7e8ae28d4430..baddd9f30200 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/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`. diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst index d9fc3744d3c0..5900adc415af 100644 --- a/doc/sphinx/language/extensions/canonical.rst +++ b/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 diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 06aebd90b168..c9e42b206b6b 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/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: