diff options
Diffstat (limited to 'doc/sphinx/using')
| -rw-r--r-- | doc/sphinx/using/tools/coqdoc.rst | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/doc/sphinx/using/tools/coqdoc.rst b/doc/sphinx/using/tools/coqdoc.rst index 7ab8f9d763..b68b2ed2a7 100644 --- a/doc/sphinx/using/tools/coqdoc.rst +++ b/doc/sphinx/using/tools/coqdoc.rst @@ -200,6 +200,14 @@ at the beginning of a line. if n <= 1 then 1 else n * fact (n-1) >> +Verbatim material on a single line is also possible (assuming that +``>>`` is not part of the text to be presented as verbatim). + +.. example:: + + :: + + Here is the corresponding caml expression: << fact (n-1) >> Hyperlinks |