diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-04-24 17:38:24 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-05 11:54:05 +0200 |
| commit | c686096482d296b96abfb852a2b24673fb8ec1e0 (patch) | |
| tree | 6c5065db3c24f8d7612b4922947fb8f30c2a6421 /doc/sphinx/addendum | |
| parent | bee08aaa00749cb2a953537a505239eaeabd1de9 (diff) | |
[sphinx] Re-indent to get much better rendering.
Add some more cmd references.
And use deprecated directives.
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/omega.rst | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index 1e9d2aa1e..009efd0d2 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -115,21 +115,23 @@ Options .. opt:: Stable Omega -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. + .. 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 -This option (on by default) allows :tacn:`omega` to use the bodies of local -variables. + This option (on by default) allows :tacn:`omega` to use the bodies of local + variables. .. opt:: Omega System -This option (off by default) activate the printing of debug information + This option (off by default) activate the printing of debug information .. opt:: Omega Action -This option (off by default) activate the printing of debug information + This option (off by default) activate the printing of debug information Technical data -------------- |