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