diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/coqdoc.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex index 63594a18f9..0e3cab3e61 100644 --- a/doc/refman/coqdoc.tex +++ b/doc/refman/coqdoc.tex @@ -104,7 +104,7 @@ combinations, e.g. \paragraph{Sections.} Sections are introduced by 1 to 4 leading stars (i.e. at the beginning of the -line). One star is a section, two stars a sub-section, etc. +line) followed by a space. One star is a section, two stars a sub-section, etc. The section title is given on the remaining of the line. Example: \begin{verbatim} @@ -152,7 +152,7 @@ escape sequences: \paragraph{Verbatim.} Verbatim material is introduced by a leading \verb+<<+ and closed by -\verb+>>+. Example: +\verb+>>+ at the beginning of a line. Example: \begin{verbatim} Here is the corresponding caml code: << |