From 7a57a23e4fb8a74e8746d4eaee900f2ced37a28a Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Sun, 9 Aug 2020 14:25:51 -0700 Subject: Convert misc chapters to prodn --- doc/sphinx/language/core/basic.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'doc/sphinx/language/core/basic.rst') diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 3cc3fe231a..321199f05f 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 ` 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 -- cgit v1.2.3