Shorter tables and explanations

Villetaneuse · Aug 1, 2024 · 20a6661 · 20a6661
1 parent 8d19e5d
commit 20a6661
Show file tree

Hide file tree

Showing 4 changed files with 93 additions and 76 deletions.
diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst
@@ -1070,84 +1070,94 @@ while noting a few exceptional commands for which :attr:`local` and
 
 .. _visibility-attributes-modules:
 
-The following table sums up the locality of vernacular commands in modules, when
-outside the module where they were entered.
+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.
+
 A similar table for :cmd:`Section` can be found
 :ref:`here<visibility-attributes-sections>`.
 
 .. list-table::
   :header-rows: 1
 
   * - ``Command``
-    - without attribute
+    - no attribute
     - :attr:`local`
     - :attr:`export`
     - :attr:`global`
 
   * - :cmd:`Definition`, :cmd:`Lemma`, :cmd:`Axiom`, ...
-    - same as :attr:`global`
-    - available with qualified name
-    - attribute not supported
-    - available with short name if imported, with qualified name if not
+    - :attr:`global`
+    - qualified name
+    - ❌
+    - short name when imported
 
   * - :cmd:`Notation`
-    - same as :attr:`global`
+    - :attr:`global`
     - not available
-    - attribute not supported
-    - available when imported
+    - ❌
+    - when imported
 
   * - :cmd:`Notation (abbreviation)`
-    - same as :attr:`global`
+    - :attr:`global`
     - not available
-    - attribute not supported
-    - available with short name if imported, with qualified name if not
+    - ❌
+    - short name when imported
 
   * - ``Hints`` (and :cmd:`Instance`)
-    - same as :attr:`export`
+    - :attr:`export`
     - not available
-    - available when imported
-    - always available outside
+    - when imported
+    - always
 
   * - :cmd:`Set` or :cmd:`Unset` a flag
-    - same as :attr:`local`
-    - no effect
-    - in effect when imported
-    - in effect outside
+    - :attr:`local`
+    - not available
+    - when imported
+    - always
 
   * - :cmd:`Canonical Structure`
-    - same as :attr:`local`
+    - :attr:`local`
 
       or :attr:`global`
-    - available when imported
-    - attribute not supported
-    - available when imported
+    - when imported
+    - ❌
+    - when imported
 
   * - :cmd:`Coercion`
-    - same as :attr:`global`
+    - :attr:`global`
     - not available
-    - attribute not supported
-    - available when imported
+    - ❌
+    - when imported
 
   * - :cmd:`Ltac`
-    - same as :attr:`global`
+    - :attr:`global`
     - not available
-    - attribute not supported
-    - available with short name if imported, with qualified name if not
+    - ❌
+    - short name when imported
 
   * - :cmd:`Ltac2`
-    - same as :attr:`global`
+    - :attr:`global`
     - not available
-    - attribute not supported
-    - available with short name if imported, with qualified name if not
+    - ❌
+    - short name when imported
 
   * - :cmd:`Tactic Notation`
-    - same as :attr:`global`
+    - :attr:`global`
     - not available
-    - attribute not supported
-    - available when imported
+    - ❌
+    - when imported
 
   * - :cmd:`Ltac2 Notation`
-    - same as :attr:`global`
+    - :attr:`global`
     - not available
-    - attribute not supported
-    - available when imported
+    - ❌
+    - when imported
diff --git a/doc/sphinx/language/core/sections.rst b/doc/sphinx/language/core/sections.rst
@@ -136,85 +136,90 @@ usable outside the section as shown in this :ref:`example <section_local_declara
 Summary of locality attributes in a section
 -------------------------------------------
 
-The following table sums up the locality of vernacular commands in sections, when
-outside the section it was entered.
+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.
+
 A similar table for :cmd:`Module` can be found
 :ref:`here <visibility-attributes-modules>`.
 
 .. list-table::
   :header-rows: 1
 
   * - ``Command``
-    - without attribute
+    - no attribute
     - :attr:`local`
     - :attr:`export`
     - :attr:`global`
 
   * - :cmd:`Definition`, :cmd:`Lemma`, :cmd:`Axiom`, ...
-    - same as :attr:`local`
+    - :attr:`local`
     - available
-    - attribute not supported
-    - attribute not supported
+    - ❌
+    - ❌
 
   * - :cmd:`Notation`
-    - same as :`local`
+    - :attr:`local`
     - not available
-    - attribute not supported
-    - attribute not supported
+    - ❌
+    - ❌
 
   * - :cmd:`Notation (abbreviation)`
-    - same as :attr:`local`
+    - :attr:`local`
     - not available
-    - attribute not supported
-    - attribute not supported
+    - ❌
+    - ❌
 
   * - ``Hints`` (and :cmd:`Instance`)
-    - same as :attr:`local`
+    - :attr:`local`
     - not available
-    - attribute not supported
-    - attribute not supported
+    - ❌
+    - ❌
 
   * - :cmd:`Set` or :cmd:`Unset` a flag
-    - same as :attr:`local`
-    - no effect
-    - in effect
-    - in effect
+    - :attr:`local`
+    - not available
+    - available
+    - available
 
   * - :cmd:`Canonical Structure`
-    - same as :attr:`global`
+    - :attr:`global`
     - not available
-    - attribute not supported
+    - ❌
     - available
 
   * - :cmd:`Coercion`
-    - same as :attr:`global`
+    - :attr:`global`
     - not available
-    - attribute not supported
+    - ❌
     - available
 
   * - :cmd:`Ltac`
-    - same as :attr:`local`
-    - not available outside
-    - attribute not supported
-    - attribute not supported
+    - :attr:`local`
+    - not available
+    - ❌
+    - ❌
 
   * - :cmd:`Ltac2`
-    - same as :attr:`local`
-    - not available outside
-    - attribute not supported
-    - attribute not supported
+    - :attr:`local`
+    - not available
+    - ❌
+    - ❌
 
   * - :cmd:`Tactic Notation`
-    - same as :attr:`local`
+    - :attr:`local`
     - not available
-    - attribute not supported
-    - attribute not supported
+    - ❌
+    - ❌
 
   * - :cmd:`Ltac2 Notation`
-    - same as :attr:`local`
+    - :attr:`local`
     - not available
-    - attribute not supported
-    - attribute not supported
+    - ❌
+    - ❌
 
 .. _Admissible-rules-for-global-environments:
 

diff --git a/test-suite/success/locality_attributes_modules_ltac2.v b/test-suite/success/locality_attributes_modules_ltac2.v
@@ -113,3 +113,4 @@ Print Bar.find_secret.
 (* Availability of the tactic notation *)
 Lemma plop_i : 2 + 2 = 4.
 Proof. rfl. Qed.
+End InModuleGlobal.
diff --git a/test-suite/success/locality_attributes_sections_ltac2.v b/test-suite/success/locality_attributes_sections_ltac2.v
@@ -76,3 +76,4 @@ Fail Print find_secret.
 (* Availability of the tactic notation *)
 Lemma plop_ni : 2 + 2 = 4.
 Proof. Fail rfl. Admitted.
+End InSectionGlobal.