diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/coqdoc.tex | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex index e00484e6c1..271a13f7f6 100644 --- a/doc/refman/coqdoc.tex +++ b/doc/refman/coqdoc.tex @@ -167,6 +167,8 @@ escape sequences: discarded in \LaTeX\ output. \end{itemize} +Note: to simply output the characters \verb+$+, \verb+%+ and \verb+#+ +and escaping their escaping role, these characters must be doubled. \paragraph{Verbatim.} Verbatim material is introduced by a leading \verb+<<+ and closed by |