6 files changed, 10 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