7 files changed, 12 insertions, 0 deletions
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.*)