Convert rewriting and proof-mode chapters to prodn

2 files changed, 3 insertions, 5 deletions

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.