Convert misc chapters to prodn

1 files changed, 44 insertions, 50 deletions

diff --git a/doc/sphinx/using/libraries/funind.rst b/doc/sphinx/using/libraries/funind.rst
index 738d64bfc3..93571ecebb 100644
--- a/doc/sphinx/using/libraries/funind.rst
+++ b/doc/sphinx/using/libraries/funind.rst
@@ -169,13 +169,24 @@ terminating functions.
 Tactics
 -------
 
-.. tacn:: functional induction (@qualid {+ @term})
+.. tacn:: functional induction @term {? using @one_term {? with @bindings } } {? as @simple_intropattern }
    :name: functional induction
 
-   The tactic functional induction performs case analysis and induction
-   following the definition of a function. It makes use of a principle
+   Performs case analysis and induction following the definition of a function
+   :token:`qualid`, which must be fully applied to its arguments as part of
+   :token:`term`. It uses a principle
    generated by :cmd:`Function` or :cmd:`Functional Scheme`.
    Note that this tactic is only available after a ``Require Import FunInd``.
+   See the :cmd:`Function` command.
+
+   :n:`using @one_term`
+     Specifies the induction principle (aka elimination scheme).
+
+   :n:`with @bindings`
+     Specifies the arguments of the induction principle.
+
+   :n:`as @simple_intropattern`
+     Provides names for the introduced variables.
 
    .. example::
 
@@ -189,15 +200,6 @@ Tactics
          Qed.
 
    .. note::
-      :n:`(@qualid {+ @term})` must be a correct full application
-      of :n:`@qualid`. In particular, the rules for implicit arguments are the
-      same as usual. For example use :n:`@@qualid` if you want to write implicit
-      arguments explicitly.
-
-   .. note::
-      Parentheses around :n:`@qualid {+ @term}` are not mandatory and can be skipped.
-
-   .. note::
       :n:`functional induction (f x1 x2 x3)` is actually a wrapper for
       :n:`induction x1, x2, x3, (f x1 x2 x3) using @qualid` followed by a cleaning
       phase, where :n:`@qualid` is the induction principle registered for :g:`f`
@@ -218,22 +220,27 @@ Tactics
    .. exn:: Not the right number of induction arguments.
       :undocumented:
 
-   .. tacv:: functional induction (@qualid {+ @term}) as @simple_intropattern using @term with @bindings_list
-
-      Similarly to :tacn:`induction` and :tacn:`elim`, this allows giving
-      explicitly the name of the introduced variables, the induction principle, and
-      the values of dependent premises of the elimination scheme, including
-      *predicates* for mutual induction when :n:`@qualid` is part of a mutually
-      recursive definition.
-
-.. tacn:: functional inversion @ident
+.. tacn:: functional inversion {| @ident | @natural } {? @qualid }
    :name: functional inversion
 
-   :tacn:`functional inversion` is a tactic that performs inversion on hypothesis
-   :n:`@ident` of the form :n:`@qualid {+ @term} = @term` or :n:`@term = @qualid
-   {+ @term}` where :n:`@qualid` must have been defined using :cmd:`Function`.
+   Performs inversion on hypothesis
+   :n:`@ident` of the form :n:`@qualid {+ @term} = @term` or
+   :n:`@term = @qualid {+ @term}` when :n:`@qualid` is defined using :cmd:`Function`.
    Note that this tactic is only available after a ``Require Import FunInd``.
 
+   :n:`@natural`
+     Does the same thing as :n:`intros until @natural` followed by
+     :n:`functional inversion @ident` where :token:`ident` is the
+     identifier for the last introduced hypothesis.
+
+   :n:`@qualid`
+     If the hypothesis :token:`ident` (or :token:`natural`) has a type of the form
+     :n:`@qualid__1 {+ @term__i } = @qualid__2 {+ @term__j }` where
+     :n:`@qualid__1` and :n:`@qualid__2` are valid candidates to
+     functional inversion, this variant allows choosing which :token:`qualid`
+     is inverted.
+
+
    .. exn:: Hypothesis @ident must contain at least one Function.
       :undocumented:
 
@@ -242,39 +249,26 @@ Tactics
       This error may be raised when some inversion lemma failed to be generated by
       Function.
 
-
-   .. tacv:: functional inversion @natural
-
-      This does the same thing as :n:`intros until @natural` followed by
-      :n:`functional inversion @ident` where :token:`ident` is the
-      identifier for the last introduced hypothesis.
-
-   .. tacv:: functional inversion @ident @qualid
-             functional inversion @natural @qualid
-
-      If the hypothesis :token:`ident` (or :token:`natural`) has a type of the form
-      :n:`@qualid__1 {+ @term__i } = @qualid__2 {+ @term__j }` where
-      :n:`@qualid__1` and :n:`@qualid__2` are valid candidates to
-      functional inversion, this variant allows choosing which :token:`qualid`
-      is inverted.
-
 .. _functional-scheme:
 
 Generation of induction principles with ``Functional`` ``Scheme``
 -----------------------------------------------------------------
 
 
-.. cmd:: Functional Scheme @ident__0 := Induction for @ident' Sort @sort {* with @ident__i := Induction for @ident__i' Sort @sort}
+.. cmd:: Functional Scheme @func_scheme_def {* with @func_scheme_def }
+
+   .. insertprodn func_scheme_def func_scheme_def
+
+   .. prodn::
+      func_scheme_def ::= @ident := Induction for @qualid Sort @sort_family
+
+   An experimental high-level tool that
+   automatically generates induction principles corresponding to functions that
+   may be mutually recursive.  The command generates an
+   induction principle named :n:`@ident` for each given function named :n:`@qualid`.
+   The :n:`@qualid`\s must be given in the same order as when they were defined.
 
-   This command is a high-level experimental tool for
-   generating automatically induction principles corresponding to
-   (possibly mutually recursive) functions. First, it must be made
-   available via ``Require Import FunInd``.
-   Each :n:`@ident__i` is a different mutually defined function
-   name (the names must be in the same order as when they were defined). This
-   command generates the induction principle for each :n:`@ident__i`, following
-   the recursive structure and case analyses of the corresponding function
-   :n:`@ident__i'`.
+   Note the command must be made available via :cmd:`Require Import` ``FunInd``.
 
 .. warning::