Add locality rules for sections

Villetaneuse · Jul 5, 2024 · 00fd874 · 00fd874
1 parent 062067f
commit 00fd874
Show file tree

Hide file tree

Showing 2 changed files with 78 additions and 0 deletions.
diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst
@@ -1064,16 +1064,22 @@ while noting a few exceptional commands for which :attr:`local` and
       the user little control. We recommend using the :attr:`export`
       locality attribute where it is supported.
 
+.. _visibility-attributes-modules:
+
 The following table sums up the locality of vernacular commands in modules, when
 outside the module.
+A similar table for :cmd:`Section` can be found
+:ref:`here<visibility-attributes-sections>`.
 
 .. list-table::
   :header-rows: 1
 
   * - ``Command``
     - without attribute,
+
       not imported
     - without attribute,
+
       imported
     - :attr:`local`
     - :attr:`export`

diff --git a/doc/sphinx/language/core/sections.rst b/doc/sphinx/language/core/sections.rst
@@ -131,6 +131,78 @@ usable outside the section as shown in this :ref:`example <section_local_declara
    Notice the difference between the value of :g:`x'` and :g:`x''` inside section
    :g:`s1` and outside.
 
+.. _visibility-attributes-sections:
+
+Summary of locality attributes in a section
+-------------------------------------------
+
+The following table sums up the locality of vernacular commands in modules, when
+outside the module.
+A similar table for :cmd:`Module` can be found
+:ref:`here <visibility-attributes-modules>`.
+
+.. list-table::
+  :header-rows: 1
+
+  * - ``Command``
+    - without attribute
+    - :attr:`local`
+    - :attr:`export`
+    - :attr:`global`
+
+  * - :cmd:`Definition`, :cmd:`Lemma`, :cmd:`Axiom`, ...
+    - available
+    - available
+    - attribute not supported
+    - attribute not supported
+
+  * - :cmd:`Notation`
+    - not available outside
+    - not available outside
+    - attribute not supported
+    - attribute not supported
+
+  * - :cmd:`Notation (abbreviation)`
+    - not available outside
+    - not available outside
+    - attribute not supported
+    - attribute not supported
+
+  * - ``Hints`` (and :cmd:`Instance`)
+    - not available outside
+    - not available outside
+    - attribute not supported
+    - attribute not supported
+
+  * - :cmd:`Set` or :cmd:`Unset` a flag
+    - not available outside
+    - not available outside
+    - available outside
+    - available outside
+
+  * - :cmd:`Canonical Structure`
+    - available outside
+    - not available outside
+    - attribute not supported
+    - available outside
+
+  * - :cmd:`Ltac`
+    - not available outside
+    - not available outside
+    - attribute not supported
+    - attribute not supported
+
+  * - :cmd:`Coercion`
+    - available outside
+    - not available outside
+    - attribute not supported
+    - available outside
+
+  * - :cmd:`Tactic Notation`
+    - not available outside
+    - not available outside
+    - attribute not supported
+    - attribute not supported
 
 .. _Admissible-rules-for-global-environments: