diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst index 5886b2b28f057..df35d0b64e8b8 100644 --- 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`. .. 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 index f3a9a04eb4ee2..d711606551972 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 `. + +.. 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: