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/language/coq-library.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/language/coq-library.rst')
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 320448d46e..85474a3e98 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -618,7 +618,7 @@ Finally, it gives the definition of the usual orderings ``le``, Properties of these relations are not initially known, but may be required by the user from modules ``Le`` and ``Lt``. Finally, -``Peano`` gives some lemmas allowing pattern-matching, and a double +``Peano`` gives some lemmas allowing pattern matching, and a double induction principle. .. index:: |