[refman] Fix name of tactic: function induction -> functional induction.

1 files changed, 53 insertions, 54 deletions

diff --git a/doc/sphinx/using/libraries/funind.rst b/doc/sphinx/using/libraries/funind.rst
index 179a4df781..40f9eedcf0 100644
--- a/doc/sphinx/using/libraries/funind.rst
+++ b/doc/sphinx/using/libraries/funind.rst
@@ -13,7 +13,7 @@ The following command is available when the ``FunInd`` library has been loaded v
    This command is a generalization of :cmd:`Fixpoint`. It is a wrapper
    for several ways of defining a function *and* other useful related
    objects, namely: an induction principle that reflects the recursive
-   structure of the function (see :tacn:`function induction`) and its fixpoint equality.
+   structure of the function (see :tacn:`functional induction`) and its fixpoint equality.
    This defines a function similar to those defined by :cmd:`Fixpoint`.
    As in :cmd:`Fixpoint`, the decreasing argument must
    be given (unless the function is not recursive), but it might not
@@ -27,7 +27,7 @@ The following command is available when the ``FunInd`` library has been loaded v
    to structurally recursive functions (i.e. when :n:`@fixannot` is a :n:`struct`
    clause).
 
-   See :tacn:`function induction` and :cmd:`Functional Scheme` for how to use
+   See :tacn:`functional induction` and :cmd:`Functional Scheme` for how to use
    the induction principle to reason easily about the function.
 
    The form of the :n:`@fixannot` clause determines which definition mechanism :cmd:`Function` uses.
@@ -166,74 +166,73 @@ terminating functions.
 
    :tacn:`functional inversion` will not be available for the function.
 
-.. seealso:: :ref:`functional-scheme` and :tacn:`function induction`
-
 Tactics
 -------
 
-.. tacn:: function induction (@qualid {+ @term})
-   :name: function induction
+.. tacn:: functional induction (@qualid {+ @term})
+   :name: functional induction
 
    The tactic functional induction performs case analysis and induction
    following the definition of a function. It makes use of a principle
-   generated by ``Function`` (see :ref:`advanced-recursive-functions`) or
-   ``Functional Scheme`` (see :ref:`functional-scheme`).
+   generated by :cmd:`Function` or :cmd:`Functional Scheme`.
    Note that this tactic is only available after a ``Require Import FunInd``.
 
-.. example::
-
-   .. coqtop:: reset all
-
-      Require Import FunInd.
-      Functional Scheme minus_ind := Induction for minus Sort Prop.
-      Check minus_ind.
-      Lemma le_minus (n m:nat) : n - m <= n.
-      functional induction (minus n m) using minus_ind; simpl; auto.
-      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`
-   (by the ``Function`` (see :ref:`advanced-recursive-functions`) or
-   ``Functional Scheme`` (see :ref:`functional-scheme`)
-   command) corresponding to the sort of the goal. Therefore
-   ``functional induction`` may fail if the induction scheme :n:`@qualid` is not
-   defined. See also :ref:`advanced-recursive-functions` for the function
-   terms accepted by ``Function``.
-
-.. note::
-   There is a difference between obtaining an induction scheme
-   for a function by using :g:`Function` (see :ref:`advanced-recursive-functions`)
-   and by using :g:`Functional Scheme` after a normal definition using
-   :g:`Fixpoint` or :g:`Definition`. See :ref:`advanced-recursive-functions`
-   for details.
+   .. example::
+
+      .. coqtop:: reset all
+
+         Require Import FunInd.
+         Functional Scheme minus_ind := Induction for minus Sort Prop.
+         Check minus_ind.
+         Lemma le_minus (n m:nat) : n - m <= n.
+         functional induction (minus n m) using minus_ind; simpl; auto.
+         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`
+      (by the :cmd:`Function` or :cmd:`Functional Scheme` command)
+      corresponding to the sort of the goal. Therefore
+      :tacn:`functional induction` may fail if the induction scheme :n:`@qualid` is not
+      defined.
+
+   .. note::
+      There is a difference between obtaining an induction scheme
+      for a function by using :cmd:`Function`
+      and by using :cmd:`Functional Scheme` after a normal definition using
+      :cmd:`Fixpoint` or :cmd:`Definition`.
+
+   .. exn:: Cannot find induction information on @qualid.
+      :undocumented:
 
-.. seealso:: :ref:`advanced-recursive-functions`, :ref:`functional-scheme` and :tacn:`inversion`
+   .. exn:: Not the right number of induction arguments.
+      :undocumented:
 
-.. exn:: Cannot find induction information on @qualid.
-   :undocumented:
+   .. tacv:: functional induction (@qualid {+ @term}) as @simple_intropattern using @term with @bindings_list
 
-.. exn:: Not the right number of induction arguments.
-   :undocumented:
+      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
    :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 Function (see
-   :ref:`advanced-recursive-functions`). Note that this tactic is only
-   available after a ``Require Import FunInd``.
+   {+ @term}` where :n:`@qualid` must have been defined using :cmd:`Function`.
+   Note that this tactic is only available after a ``Require Import FunInd``.
 
    .. exn:: Hypothesis @ident must contain at least one Function.
       :undocumented:
@@ -328,7 +327,7 @@ Generation of induction principles with ``Functional`` ``Scheme``
     simpl; auto with arith.
     Qed.
 
-  We can use directly the functional induction (:tacn:`function induction`) tactic instead
+  We can use directly the functional induction (:tacn:`functional induction`) tactic instead
   of the pattern/apply trick:
 
   .. coqtop:: all