aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorOlivier Laurent2020-01-10 13:39:28 +0100
committerOlivier Laurent2020-01-10 13:39:28 +0100
commit1c950aa1b022fd338765b57dacf853dd96941ae4 (patch)
treebfde767eb70e639a41c3ea8405d4f8f4b8ae5fa4
parent620986fc66f9c383bc47188f1c3e9320d8437378 (diff)
missing space
-rw-r--r--doc/sphinx/proof-engine/vernacular-commands.rst2
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