Prelude : no more autoload of plugins extraction and recdef

 The user now has to manually load them, respectively via:
   Require Extraction
   Require Import FunInd

 The "Import" in the case of FunInd is to ensure that the
 tactics functional induction and functional inversion are indeed
 in scope.

 Note that the Recdef.v file is still there as well (it contains
 complements used when doing Function with measures), and it also
 triggers a load of FunInd.v.

 This change is correctly documented in the refman, and the test-suite
 has been adapted.

4 files changed, 22 insertions, 7 deletions

diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index 01dbcfb1c..fa3d61b1c 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -19,6 +19,12 @@ be used (abusively) to refer to any of the three.
 %% the one in previous versions of \Coq: there is no more
 %% an explicit toplevel for the language (formerly called \textsc{Fml}). 
 
+Before using any of the commands or options described in this chapter,
+the extraction framework should first be loaded explicitly
+via {\tt Require Extraction}. Note that in earlier versions of Coq, these
+commands and options were directly available without any preliminary
+{\tt Require}.
+
 \asection{Generating ML code}
 \comindex{Extraction}
 \comindex{Recursive Extraction}
@@ -501,6 +507,7 @@ We can now extract this program to \ocaml:
 Reset Initial.
 \end{coq_eval}
 \begin{coq_example}
+Require Extraction.
 Require Import Euclid Wf_nat.
 Extraction Inline gt_wf_rec lt_wf_rec induction_ltof2.
 Recursive Extraction eucl_dev.
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 6dd0ddf81..939fc87a6 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -721,18 +721,20 @@ a given type. See Section~\ref{Show}.
 
 \section{Advanced recursive functions}
 
-The \emph{experimental} command 
+The following \emph{experimental} command is available
+when the {\tt FunInd} library has been loaded via {\tt Require Import FunInd}:
 \begin{center}
    \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
      \{decrease\_annot\} : type$_0$ := \term$_0$}
    \comindex{Function}
    \label{Function}
 \end{center}
-can be seen as a generalization of {\tt Fixpoint}.  It is actually a
-wrapper for several ways of defining a function \emph{and other useful
+This command can be seen as a generalization of {\tt Fixpoint}.  It is actually
+a wrapper for several ways of defining a function \emph{and other useful
   related objects}, namely: an induction principle that reflects the
 recursive structure of the function (see \ref{FunInduction}), and its
-fixpoint equality.  The meaning of this
+fixpoint equality.
+ The meaning of this
 declaration is to define a function {\it ident}, similarly to {\tt
   Fixpoint}. Like in {\tt Fixpoint}, the decreasing argument must be
 given (unless the function is not recursive), but it must not
diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex
index 53aa6b86a..d3719bed4 100644
--- a/doc/refman/RefMan-sch.tex
+++ b/doc/refman/RefMan-sch.tex
@@ -196,8 +196,10 @@ Check tree_forest_mutind.
 
 The {\tt Functional Scheme} command is a high-level experimental
 tool for generating automatically induction principles
-corresponding to (possibly mutually recursive) functions.  Its
-syntax follows the schema:
+corresponding to (possibly mutually recursive) functions.
+First, it must be made available via {\tt Require Import FunInd}.
+ Its
+syntax then follows the schema:
 \begin{quote}
 {\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\
   with\\
@@ -319,6 +321,7 @@ of a tree or a forest. Note that we use \texttt{Function} which
 generally produces better principles.
 
 \begin{coq_example*}
+Require Import FunInd.
 Function tree_size (t:tree) : nat :=
   match t with
   | node A f => S (forest_size f)
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 253eb7f01..2bab04e90 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2113,13 +2113,15 @@ The tactic \texttt{functional induction} performs
 case analysis and induction following the definition of a function. It
 makes use of a principle generated by \texttt{Function}
 (see Section~\ref{Function}) or \texttt{Functional Scheme}
-(see Section~\ref{FunScheme}).
+(see Section~\ref{FunScheme}). Note that this tactic is only available
+after a {\tt Require Import FunInd}.
 
 \begin{coq_eval}
 Reset Initial.
 Import Nat.
 \end{coq_eval}
 \begin{coq_example}
+Require Import FunInd.
 Functional Scheme minus_ind := Induction for minus Sort Prop.
 Check minus_ind.
 Lemma le_minus (n m:nat) : n - m <= n.
@@ -4797,6 +4799,7 @@ that performs inversion on hypothesis {\ident} of the form
 \texttt{\qualid\ \term$_1$\dots\term$_n$\ = \term} or \texttt{\term\ =
   \qualid\ \term$_1$\dots\term$_n$} where \qualid\ must have been
 defined using \texttt{Function} (see Section~\ref{Function}).
+Note that this tactic is only available after a {\tt Require Import FunInd}.
 
 \begin{ErrMsgs}
 \item \errindex{Hypothesis {\ident} must contain at least one Function}