Remove funind tactics from Tactics chapter.

1 files changed, 1 insertions, 90 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 19573eee43..533dfb44cd 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -2099,60 +2099,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
 See also the larger example of :tacn:`dependent induction`
 and an explanation of the underlying technique.
 
-.. tacn:: function induction (@qualid {+ @term})
-   :name: function 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`).
-   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.
-
-.. seealso:: :ref:`advanced-recursive-functions`, :ref:`functional-scheme` and :tacn:`inversion`
-
-.. exn:: Cannot find induction information on @qualid.
-   :undocumented:
-
-.. exn:: Not the right number of induction arguments.
-   :undocumented:
+.. seealso:: :tacn:`function induction`
 
 .. tacv:: functional induction (@qualid {+ @term}) as @simple_intropattern using @term with @bindings_list
 
@@ -4597,42 +4544,6 @@ symbol :g:`=`.
    Analogous to :tacn:`dependent rewrite ->` but uses the equality from right to
    left.
 
-Inversion
----------
-
-.. 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``.
-
-   .. exn:: Hypothesis @ident must contain at least one Function.
-      :undocumented:
-
-   .. exn:: Cannot find inversion information for hypothesis @ident.
-
-      This error may be raised when some inversion lemma failed to be generated by
-      Function.
-
-
-   .. tacv:: functional inversion @num
-
-      This does the same thing as :n:`intros until @num` followed by
-      :n:`functional inversion @ident` where :token:`ident` is the
-      identifier for the last introduced hypothesis.
-
-   .. tacv:: functional inversion @ident @qualid
-             functional inversion @num @qualid
-
-      If the hypothesis :token:`ident` (or :token:`num`) 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.
-
 Classical tactics
 -----------------