diff options
| author | Théo Zimmermann | 2020-01-10 14:14:04 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-01-10 14:14:04 +0100 |
| commit | ba6ea757c79318a452bc1c044e140ebade6b224c (patch) | |
| tree | 98fbe0f4dadfda41245bc801aee92f83bd69b70f | |
| parent | 68f6523fa4752aa8d449a0d7a1660f1963c1ea5c (diff) | |
| parent | 1c950aa1b022fd338765b57dacf853dd96941ae4 (diff) | |
Merge PR #11387: [refman] missing space in "Controlling the locality of commands"
Reviewed-by: Zimmi48
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 89b24ea8a3..a38c26c2b3 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1200,7 +1200,7 @@ Controlling the locality of commands + Commands whose default behavior is to extend their effect outside sections but not outside modules when they occur in a section and to extend their effect outside the module or library file they occur in - when no section contains them.For these commands, the Local modifier + when no section contains them. For these commands, the Local modifier limits the effect to the current section or module while the Global modifier extends the effect outside the module even when the command occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this |