diff options
| author | Jim Fehrle | 2018-09-01 12:39:09 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2018-09-20 18:27:08 -0700 |
| commit | ec7dd674ea25dfd36c007bb863fed63ce8d31ff2 (patch) | |
| tree | 2f73dd477ac9276ba8ed9409aab613370d29c7fb /doc/sphinx/addendum/omega.rst | |
| parent | d4b5de427d94d82f09d58e0f1095f052a5900914 (diff) | |
Rewrite "Flags, Options and Tables" section.
Mark boolean-valued options with :flag:
Adjust tactic and command names so parameters aren't shown in the index unless
they're needed for disambiguation.
Remove references to synchronous options.
Revise doc for tables.
Correct indentation for text below :flag:
Diffstat (limited to 'doc/sphinx/addendum/omega.rst')
| -rw-r--r-- | doc/sphinx/addendum/omega.rst | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index f7a431ef29..828505b850 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -116,23 +116,23 @@ loaded by Options ------- -.. opt:: Stable Omega +.. flag:: Stable Omega .. deprecated:: 8.5 This deprecated option (on by default) is for compatibility with Coq pre 8.5. It resets internal name counters to make executions of :tacn:`omega` independent. -.. opt:: Omega UseLocalDefs +.. flag:: Omega UseLocalDefs This option (on by default) allows :tacn:`omega` to use the bodies of local variables. -.. opt:: Omega System +.. flag:: Omega System This option (off by default) activate the printing of debug information -.. opt:: Omega Action +.. flag:: Omega Action This option (off by default) activate the printing of debug information |