From 0b12bb8c03b0ac7cc8aa7578a8db8ca93ecd1fd0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 5 Nov 2020 13:17:38 +0100
Subject: Documenting one-line verbatim.

---
 doc/sphinx/using/tools/coqdoc.rst | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'doc/sphinx/using')

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
-- 
cgit v1.2.3