diff options
Diffstat (limited to 'doc/sphinx/using/tools')
| -rw-r--r-- | doc/sphinx/using/tools/coqdoc.rst | 6 |
1 files changed, 3 insertions, 3 deletions
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. |