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.

49 files changed, 111 insertions, 17 deletions

diff --git a/Makefile.dev b/Makefile.dev
index 0105df972..b0299bd16 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -186,7 +186,7 @@ omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO)
 micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT)
 setoid_ring: $(RINGVO) $(RINGCMO)
 nsatz: $(NSATZVO) $(NSATZCMO)
-extraction: $(EXTRACTIONCMO)
+extraction: $(EXTRACTIONCMO) $(EXTRACTIONVO)
 fourier: $(FOURIERVO) $(FOURIERCMO)
 funind: $(FUNINDCMO) $(FUNINDVO)
 cc: $(CCVO) $(CCCMO)
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}
diff --git a/plugins/extraction/ExtrHaskellBasic.v b/plugins/extraction/ExtrHaskellBasic.v
index 294d61023..d08a81da6 100644
--- a/plugins/extraction/ExtrHaskellBasic.v
+++ b/plugins/extraction/ExtrHaskellBasic.v
@@ -1,5 +1,7 @@
 (** Extraction to Haskell : use of basic Haskell types *)
 
+Require Coq.extraction.Extraction.
+
 Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
 Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
 Extract Inductive unit => "()" [ "()" ].
diff --git a/plugins/extraction/ExtrHaskellNatInt.v b/plugins/extraction/ExtrHaskellNatInt.v
index e94e7d42b..267322d9e 100644
--- a/plugins/extraction/ExtrHaskellNatInt.v
+++ b/plugins/extraction/ExtrHaskellNatInt.v
@@ -1,5 +1,7 @@
 (** Extraction of [nat] into Haskell's [Int] *)
 
+Require Coq.extraction.Extraction.
+
 Require Import Arith.
 Require Import ExtrHaskellNatNum.
 
diff --git a/plugins/extraction/ExtrHaskellNatInteger.v b/plugins/extraction/ExtrHaskellNatInteger.v
index 038f0ed81..4c5c71f58 100644
--- a/plugins/extraction/ExtrHaskellNatInteger.v
+++ b/plugins/extraction/ExtrHaskellNatInteger.v
@@ -1,5 +1,7 @@
 (** Extraction of [nat] into Haskell's [Integer] *)
 
+Require Coq.extraction.Extraction.
+
 Require Import Arith.
 Require Import ExtrHaskellNatNum.
 
diff --git a/plugins/extraction/ExtrHaskellNatNum.v b/plugins/extraction/ExtrHaskellNatNum.v
index 244eb85fc..fabe9a4c6 100644
--- a/plugins/extraction/ExtrHaskellNatNum.v
+++ b/plugins/extraction/ExtrHaskellNatNum.v
@@ -6,6 +6,8 @@
  * implements [Num].
  *)
 
+Require Coq.extraction.Extraction.
+
 Require Import Arith.
 Require Import EqNat.
 
diff --git a/plugins/extraction/ExtrHaskellString.v b/plugins/extraction/ExtrHaskellString.v
index 3558f4f25..ac1f6f913 100644
--- a/plugins/extraction/ExtrHaskellString.v
+++ b/plugins/extraction/ExtrHaskellString.v
@@ -2,6 +2,8 @@
  * Special handling of ascii and strings for extraction to Haskell.
  *)
 
+Require Coq.extraction.Extraction.
+
 Require Import Ascii.
 Require Import String.
 
diff --git a/plugins/extraction/ExtrHaskellZInt.v b/plugins/extraction/ExtrHaskellZInt.v
index 66690851a..0345ffc4e 100644
--- a/plugins/extraction/ExtrHaskellZInt.v
+++ b/plugins/extraction/ExtrHaskellZInt.v
@@ -1,5 +1,7 @@
 (** Extraction of [Z] into Haskell's [Int] *)
 
+Require Coq.extraction.Extraction.
+
 Require Import ZArith.
 Require Import ExtrHaskellZNum.
 
diff --git a/plugins/extraction/ExtrHaskellZInteger.v b/plugins/extraction/ExtrHaskellZInteger.v
index f192f16ee..f7f9e2f80 100644
--- a/plugins/extraction/ExtrHaskellZInteger.v
+++ b/plugins/extraction/ExtrHaskellZInteger.v
@@ -1,5 +1,7 @@
 (** Extraction of [Z] into Haskell's [Integer] *)
 
+Require Coq.extraction.Extraction.
+
 Require Import ZArith.
 Require Import ExtrHaskellZNum.
 
diff --git a/plugins/extraction/ExtrHaskellZNum.v b/plugins/extraction/ExtrHaskellZNum.v
index cbbfda75e..4141bd203 100644
--- a/plugins/extraction/ExtrHaskellZNum.v
+++ b/plugins/extraction/ExtrHaskellZNum.v
@@ -6,6 +6,8 @@
  * implements [Num].
  *)
 
+Require Coq.extraction.Extraction.
+
 Require Import ZArith.
 Require Import EqNat.
 
diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v
index d9b000c2a..dfdc49863 100644
--- a/plugins/extraction/ExtrOcamlBasic.v
+++ b/plugins/extraction/ExtrOcamlBasic.v
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+Require Coq.extraction.Extraction.
+
 (** Extraction to Ocaml : use of basic Ocaml types *)
 
 Extract Inductive bool => bool [ true false ].
diff --git a/plugins/extraction/ExtrOcamlBigIntConv.v b/plugins/extraction/ExtrOcamlBigIntConv.v
index c42938c8e..78ee46085 100644
--- a/plugins/extraction/ExtrOcamlBigIntConv.v
+++ b/plugins/extraction/ExtrOcamlBigIntConv.v
@@ -13,6 +13,8 @@
     simplifies the use of [Big_int] (it can be found in the sources
     of Coq). *)
 
+Require Coq.extraction.Extraction.
+
 Require Import Arith ZArith.
 
 Parameter bigint : Type.
diff --git a/plugins/extraction/ExtrOcamlIntConv.v b/plugins/extraction/ExtrOcamlIntConv.v
index 515fa52df..fcfea352a 100644
--- a/plugins/extraction/ExtrOcamlIntConv.v
+++ b/plugins/extraction/ExtrOcamlIntConv.v
@@ -10,6 +10,8 @@
 
     Nota: no check that [int] values aren't generating overflows *)
 
+Require Coq.extraction.Extraction.
+
 Require Import Arith ZArith.
 
 Parameter int : Type.
diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/plugins/extraction/ExtrOcamlNatBigInt.v
index 3149e7029..e0837be62 100644
--- a/plugins/extraction/ExtrOcamlNatBigInt.v
+++ b/plugins/extraction/ExtrOcamlNatBigInt.v
@@ -8,6 +8,8 @@
 
 (** Extraction of [nat] into Ocaml's [big_int] *)
 
+Require Coq.extraction.Extraction.
+
 Require Import Arith Even Div2 EqNat Euclid.
 Require Import ExtrOcamlBasic.
 
diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v
index 7c607f7ae..80da72d43 100644
--- a/plugins/extraction/ExtrOcamlNatInt.v
+++ b/plugins/extraction/ExtrOcamlNatInt.v
@@ -8,6 +8,8 @@
 
 (** Extraction of [nat] into Ocaml's [int] *)
 
+Require Coq.extraction.Extraction.
+
 Require Import Arith Even Div2 EqNat Euclid.
 Require Import ExtrOcamlBasic.
 
diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v
index 6af591eed..64ca6c85d 100644
--- a/plugins/extraction/ExtrOcamlString.v
+++ b/plugins/extraction/ExtrOcamlString.v
@@ -8,6 +8,8 @@
 
 (* Extraction to Ocaml : special handling of ascii and strings *)
 
+Require Coq.extraction.Extraction.
+
 Require Import Ascii String.
 
 Extract Inductive ascii => char
diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v
index c9e8eac0c..66f188c84 100644
--- a/plugins/extraction/ExtrOcamlZBigInt.v
+++ b/plugins/extraction/ExtrOcamlZBigInt.v
@@ -8,6 +8,8 @@
 
 (** Extraction of [positive], [N] and [Z] into Ocaml's [big_int] *)
 
+Require Coq.extraction.Extraction.
+
 Require Import ZArith NArith.
 Require Import ExtrOcamlBasic.
 
diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v
index 4d33174b3..c93cfb9d4 100644
--- a/plugins/extraction/ExtrOcamlZInt.v
+++ b/plugins/extraction/ExtrOcamlZInt.v
@@ -8,6 +8,8 @@
 
 (** Extraction of [positive], [N] and [Z] into Ocaml's [int] *)
 
+Require Coq.extraction.Extraction.
+
 Require Import ZArith NArith.
 Require Import ExtrOcamlBasic.
 
diff --git a/plugins/extraction/Extraction.v b/plugins/extraction/Extraction.v
new file mode 100644
index 000000000..ab1416b1d
--- /dev/null
+++ b/plugins/extraction/Extraction.v
@@ -0,0 +1,9 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Declare ML Module "extraction_plugin".
\ No newline at end of file
diff --git a/plugins/funind/FunInd.v b/plugins/funind/FunInd.v
new file mode 100644
index 000000000..e40aea776
--- /dev/null
+++ b/plugins/funind/FunInd.v
@@ -0,0 +1,10 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Coq.extraction.Extraction.
+Declare ML Module "recdef_plugin".
diff --git a/plugins/funind/Recdef.v b/plugins/funind/Recdef.v
index e4433247b..c6fcd647f 100644
--- a/plugins/funind/Recdef.v
+++ b/plugins/funind/Recdef.v
@@ -6,8 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+Require Import Coq.funind.FunInd.
 Require Import PeanoNat.
-
 Require Compare_dec.
 Require Wf_nat.
 
diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index 135a71520..95f135c8f 100644
--- a/plugins/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.v
@@ -14,6 +14,7 @@
 
 (* Used to generate micromega.ml *)
 
+Require Extraction.
 Require Import ZMicromega.
 Require Import QMicromega.
 Require Import RMicromega.
diff --git a/test-suite/bugs/closed/2141.v b/test-suite/bugs/closed/2141.v
index 941ae530f..098a7e9e7 100644
--- a/test-suite/bugs/closed/2141.v
+++ b/test-suite/bugs/closed/2141.v
@@ -1,3 +1,4 @@
+Require Coq.extraction.Extraction.
 Require Import FSetList.
 Require Import OrderedTypeEx.
 
diff --git a/test-suite/bugs/closed/3287.v b/test-suite/bugs/closed/3287.v
index 7c7813125..1b758acd7 100644
--- a/test-suite/bugs/closed/3287.v
+++ b/test-suite/bugs/closed/3287.v
@@ -1,3 +1,5 @@
+Require Coq.extraction.Extraction.
+
 Module Foo.
 (* Definition foo := (I,I). *)
 Definition bar := true.
diff --git a/test-suite/bugs/closed/3923.v b/test-suite/bugs/closed/3923.v
index 0aa029e73..2fb0a5439 100644
--- a/test-suite/bugs/closed/3923.v
+++ b/test-suite/bugs/closed/3923.v
@@ -1,3 +1,5 @@
+Require Coq.extraction.Extraction.
+
 Module Type TRIVIAL.
 Parameter t:Type.
 End TRIVIAL.
diff --git a/test-suite/bugs/closed/4616.v b/test-suite/bugs/closed/4616.v
index c862f8206..a59975dbc 100644
--- a/test-suite/bugs/closed/4616.v
+++ b/test-suite/bugs/closed/4616.v
@@ -1,3 +1,5 @@
+Require Coq.extraction.Extraction.
+
 Set Primitive Projections.
 Record Foo' := Foo { foo : Type }.
 Axiom f : forall t : Foo', foo t.
diff --git a/test-suite/bugs/closed/4710.v b/test-suite/bugs/closed/4710.v
index fdc850109..5d8ca330a 100644
--- a/test-suite/bugs/closed/4710.v
+++ b/test-suite/bugs/closed/4710.v
@@ -1,3 +1,5 @@
+Require Coq.extraction.Extraction.
+
 Set Primitive Projections.
 Record Foo' := Foo { foo : nat }.
 Extraction foo.
diff --git a/test-suite/bugs/closed/5372.v b/test-suite/bugs/closed/5372.v
index 2dc78d4c7..e60244cd1 100644
--- a/test-suite/bugs/closed/5372.v
+++ b/test-suite/bugs/closed/5372.v
@@ -1,4 +1,5 @@
 (* coq bug 5372: https://coq.inria.fr/bugs/show_bug.cgi?id=5372 *)
+Require Import FunInd.
 Function odd (n:nat) :=
   match n with
   | 0 => false
diff --git a/test-suite/ide/blocking-futures.fake b/test-suite/ide/blocking-futures.fake
index b63f09bcf..541fb798c 100644
--- a/test-suite/ide/blocking-futures.fake
+++ b/test-suite/ide/blocking-futures.fake
@@ -4,6 +4,7 @@
 # Extraction will force the future computation, assert it is blocking
 # Example courtesy of Jonathan (jonikelee)
 #
+ADD { Require Coq.extraction.Extraction. }
 ADD { Require Import List. }
 ADD { Import ListNotations. }
 ADD { Definition myrev{A}(l : list A) : {rl : list A | rl = rev l}. }
diff --git a/test-suite/output/Extraction_matchs_2413.v b/test-suite/output/Extraction_matchs_2413.v
index 6c514b16e..1ecd9771e 100644
--- a/test-suite/output/Extraction_matchs_2413.v
+++ b/test-suite/output/Extraction_matchs_2413.v
@@ -1,5 +1,7 @@
 (** Extraction : tests of optimizations of pattern matching *)
 
+Require Coq.extraction.Extraction.
+
 (** First, a few basic tests *)
 
 Definition test1 b :=
diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v
index 3bf97c131..f87f2e2a9 100644
--- a/test-suite/success/Funind.v
+++ b/test-suite/success/Funind.v
@@ -1,4 +1,6 @@
 
+Require Import Coq.funind.FunInd.
+
 Definition iszero (n : nat) : bool :=
   match n with
   | O => true
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index d8f804246..841940492 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -147,6 +147,7 @@ Proof.
  intros; absurd (p < p); eauto with arith.
 Qed.
 
+Require Coq.extraction.Extraction.
 Extraction max.
 
 
diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v
index 0086e090b..89be14415 100644
--- a/test-suite/success/extraction.v
+++ b/test-suite/success/extraction.v
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+Require Coq.extraction.Extraction.
 Require Import Arith.
 Require Import List.
 
diff --git a/test-suite/success/extraction_dep.v b/test-suite/success/extraction_dep.v
index 11bb25fda..e770cf779 100644
--- a/test-suite/success/extraction_dep.v
+++ b/test-suite/success/extraction_dep.v
@@ -1,6 +1,8 @@
 
 (** Examples of code elimination inside modules during extraction *)
 
+Require Coq.extraction.Extraction.
+
 (** NB: we should someday check the produced code instead of
     simply running the commands. *)
 
diff --git a/test-suite/success/extraction_impl.v b/test-suite/success/extraction_impl.v
index dfdeff82f..5bf807b1c 100644
--- a/test-suite/success/extraction_impl.v
+++ b/test-suite/success/extraction_impl.v
@@ -4,6 +4,8 @@
 (** NB: we should someday check the produced code instead of
     simply running the commands. *)
 
+Require Coq.extraction.Extraction.
+
 (** Bug #4243, part 1 *)
 
 Inductive dnat : nat -> Type :=
diff --git a/test-suite/success/extraction_polyprop.v b/test-suite/success/extraction_polyprop.v
index 7215bd990..936d838c5 100644
--- a/test-suite/success/extraction_polyprop.v
+++ b/test-suite/success/extraction_polyprop.v
@@ -3,6 +3,8 @@
    code that segfaults. See Table.error_singleton_become_prop
    or S. Glondu's thesis for more details. *)
 
+Require Coq.extraction.Extraction.
+
 Definition f {X} (p : (nat -> X) * True) : X * nat :=
   (fst p 0, 0).
 
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 2fa770494..789854b2d 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -181,6 +181,8 @@ Record wrap (A : Type) := { unwrap : A; unwrap2 : A }.
 
 Definition term (x : wrap nat) := x.(unwrap).
 Definition term' (x : wrap nat) := let f := (@unwrap2 nat) in f x.
+
+Require Coq.extraction.Extraction.
 Recursive Extraction term term'.
 (*Unset Printing Primitive Projection Parameters.*)
 
diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v
index 64ba6b1e3..b30ad1af8 100644
--- a/theories/Compat/Coq85.v
+++ b/theories/Compat/Coq85.v
@@ -34,3 +34,6 @@ Global Unset Typeclasses Filtered Unification.
 
 (** Allow silently letting unification constraints float after a "." *)
 Global Unset Solve Unification Constraints.
+
+Require Export Coq.extraction.Extraction.
+Require Export Coq.funind.FunInd.
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index c9e5b8dd2..4a790296b 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -16,7 +16,7 @@
     See the comments at the beginning of FSetAVL for more details.
 *)
 
-Require Import FMapInterface FMapList ZArith Int.
+Require Import FunInd FMapInterface FMapList ZArith Int.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v
index a7be32328..b8e362f15 100644
--- a/theories/FSets/FMapFullAVL.v
+++ b/theories/FSets/FMapFullAVL.v
@@ -25,7 +25,7 @@
 
 *)
 
-Require Import Recdef FMapInterface FMapList ZArith Int FMapAVL ROmega.
+Require Import FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL ROmega.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index 5acdb7eb7..aadef476d 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -12,7 +12,7 @@
  [FMapInterface.S] using lists of pairs ordered (increasing) with respect to
  left projection. *)
 
-Require Import FMapInterface.
+Require Import FunInd FMapInterface.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index 130cbee87..812409702 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -11,7 +11,7 @@
 (** This file proposes an implementation of the non-dependent interface
  [FMapInterface.WS] using lists of pairs, unordered but without redundancy. *)
 
-Require Import FMapInterface.
+Require Import FunInd FMapInterface.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index e71a8774e..28049e9ee 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -18,9 +18,7 @@ Require Export Coq.Init.Tactics.
 Require Export Coq.Init.Tauto.
 (* Initially available plugins
    (+ nat_syntax_plugin loaded in Datatypes) *)
-Declare ML Module "extraction_plugin".
 Declare ML Module "cc_plugin".
 Declare ML Module "ground_plugin".
-Declare ML Module "recdef_plugin".
 (* Default substrings not considered by queries like SearchAbout *)
 Add Search Blacklist "_subproof" "_subterm" "Private_".
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index a3c265a21..b30cb6b56 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -31,7 +31,7 @@
     code after extraction.
 *)
 
-Require Import MSetInterface MSetGenTree BinInt Int.
+Require Import FunInd MSetInterface MSetGenTree BinInt Int.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v
index 154c2384c..036ff1aa4 100644
--- a/theories/MSets/MSetGenTree.v
+++ b/theories/MSets/MSetGenTree.v
@@ -27,7 +27,7 @@
      - min_elt max_elt choose
 *)
 
-Require Import Orders OrdersFacts MSetInterface PeanoNat.
+Require Import FunInd Orders OrdersFacts MSetInterface PeanoNat.
 Local Open Scope list_scope.
 Local Open Scope lazy_bool_scope.
 
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index c490ea516..6e51f6187 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -69,6 +69,7 @@ Section Well_founded.
 
 End Well_founded.
 
+Require Coq.extraction.Extraction.
 Extraction Inline Fix_F_sub Fix_sub.
 
 Set Implicit Arguments.