From e02120ed6580733db2276f0c11b4f432ea670ee3 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sat, 12 Sep 2020 20:54:22 -0700
Subject: Convert rewriting and proof-mode chapters to prodn

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

(limited to 'doc/sphinx/using/tools')

diff --git a/doc/sphinx/using/tools/coqdoc.rst b/doc/sphinx/using/tools/coqdoc.rst
index b68b2ed2a7..78ac17bda1 100644
--- a/doc/sphinx/using/tools/coqdoc.rst
+++ b/doc/sphinx/using/tools/coqdoc.rst
@@ -34,9 +34,9 @@ Coq material inside documentation.
 
 Coq material is quoted between the delimiters ``[`` and ``]``. Square brackets
 may be nested, the inner ones being understood as being part of the
-quoted code (thus you can quote a term like ``fun x => u`` by writing  ``[fun
-x => u]``). Inside quotations, the code is pretty-printed in the same
-way as it is in code parts.
+quoted code (thus you can quote a term like ``let id := fun [T : Type] (x : t) => x in id 0``
+by writing  ``[let id := fun [T : Type] (x : t) => x in id 0]``).
+Inside quotations, the code is pretty-printed the same way as in code parts.
 
 Preformatted vernacular is enclosed by ``[[`` and ``]]``. The former must be
 followed by a newline and the latter must follow a newline.
-- 
cgit v1.2.3