Clarify meaning of entries in tables

Also group commands by similar behaviour.
Villetaneuse · Aug 2, 2024 · a30563f · a30563f
1 parent 440bb6b
commit a30563f
Show file tree

Hide file tree

Showing 2 changed files with 71 additions and 64 deletions.
diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst
@@ -679,13 +679,20 @@ Summary of locality attributes in a module
 ------------------------------------------
 
 This table sums up the effect of locality attributes on the scope of vernacular
-commands in a module, when outside the module where they were entered. A cross
-(❌) marks an unsupported attribute, which will provoke a compilation error. In
-this table, "not available", means that the command has no effect outside the
-module it was entered and "short name when imported" means that the command
-always has effects outside the module but if the module (or the command, via
-selective importation, when available) is not imported, the corresponding
-identifier must be qualified in order to be used.
+commands in a module, when outside the module where they were entered. In the
+following table:
+
+* a cross (❌) marks an unsupported attribute (compilation error);
+* "not available" means that the command has no effect outside the module it was entered;
+* "when imported" means that the command has effect outside the module if, and
+  only if, the module (or the command, via selective importation) is imported;
+* "short name when imported" means that the command has effects outside the module;
+  if the module (or command, via selective importation) is not imported, the
+  associated identifiers must be qualified;
+* "qualified name" means that the command has effects outside the module, but
+  the corresponding identifier may only be referred to with a qualified name;
+* "always" means that the command always has effects outside the module (even if
+  it is not imported).
 
 A similar table for :cmd:`Section` can be found
 :ref:`here<visibility-attributes-sections>`.
@@ -709,73 +716,72 @@ A similar table for :cmd:`Section` can be found
 
       when imported
 
-  * - :cmd:`Notation`
+  * - :cmd:`Ltac`
     - :attr:`global`
     - not available
     - ❌
-    - when imported
+    - short name
 
-  * - :cmd:`Notation (abbreviation)`
+      when imported
+
+  * - :cmd:`Ltac2`
     - :attr:`global`
     - not available
     - ❌
     - short name
 
       when imported
 
-  * - ``Hints`` (and :cmd:`Instance`)
-    - :attr:`export`
-    - not available
-    - when imported
-    - always
-
-  * - :cmd:`Set` or :cmd:`Unset` a flag
-    - :attr:`local`
+  * - :cmd:`Notation (abbreviation)`
+    - :attr:`global`
     - not available
-    - when imported
-    - always
+    - ❌
+    - short name
 
-  * - :cmd:`Canonical Structure`
-    - :attr:`local`
+      when imported
 
-      or :attr:`global`
-    - when imported
+  * - :cmd:`Notation`
+    - :attr:`global`
+    - not available
     - ❌
     - when imported
 
-  * - :cmd:`Coercion`
+  * - :cmd:`Tactic Notation`
     - :attr:`global`
     - not available
     - ❌
     - when imported
 
-  * - :cmd:`Ltac`
+  * - :cmd:`Ltac2 Notation`
     - :attr:`global`
     - not available
     - ❌
-    - short name
-
-      when imported
+    - when imported
 
-  * - :cmd:`Ltac2`
+  * - :cmd:`Coercion`
     - :attr:`global`
     - not available
     - ❌
-    - short name
-
-      when imported
+    - when imported
 
-  * - :cmd:`Tactic Notation`
+  * - :cmd:`Canonical Structure`
     - :attr:`global`
-    - not available
+
+    - when imported
     - ❌
     - when imported
 
-  * - :cmd:`Ltac2 Notation`
-    - :attr:`global`
+  * - ``Hints`` (and :cmd:`Instance`)
+    - :attr:`export`
     - not available
-    - ❌
     - when imported
+    - always
+
+  * - :cmd:`Set` or :cmd:`Unset` a flag
+    - :attr:`local`
+    - not available
+    - when imported
+    - always
 
 Typing Modules
 ------------------

diff --git a/doc/sphinx/language/core/sections.rst b/doc/sphinx/language/core/sections.rst
@@ -137,11 +137,12 @@ Summary of locality attributes in a section
 -------------------------------------------
 
 This table sums up the effect of locality attributes on the scope of vernacular
-commands in a section, when outside the section where they were entered. A cross
-(❌) marks an unsupported attribute, which will provoke a compilation error. In
-this table, "not available", means that the command has no effect outside the
-section it was entered, while "available" means that the effects of the command
-persists outside the section.
+commands in a section, when outside the section where they were entered. In the
+following table:
+
+* a cross (❌) marks an unsupported attribute (compilation error);
+* "not available" means that the command has no effect outside the section it was entered;
+* "available" means that the effect of the command persists outside the section.
 
 A similar table for :cmd:`Module` can be found
 :ref:`here <visibility-attributes-modules>`.
@@ -161,66 +162,66 @@ A similar table for :cmd:`Module` can be found
     - ❌
     - ❌
 
-  * - :cmd:`Notation`
+  * - :cmd:`Ltac`
     - :attr:`local`
     - not available
     - ❌
     - ❌
 
-  * - :cmd:`Notation (abbreviation)`
+  * - :cmd:`Ltac2`
     - :attr:`local`
     - not available
     - ❌
     - ❌
 
-  * - ``Hints`` (and :cmd:`Instance`)
+  * - :cmd:`Notation (abbreviation)`
     - :attr:`local`
     - not available
     - ❌
     - ❌
 
-  * - :cmd:`Set` or :cmd:`Unset` a flag
+  * - :cmd:`Notation`
     - :attr:`local`
     - not available
-    - available
-    - available
-
-  * - :cmd:`Canonical Structure`
-    - :attr:`global`
-    - not available
     - ❌
-    - available
-
-  * - :cmd:`Coercion`
-    - :attr:`global`
-    - not available
     - ❌
-    - available
 
-  * - :cmd:`Ltac`
+  * - :cmd:`Tactic Notation`
     - :attr:`local`
     - not available
     - ❌
     - ❌
 
-  * - :cmd:`Ltac2`
+  * - :cmd:`Ltac2 Notation`
     - :attr:`local`
     - not available
     - ❌
     - ❌
 
-  * - :cmd:`Tactic Notation`
-    - :attr:`local`
+  * - :cmd:`Coercion`
+    - :attr:`global`
     - not available
     - ❌
+    - available
+
+  * - :cmd:`Canonical Structure`
+    - :attr:`global`
+    - not available
     - ❌
+    - available
 
-  * - :cmd:`Ltac2 Notation`
+  * - ``Hints`` (and :cmd:`Instance`)
     - :attr:`local`
     - not available
     - ❌
     - ❌
 
+  * - :cmd:`Set` or :cmd:`Unset` a flag
+    - :attr:`local`
+    - not available
+    - available
+    - available
+
 .. _Admissible-rules-for-global-environments:
 
 Typing rules used at the end of a section