Merge PR #10476: Remove library-specific code for `Import`.

Reviewed-by: gares
Reviewed-by: ppedrot

2 files changed, 1 insertions, 3 deletions

diff --git a/test-suite/bugs/closed/bug_3481.v b/test-suite/bugs/closed/bug_3481.v
index 41e1a8e959..f54810d359 100644
--- a/test-suite/bugs/closed/bug_3481.v
+++ b/test-suite/bugs/closed/bug_3481.v
@@ -1,7 +1,6 @@
 
 Set Implicit Arguments.
 
-Require Import Logic.
 Module NonPrim.
 Local Set Nonrecursive Elimination Schemes.
 Record prodwithlet (A B : Type) : Type :=
diff --git a/test-suite/bugs/closed/bug_4498.v b/test-suite/bugs/closed/bug_4498.v
index 9b3210860c..ba63b707af 100644
--- a/test-suite/bugs/closed/bug_4498.v
+++ b/test-suite/bugs/closed/bug_4498.v
@@ -1,6 +1,7 @@
 Require Export Coq.Unicode.Utf8.
 Require Export Coq.Classes.Morphisms.
 Require Export Coq.Relations.Relation_Definitions.
+Require Export Coq.Setoids.Setoid.
 
 Set Universe Polymorphism.
 
@@ -17,8 +18,6 @@ Class Category := {
       Proper (@equiv B C ==> @equiv A B ==> @equiv A C) (@compose A B C);
 }.
 
-Require Export Coq.Setoids.Setoid.
-
 Add Parametric Morphism `{Category} {A B C} : (@compose _ A B C) with
   signature equiv ==> equiv ==> equiv as compose_mor.
 Proof. apply comp_respects. Qed.