From 30a28e4d6f619610ea8f29c7055cc2bfc8a5f640 Mon Sep 17 00:00:00 2001
From: Pierre Rousselin <rousselin@math.univ-paris13.fr>
Date: Thu, 4 Jul 2024 18:24:49 +0200
Subject: [PATCH] Add locality rules for sections

---
 doc/sphinx/language/core/modules.rst  |  4 ++
 doc/sphinx/language/core/sections.rst | 72 +++++++++++++++++++++++++++
 2 files changed, 76 insertions(+)

diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst
index 5886b2b28f057..a69d1420b84f9 100644
--- a/doc/sphinx/language/core/modules.rst
+++ b/doc/sphinx/language/core/modules.rst
@@ -1066,6 +1066,10 @@ while noting a few exceptional commands for which :attr:`local` and
 
 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 <_Visibililty-attributes-sections>`.
+
+.. _Visibililty-attributes-modules:
 
 .. list-table::
   :header-rows: 1
diff --git a/doc/sphinx/language/core/sections.rst b/doc/sphinx/language/core/sections.rst
index f3a9a04eb4ee2..64090814e1d67 100644
--- 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.
 
+.. _Visibililty-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 <_Visibililty-attributes-sections>`.
+
+.. 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: