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/libraries/funind.rst | 2 --
 doc/sphinx/using/tools/coqdoc.rst     | 6 +++---
 2 files changed, 3 insertions(+), 5 deletions(-)

(limited to 'doc/sphinx/using')

diff --git a/doc/sphinx/using/libraries/funind.rst b/doc/sphinx/using/libraries/funind.rst
index 93571ecebb..0f0edc6bdd 100644
--- a/doc/sphinx/using/libraries/funind.rst
+++ b/doc/sphinx/using/libraries/funind.rst
@@ -170,7 +170,6 @@ Tactics
 -------
 
 .. tacn:: functional induction @term {? using @one_term {? with @bindings } } {? as @simple_intropattern }
-   :name: functional induction
 
    Performs case analysis and induction following the definition of a function
    :token:`qualid`, which must be fully applied to its arguments as part of
@@ -221,7 +220,6 @@ Tactics
       :undocumented:
 
 .. tacn:: functional inversion {| @ident | @natural } {? @qualid }
-   :name: functional inversion
 
    Performs inversion on hypothesis
    :n:`@ident` of the form :n:`@qualid {+ @term} = @term` or
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