Test-suite: avoid explicit references to “Top”

2 files changed, 5 insertions, 3 deletions

diff --git a/test-suite/modules/modeq.v b/test-suite/modules/modeq.v
index c8129eec5e..4ebcae82e5 100644
--- a/test-suite/modules/modeq.v
+++ b/test-suite/modules/modeq.v
@@ -1,10 +1,11 @@
+(* coq-prog-args: ("-top" "modeq") *)
 Module M.
   Definition T := nat.
   Definition x : T := 0.
 End M.
 
 Module Type SIG.
-  Module M := Top.M.
+  Module M := modeq.M.
   Module Type SIG.
     Parameter T : Set.
   End SIG.
@@ -12,7 +13,7 @@ Module Type SIG.
 End SIG.
 
 Module Z.
-  Module M := Top.M.
+  Module M := modeq.M.
   Module Type SIG.
     Parameter T : Set.
   End SIG.
diff --git a/test-suite/modules/modul.v b/test-suite/modules/modul.v
index 36a542ef0a..9b3772b0d9 100644
--- a/test-suite/modules/modul.v
+++ b/test-suite/modules/modul.v
@@ -1,3 +1,4 @@
+(* coq-prog-args: ("-top" "modul") *)
 Module M.
   Parameter rel : nat -> nat -> Prop.
 
@@ -32,4 +33,4 @@ Locate rel.
 
 Locate Module M.
 
-Module N := Top.M.
+Module N := modul.M.