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:03 +0200 |
| commit | bea89948b3b9d508726b52a4e2fed3fa843717ef (patch) | |
| tree | 2514e067b489276d8f642c6cdff3f8afc2f71cf0 /doc/sphinx/proof-engine/vernacular-commands.rst | |
| parent | 963f07af424df45e09064bc8c8600c34e369f772 (diff) | |
Clean-up around options.
- Remove all trailing dots.
- There is only one Bullet Behavior option.
- Replaces `@natural` and `@integer` by `@num`.
Diffstat (limited to 'doc/sphinx/proof-engine/vernacular-commands.rst')
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 692ff294a..672c7a0fe 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1131,13 +1131,13 @@ Controlling display :cmd:`SearchPattern`, :cmd:`SearchRewrite` etc. to omit types from their output, printing only identifiers. -.. opt:: Printing Width @integer +.. opt:: Printing Width @num This command sets which left-aligned part of the width of the screen is used for display. At the time of writing this documentation, the default value is 78. -.. opt:: Printing Depth @integer +.. opt:: Printing Depth @num This option controls the nesting depth of the formatter used for pretty- printing. Beyond this depth, display of subterms is replaced by dots. At the |