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.

15 files changed, 25 insertions, 0 deletions

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.*)