aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/practical-tools
diff options
context:
space:
mode:
authorMaxime Dénès2018-05-07 14:49:10 +0200
committerMaxime Dénès2018-05-07 14:49:10 +0200
commita8985ab0e8cebb8b06ff6680ac65121357448076 (patch)
tree4c4f4175b75ddfb36f3d7f604fd91c8b551bcabf /doc/sphinx/practical-tools
parentbb974290e7d05f1b1159c3add9f68f923ab4e1c4 (diff)
parent3387e130b15ab56220c7bfb211e9f0373448f9f4 (diff)
Merge PR #7301: [sphinx] Backport forgotten updates during the migration & other improvements
Diffstat (limited to 'doc/sphinx/practical-tools')
-rw-r--r--doc/sphinx/practical-tools/coq-commands.rst2
-rw-r--r--doc/sphinx/practical-tools/utilities.rst2
2 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 93dcfca4bf..83dddab4f5 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -171,7 +171,7 @@ and ``coqtop``, unless stated otherwise:
Coq's auto-generated name scheme with names of the form *ident0*, *ident1*,
etc. The command ``Set Mangle Names`` turns the behavior on in a document,
and ``Set Mangle Names Prefix "ident"`` changes the used prefix. This feature
- s intended to be used as a linter for developments that want to be robust to
+ is intended to be used as a linter for developments that want to be robust to
changes in the auto-generated name scheme. The options are provided to
facilitate tracking down problems.
:-compat *version*: Attempt to maintain some backward-compatibility
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 59867988a4..59a88771a0 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -137,7 +137,7 @@ Here we describe only few of them.
(e.g. wrappers)
:COQ_SRC_SUBDIRS:
can be extended by including other paths in which ``*.cm*`` files
- are searched. For example ``COQ\_SRC\_SUBDIRS+=user-contrib/Unicoq``
+ are searched. For example ``COQ_SRC_SUBDIRS+=user-contrib/Unicoq``
lets you build a plugin containing OCaml code that depends on the
OCaml code of ``Unicoq``.