diff options
| author | coqbot-app[bot] | 2020-10-25 20:00:32 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-25 20:00:32 +0000 |
| commit | a12112c15cdcb0467d4cf5f5a7cfa639852ccd49 (patch) | |
| tree | 3e2d8983efe06e93cbfab75a65b4f4420525332a /doc/sphinx/language/core/basic.rst | |
| parent | d397f10bf4d334189523e187b2cd5fd6e18b4bcc (diff) | |
| parent | 7a57a23e4fb8a74e8746d4eaee900f2ced37a28a (diff) | |
Merge PR #12936: Convert misc chapters to prodn, update syntax
Reviewed-by: Zimmi48
Ack-by: mattam82
Ack-by: pi8027
Ack-by: herbelin
Ack-by: gares
Ack-by: fajb
Ack-by: proux01
Diffstat (limited to 'doc/sphinx/language/core/basic.rst')
| -rw-r--r-- | doc/sphinx/language/core/basic.rst | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index b1f7646be0..29a2b40162 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -325,10 +325,10 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types boldface label "Command:". Commands are listed in the :ref:`command_index`. Example: - .. cmd:: Comments {* @string } + .. cmd:: Comments {* {| @one_term | @string | @natural } } - This command prints "Comments ok" and does not change anything - to the state of the document. + Prints "Comments ok" and does not change + the state of the document. tactic |