From 7d93822b72c277ca0358be90062cee84ec13ba46 Mon Sep 17 00:00:00 2001 From: Pierre Rousselin Date: Sat, 3 Aug 2024 18:22:19 +0200 Subject: [PATCH] Add visibility rules in section in module A local definition in a section is also local in the current module. An export/global setting in a section is also export/global in the current module. Unfortunately, this makes the section table more complicated. The section part of the refman is also slightly modified: - a subtitle "Using sections" appears before the description of the commands, in order to have a better TOC - In the first sentences, "declarations" was inaccurate, since Let introduces definitions - The "Note" starting with "Most commands" refers to the locality table --- doc/sphinx/language/core/modules.rst | 10 ++-- doc/sphinx/language/core/sections.rst | 68 +++++++++++++++++++++------ 2 files changed, 59 insertions(+), 19 deletions(-) diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst index be118554a8c7..5401f57a283e 100644 --- a/doc/sphinx/language/core/modules.rst +++ b/doc/sphinx/language/core/modules.rst @@ -683,15 +683,15 @@ 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 +* “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; +* “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 +* “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 +* “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 diff --git a/doc/sphinx/language/core/sections.rst b/doc/sphinx/language/core/sections.rst index 3a75e93abdeb..79d9d4ad59a9 100644 --- a/doc/sphinx/language/core/sections.rst +++ b/doc/sphinx/language/core/sections.rst @@ -4,16 +4,20 @@ Sections ==================================== Sections are naming scopes that permit creating section-local declarations that can -be used by other declarations in the section. Declarations made -with :cmd:`Variable`, :cmd:`Hypothesis`, :cmd:`Context`, -:cmd:`Let`, :cmd:`Let Fixpoint` and -:cmd:`Let CoFixpoint` (or the plural variants of the first two) within sections -are local to the section. +be used by other declarations in the section. Declarations made with +:cmd:`Variable`, :cmd:`Hypothesis`, :cmd:`Context` +(or the plural variants of the first two) +and definitions made with +:cmd:`Let`, :cmd:`Let Fixpoint` and :cmd:`Let CoFixpoint` +within sections are local to the section. In proofs done within the section, section-local declarations are included in the :term:`local context` of the initial goal of the proof. They are also accessible in definitions made with the :cmd:`Definition` command. +Using sections +-------------- + Sections are opened by the :cmd:`Section` command, and closed by :cmd:`End`. Sections can be nested. When a section is closed, its local declarations are no longer available. @@ -48,6 +52,8 @@ usable outside the section as shown in this :ref:`example ` commands, :cmd:`Notation` and option management commands that appear inside a section are canceled when the section is closed. + In some cases, this behaviour can be tuned with locality attributes. + See :ref:`this table`. .. cmd:: Let @ident_decl @def_body Let Fixpoint @fix_definition {* with @fix_definition } @@ -141,8 +147,14 @@ 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. +* “not available” means that the command has no effect outside the section it + was entered; +* “available” means that the effects of the command persists outside the section. +* For :cmd:`Definition` (and :cmd:`Lemma`, ...), :cmd:`Canonical Structure`, + :cmd:`Coercion` and :cmd:`Set` (and :cmd:`Unset`), some locality attributes + will be passed on to the :cmd:`Module` containing the current :cmd:`Section`, + see the associated footnotes. + A similar table for :cmd:`Module` can be found :ref:`here `. @@ -157,8 +169,10 @@ A similar table for :cmd:`Module` can be found - :attr:`global` * - :cmd:`Definition`, :cmd:`Lemma`, :cmd:`Axiom`, ... - - :attr:`local` - - available + - available [#note1]_ + - :attr:`local` in + + current module [#note1]_ - ❌ - ❌ @@ -202,13 +216,17 @@ A similar table for :cmd:`Module` can be found - :attr:`global` - not available - ❌ - - available + - :attr:`global` in + + current module [#note2]_ * - :cmd:`Canonical Structure` - :attr:`global` - not available - ❌ - - available + - :attr:`global` in + + current module [#note2]_ * - ``Hints`` (and :cmd:`Instance`) - :attr:`local` @@ -217,10 +235,32 @@ A similar table for :cmd:`Module` can be found - ❌ * - :cmd:`Set` or :cmd:`Unset` a flag - - :attr:`local` - - not available - - available - available + - not available + - :attr:`export` in + + current module [#note3]_ + - :attr:`global` in + + current module [#note3]_ + +.. [#note1] For :cmd:`Definition`, :cmd:`Lemma`, ... the default visibility is + to be available outside the section and available with a short name when + imported outside the current module. The :attr:`local` attribute make the + corresponding identifiers available in the current module but only with a + fully qualified name outside the current module. + +.. [#note2] For :cmd:`Coercion` and :cmd:`Canonical Structure`, the :attr:`global` + visibility, which is the default, makes them available outside the section, + in the current module, and outside the current module when it is imported. + +.. [#note3] For :cmd:`Set` and :cmd:`Unset`, the :attr:`export` and + :attr:`global` attributes both make the command's effects persist outside the + current section, in the current module. It will also persist outside the + current module with the :attr:`global` attribute, or with the :attr:`export` + attribute, when the module is imported. + The default behaviour (no attribute) is to make the setting persist outside + the section in the current module, but not outside the current module. .. _Admissible-rules-for-global-environments: