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.

20 files changed, 53 insertions, 1 deletions

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..c6fcd647ff 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 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.