diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-04-24 11:59:49 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-05 11:54:02 +0200 |
| commit | 75715450906ffbf65a4f7a9f92031dd00ac96ead (patch) | |
| tree | b447b2767c40f4cf5fd4539e336d8029fb93babe /doc/sphinx/practical-tools | |
| parent | dd9a54e1e3cc81e2efd92303f0f7249064e68ea4 (diff) | |
[sphinx] Fix a typo that appeared during the migration.
Diffstat (limited to 'doc/sphinx/practical-tools')
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 93dcfca4b..83dddab4f 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 |