diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst index edca38a58aec..be118554a8c7 100644 --- 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`. @@ -709,13 +716,15 @@ 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 - ❌ @@ -723,59 +732,56 @@ A similar table for :cmd:`Section` can be found 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 index fd09bf22e8c7..3a75e93abdeb 100644 --- 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 `. @@ -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