Remove Functional Scheme from Scheme chapter.

1 files changed, 1 insertions, 140 deletions

diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index 34197c4fcf..e05be7c2c2 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -190,146 +190,7 @@ Combined Scheme
 
      Check tree_forest_mutrect.
 
-.. _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}
-
-   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'`.
-
-.. warning::
-
-   There is a difference between induction schemes generated by the command
-   :cmd:`Functional Scheme` and these generated by the :cmd:`Function`. Indeed,
-   :cmd:`Function` generally produces smaller principles that are closer to how
-   a user would implement them. See :ref:`advanced-recursive-functions` for details.
-
-.. example::
-
-  Induction scheme for div2.
-
-  We define the function div2 as follows:
-
-  .. coqtop:: all
-
-   Require Import FunInd.
-   Require Import Arith.
-
-   Fixpoint div2 (n:nat) : nat :=
-   match n with
-   | O => 0
-   | S O => 0
-   | S (S n') => S (div2 n')
-   end.
-
-  The definition of a principle of induction corresponding to the
-  recursive structure of `div2` is defined by the command:
-
-  .. coqtop:: all
-
-    Functional Scheme div2_ind := Induction for div2 Sort Prop.
-
-  You may now look at the type of div2_ind:
-
-  .. coqtop:: all
-
-    Check div2_ind.
-
-  We can now prove the following lemma using this principle:
-
-  .. coqtop:: all
-
-    Lemma div2_le' : forall n:nat, div2 n <= n.
-    intro n.
-    pattern n, (div2 n).
-    apply div2_ind; intros.
-    auto with arith.
-    auto with arith.
-    simpl; auto with arith.
-    Qed.
-
-  We can use directly the functional induction (:tacn:`function induction`) tactic instead
-  of the pattern/apply trick:
-
-  .. coqtop:: all
-
-    Reset div2_le'.
-
-    Lemma div2_le : forall n:nat, div2 n <= n.
-    intro n.
-    functional induction (div2 n).
-    auto with arith.
-    auto with arith.
-    auto with arith.
-    Qed.
-
-.. example::
-
-  Induction scheme for tree_size.
-
-  We define trees by the following mutual inductive type:
-
-  .. original LaTeX had "Variable" instead of "Axiom", which generates an ugly warning
-
-  .. coqtop:: reset all
-
-     Axiom A : Set.
-
-     Inductive tree : Set :=
-     node : A -> forest -> tree
-     with forest : Set :=
-     | empty : forest
-     | cons : tree -> forest -> forest.
-
-  We define the function tree_size that computes the size of a tree or a
-  forest. Note that we use ``Function`` which generally produces better
-  principles.
-
-  .. coqtop:: all
-
-    Require Import FunInd.
-
-    Function tree_size (t:tree) : nat :=
-    match t with
-    | node A f => S (forest_size f)
-    end
-    with forest_size (f:forest) : nat :=
-    match f with
-    | empty => 0
-    | cons t f' => (tree_size t + forest_size f')
-    end.
-
-  Notice that the induction principles ``tree_size_ind`` and ``forest_size_ind``
-  generated by ``Function`` are not mutual.
-
-  .. coqtop:: all
-
-    Check tree_size_ind.
-
-  Mutual induction principles following the recursive structure of ``tree_size``
-  and ``forest_size`` can be generated by the following command:
-
-  .. coqtop:: all
-
-    Functional Scheme tree_size_ind2 := Induction for tree_size Sort Prop
-    with forest_size_ind2 := Induction for forest_size Sort Prop.
-
-  You may now look at the type of `tree_size_ind2`:
-
-  .. coqtop:: all
-
-    Check tree_size_ind2.
+.. seealso:: :ref:`functional-scheme`
 
 .. _derive-inversion: