aboutsummaryrefslogtreecommitdiff
path: root/test-suite/modules/modul.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/modules/modul.v')
-rw-r--r--test-suite/modules/modul.v3
1 files changed, 2 insertions, 1 deletions
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.