Merge PR#220: Less init plugins

55 files changed, 168 insertions, 17 deletions

diff --git a/API/API.mli b/API/API.mli
index 20a637c1fa..9714f52b91 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -3307,6 +3307,7 @@ sig
   val declare_cache_obj : (unit -> unit) -> string -> unit
   val add_known_plugin : (unit -> unit) -> string -> unit
   val add_known_module : string -> unit
+  val module_is_known : string -> bool
 end
 
 (* All items in the Proof_type module are deprecated. *)
diff --git a/API/grammar_API.mli b/API/grammar_API.mli
index 44aae771f6..4da5b380fe 100644
--- a/API/grammar_API.mli
+++ b/API/grammar_API.mli
@@ -211,6 +211,7 @@ end
 module Mltop :
 sig
   val add_known_module : string -> unit
+  val module_is_known : string -> bool
   val declare_cache_obj : (unit -> unit) -> string -> unit
 end
 module Vernacinterp :
diff --git a/Makefile.dev b/Makefile.dev
index 0105df972a..b0299bd160 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/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index 57f569858b..a0a4e0749d 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -18,4 +18,18 @@ sed -i -e "s/From Coq Require Export BigN/From Bignums Require Export BigN/" ${C
 sed -i -e "s/From Coq Require Import BigZ/From Bignums Require Import BigZ/" ${Color_CI_DIR}/Util/*/*.v
 sed -i -e "s/From Coq Require Export BigZ/From Bignums Require Export BigZ/" ${Color_CI_DIR}/Util/*/*.v
 
+# Adapt to PR #220 (FunInd not loaded in Prelude anymore)
+sed -i -e "15i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/basis/ordered_set.v
+sed -i -e "8i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/equational_extension.v
+sed -i -e "6i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/more_list_extention.v
+sed -i -e "6i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/ring_extention.v
+sed -i -e "27i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/dickson.v
+sed -i -e "26i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_permut.v
+sed -i -e "23i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_set.v
+sed -i -e "25i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_sort.v
+sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/more_list.v
+sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/List/ListUtil.v
+sed -i -e "17i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Multiset/MultisetOrder.v
+sed -i -e "13i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Set/SetUtil.v
+
 ( cd ${Color_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index 7d23ccad97..23ef41d2dd 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -7,6 +7,8 @@ source ${ci_dir}/ci-common.sh
 wget ${sf_CI_TARURL}
 tar xvfz sf.tgz
 
+sed -i.bak '15i From Coq Require Extraction.' sf/Extraction.v
+
 ( cd sf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make -j ${NJOBS} )
 
 
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index 200d431bcb..2ecd40416f 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -47,3 +47,12 @@ if [ $TRAVIS_PULL_REQUEST == "498" ] || [ $TRAVIS_BRANCH == "outsource-bignums"
     Corn_CI_BRANCH=external-bignums
     Corn_CI_GITURL=https://github.com/letouzey/corn.git
 fi
+
+if [ $TRAVIS_PULL_REQUEST == "220" ] || [ $TRAVIS_BRANCH == "less_init_plugins" ]; then
+    CompCert_CI_BRANCH=less_init_plugins
+    CompCert_CI_GITURL=https://github.com/letouzey/CompCert.git
+    VST_CI_BRANCH=less_init_plugins
+    VST_CI_GITURL=https://github.com/letouzey/VST.git
+    fiat_crypto_CI_BRANCH=less_init_plugins
+    fiat_crypto_CI_GITURL=https://github.com/letouzey/fiat-crypto.git
+fi
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index 01dbcfb1cb..fa3d61b1cd 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 6dd0ddf81d..939fc87a6e 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 53aa6b86ab..d3719bed46 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 253eb7f01b..2bab04e90a 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/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 893605499c..b605a44c87 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -51,6 +51,20 @@ let make_bullet s =
   | '*' -> Star n
   | _ -> assert false
 
+let extraction_err ~loc =
+  if not (Mltop.module_is_known "extraction_plugin") then
+    CErrors.user_err ~loc (str "Please do first a Require Extraction.")
+  else
+    (* The right grammar entries should have been loaded.
+       We could only end here in case of syntax error. *)
+    raise (Stream.Error "unexpected end of command")
+
+let funind_err ~loc =
+  if not (Mltop.module_is_known "recdef_plugin") then
+    CErrors.user_err ~loc (str "Please do first a Require Import FunInd.")
+  else
+    raise (Stream.Error "unexpected end of command") (* Same as above... *)
+
 GEXTEND Gram
   GLOBAL: vernac gallina_ext noedit_mode subprf;
   vernac: FIRST
@@ -841,6 +855,22 @@ GEXTEND Gram
       | IDENT "DelPath"; dir = ne_string ->
 	  VernacRemoveLoadPath dir
 
+      (* Some plugins are not loaded initially anymore : extraction,
+         and funind. To ease this transition toward a mandatory Require,
+         we hack here the vernac grammar in order to get customized
+         error messages telling what to Require instead of the dreadful
+         "Illegal begin of vernac". Normally, these fake grammar entries
+         are overloaded later by the grammar extensions in these plugins.
+         This code is meant to be removed in a few releases, when this
+         transition is considered finished. *)
+
+      | IDENT "Extraction" -> extraction_err ~loc:!@loc
+      | IDENT "Extract" -> extraction_err ~loc:!@loc
+      | IDENT "Recursive"; IDENT "Extraction" -> extraction_err ~loc:!@loc
+      | IDENT "Separate"; IDENT "Extraction" -> extraction_err ~loc:!@loc
+      | IDENT "Function" -> funind_err ~loc:!@loc
+      | IDENT "Functional" -> funind_err ~loc:!@loc
+
       (* Type-Checking (pas dans le refman) *)
       | "Type"; c = lconstr -> VernacGlobalCheck c
 
diff --git a/plugins/extraction/ExtrHaskellBasic.v b/plugins/extraction/ExtrHaskellBasic.v
index 294d61023b..d08a81da64 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 e94e7d42bd..267322d9ed 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 038f0ed817..4c5c71f58a 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 244eb85fc2..fabe9a4c67 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 3558f4f254..ac1f6f9130 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 66690851a7..0345ffc4e8 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 f192f16ee8..f7f9e2f80d 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 cbbfda75e5..4141bd203f 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 d9b000c2af..dfdc498638 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 c42938c8ec..78ee460856 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 515fa52dfa..fcfea352a7 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 3149e70298..e0837be621 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 7c607f7ae6..80da72d43f 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 6af591eed3..64ca6c85d0 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 c9e8eac0c5..66f188c84e 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 4d33174b35..c93cfb9d46 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 0000000000..ab1416b1d6
--- /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 0000000000..e40aea7764
--- /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 e4433247b4..64f43b8335 100644
--- a/plugins/funind/Recdef.v
+++ b/plugins/funind/Recdef.v
@@ -6,8 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+Require Export 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 135a715203..95f135c8f0 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 941ae530fd..098a7e9e72 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 7c78131252..1b758acd73 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 0aa029e73d..2fb0a5439a 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 c862f82067..a59975dbcf 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 fdc8501099..5d8ca330ac 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 2dc78d4c7f..e60244cd1d 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 b63f09bcfc..541fb798c0 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 6c514b16ee..1ecd9771eb 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 3bf97c1312..f87f2e2a9d 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 d8f8042465..8419404925 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 0086e090bd..89be144152 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 11bb25fda0..e770cf779a 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 dfdeff82ff..5bf807b1c6 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 7215bd9905..936d838c50 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 2fa7704941..789854b2d6 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 64ba6b1e30..b30ad1af88 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 c9e5b8dd20..4a790296bb 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 a7be32328d..b8e362f159 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 5acdb7eb7e..aadef476d7 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 130cbee871..8124097020 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 e71a8774ed..28049e9ee5 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 a3c265a21f..b30cb6b565 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 154c2384c8..036ff1aa4b 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 c490ea5166..6e51f61873 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.