Test-suite: avoid explicit references to “Top”

20 files changed, 112 insertions, 94 deletions

diff --git a/test-suite/bugs/closed/bug_5096.v b/test-suite/bugs/closed/bug_5096.v
index 20a537ab3c..18ce5c7305 100644
--- a/test-suite/bugs/closed/bug_5096.v
+++ b/test-suite/bugs/closed/bug_5096.v
@@ -1,3 +1,4 @@
+(* coq-prog-args: ("-top" "bug_5096") *)
 Require Import Coq.FSets.FMapPositive Coq.PArith.BinPos Coq.Lists.List.
 
 Set Asymmetric Patterns.
@@ -81,14 +82,14 @@ Global Arguments register_reassign {_ _ _ _} ctxi ctxr e _.
 Section language5.
   Context (Name : Type).
 
-  Local Notation expr := (@Top.expr Name).
+  Local Notation expr := (@bug_5096.expr Name).
   Local Notation nexpr := (@Named.expr Name).
 
   Fixpoint ocompile (e : expr) (ls : list (option Name)) {struct e}
     : option (nexpr)
-    := match e in @Top.expr _ return option (nexpr) with
-       | Top.Const => Some Named.Const
-       | Top.LetIn ex eC
+    := match e in @bug_5096.expr _ return option (nexpr) with
+       | bug_5096.Const => Some Named.Const
+       | bug_5096.LetIn ex eC
          => match @ocompile ex nil, split_onames ls with
             | Some x, (Some n, ls')%core
               => option_map (fun C => Named.LetIn n x C) (@ocompile (eC n) ls')
@@ -189,8 +190,8 @@ Definition DefaultRegisters (e : Expr) : list Register
 
 Definition DefaultAssembleSyntax e := @AssembleSyntax e (DefaultRegisters e).
 
-Notation "'slet' x := A 'in' b" := (Top.LetIn A (fun x => b)) (at level 200, b at level 200).
-Notation "#[ var ]#" := (@Top.Const var).
+Notation "'slet' x := A 'in' b" := (bug_5096.LetIn A (fun x => b)) (at level 200, b at level 200).
+Notation "#[ var ]#" := (@bug_5096.Const var).
 
 Definition compiled_syntax : Expr := fun (var : Type) =>
 (
@@ -211,7 +212,7 @@ Definition compiled_syntax : Expr := fun (var : Type) =>
   slet x1 := #[ var ]# in
   slet x1 := #[ var ]# in
   slet x1 := #[ var ]# in
- @Top.Const var).
+ @bug_5096.Const var).
 
 Definition v :=
   Eval cbv [compiled_syntax] in (DefaultAssembleSyntax (compiled_syntax)).
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.
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index 979396969a..d587d1f09b 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -42,32 +42,32 @@ Arguments D1, C1 are implicit and maximally inserted
 Argument scopes are [foo_scope type_scope _ _ _ _ _]
 The reduction tactics never unfold pf
 pf is transparent
-Expands to: Constant Top.pf
+Expands to: Constant Arguments.pf
 fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C
 
 Arguments A, B, C are implicit and maximally inserted
 Argument scopes are [type_scope type_scope type_scope _ _ _]
 The reduction tactics unfold fcomp when applied to 6 arguments 
 fcomp is transparent
-Expands to: Constant Top.fcomp
+Expands to: Constant Arguments.fcomp
 volatile : nat -> nat
 
 Argument scope is [nat_scope]
 The reduction tactics always unfold volatile
 volatile is transparent
-Expands to: Constant Top.volatile
+Expands to: Constant Arguments.volatile
 f : T1 -> T2 -> nat -> unit -> nat -> nat
 
 Argument scopes are [_ _ nat_scope _ nat_scope]
 f is transparent
-Expands to: Constant Top.S1.S2.f
+Expands to: Constant Arguments.S1.S2.f
 f : T1 -> T2 -> nat -> unit -> nat -> nat
 
 Argument scopes are [_ _ nat_scope _ nat_scope]
 The reduction tactics unfold f when the 3rd, 4th and
   5th arguments evaluate to a constructor 
 f is transparent
-Expands to: Constant Top.S1.S2.f
+Expands to: Constant Arguments.S1.S2.f
 f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
 Argument T2 is implicit
@@ -75,7 +75,7 @@ Argument scopes are [type_scope _ _ nat_scope _ nat_scope]
 The reduction tactics unfold f when the 4th, 5th and
   6th arguments evaluate to a constructor 
 f is transparent
-Expands to: Constant Top.S1.f
+Expands to: Constant Arguments.S1.f
 f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
 Arguments T1, T2 are implicit
@@ -83,7 +83,7 @@ Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope]
 The reduction tactics unfold f when the 5th, 6th and
   7th arguments evaluate to a constructor 
 f is transparent
-Expands to: Constant Top.f
+Expands to: Constant Arguments.f
      = forall v : unit, f 0 0 5 v 3 = 2
      : Prop
      = 2 = 2
@@ -93,7 +93,7 @@ f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 The reduction tactics unfold f when the 5th, 6th and
   7th arguments evaluate to a constructor 
 f is transparent
-Expands to: Constant Top.f
+Expands to: Constant Arguments.f
 forall w : r, w 3 true = tt
      : Prop
 The command has indeed failed with message:
diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v
index b67ac4f0df..97df40f882 100644
--- a/test-suite/output/Arguments.v
+++ b/test-suite/output/Arguments.v
@@ -1,3 +1,4 @@
+(* coq-prog-args: ("-top" "Arguments") *)
 Arguments Nat.sub n m : simpl nomatch.
 About Nat.sub.
 Arguments Nat.sub n / m : simpl nomatch.
diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out
index 6643c1429a..febe160820 100644
--- a/test-suite/output/ArgumentsScope.out
+++ b/test-suite/output/ArgumentsScope.out
@@ -10,12 +10,12 @@ negb'' : bool -> bool
 
 Argument scope is [bool_scope]
 negb'' is transparent
-Expands to: Constant Top.A.B.negb''
+Expands to: Constant ArgumentsScope.A.B.negb''
 negb' : bool -> bool
 
 Argument scope is [bool_scope]
 negb' is transparent
-Expands to: Constant Top.A.negb'
+Expands to: Constant ArgumentsScope.A.negb'
 negb : bool -> bool
 
 Argument scope is [bool_scope]
@@ -34,11 +34,11 @@ Expands to: Constant Coq.Init.Datatypes.negb
 negb' : bool -> bool
 
 negb' is transparent
-Expands to: Constant Top.A.negb'
+Expands to: Constant ArgumentsScope.A.negb'
 negb'' : bool -> bool
 
 negb'' is transparent
-Expands to: Constant Top.A.B.negb''
+Expands to: Constant ArgumentsScope.A.B.negb''
 a : bool -> bool
 
 Expands to: Variable a
@@ -49,8 +49,8 @@ Expands to: Constant Coq.Init.Datatypes.negb
 negb' : bool -> bool
 
 negb' is transparent
-Expands to: Constant Top.negb'
+Expands to: Constant ArgumentsScope.negb'
 negb'' : bool -> bool
 
 negb'' is transparent
-Expands to: Constant Top.negb''
+Expands to: Constant ArgumentsScope.negb''
diff --git a/test-suite/output/ArgumentsScope.v b/test-suite/output/ArgumentsScope.v
index 3a90cb79d7..ec49d85161 100644
--- a/test-suite/output/ArgumentsScope.v
+++ b/test-suite/output/ArgumentsScope.v
@@ -1,3 +1,4 @@
+(* coq-prog-args: ("-top" "ArgumentsScope") *)
 (* A few tests to check Global Argument Scope command *)
 
 Section A.
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index c0b04eb53f..1755886967 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -1,6 +1,6 @@
 The command has indeed failed with message:
 Flag "rename" expected to rename A into B.
-File "stdin", line 2, characters 0-25:
+File "stdin", line 3, characters 0-25:
 Warning: This command is just asserting the names of arguments of identity.
 If this is what you want add ': assert' to silence the warning. If you want
 to clear implicit arguments add ': clear implicits'. If you want to clear
@@ -41,7 +41,7 @@ myrefl : forall (B : Type) (x : A), B -> myEq B x x
 Arguments are renamed to C, x, _
 Argument C is implicit and maximally inserted
 Argument scopes are [type_scope _ _]
-Expands to: Constructor Top.Test1.myrefl
+Expands to: Constructor Arguments_renaming.Test1.myrefl
 myplus = 
 fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
   match n with
@@ -61,7 +61,7 @@ Argument scopes are [type_scope _ nat_scope nat_scope]
 The reduction tactics unfold myplus when the 2nd and
   3rd arguments evaluate to a constructor 
 myplus is transparent
-Expands to: Constant Top.Test1.myplus
+Expands to: Constant Arguments_renaming.Test1.myplus
 @myplus
      : forall Z : Type, Z -> nat -> nat -> nat
 Inductive myEq (A B : Type) (x : A) : A -> Prop :=
@@ -76,7 +76,7 @@ myrefl : forall (A B : Type) (x : A), B -> myEq A B x x
 Arguments are renamed to A, C, x, _
 Argument C is implicit and maximally inserted
 Argument scopes are [type_scope type_scope _ _]
-Expands to: Constructor Top.myrefl
+Expands to: Constructor Arguments_renaming.myrefl
 myrefl
      : forall (A C : Type) (x : A), C -> myEq A C x x
 myplus = 
@@ -98,7 +98,7 @@ Argument scopes are [type_scope _ nat_scope nat_scope]
 The reduction tactics unfold myplus when the 2nd and
   3rd arguments evaluate to a constructor 
 myplus is transparent
-Expands to: Constant Top.myplus
+Expands to: Constant Arguments_renaming.myplus
 @myplus
      : forall Z : Type, Z -> nat -> nat -> nat
 The command has indeed failed with message:
diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v
index 0cb331347d..9713a9dbbe 100644
--- a/test-suite/output/Arguments_renaming.v
+++ b/test-suite/output/Arguments_renaming.v
@@ -1,3 +1,4 @@
+(* coq-prog-args: ("-top" "Arguments_renaming") *)
 Fail Arguments eq_refl {B y}, [B] y.
 Arguments identity A _ _.
 Arguments eq_refl A x : assert.
diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out
index 24180c4553..cf2d5b2850 100644
--- a/test-suite/output/Errors.out
+++ b/test-suite/output/Errors.out
@@ -1,5 +1,5 @@
 The command has indeed failed with message:
-The field t is missing in Top.M.
+The field t is missing in Errors.M.
 The command has indeed failed with message:
 Unable to unify "nat" with "True".
 The command has indeed failed with message:
diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v
index 7375227827..edc35f17b4 100644
--- a/test-suite/output/Errors.v
+++ b/test-suite/output/Errors.v
@@ -1,3 +1,4 @@
+(* coq-prog-args: ("-top" "Errors") *)
 (* Test error messages *)
 
 (* Test non-regression of bug fixed in r13486 (bad printer for module names) *)
diff --git a/test-suite/output/Nametab.out b/test-suite/output/Nametab.out
index c11621d7c1..47b19b71b3 100644
--- a/test-suite/output/Nametab.out
+++ b/test-suite/output/Nametab.out
@@ -1,36 +1,39 @@
-Constant Top.Q.N.K.foo
+Constant Nametab.Q.N.K.foo
   (shorter name to refer to it in current context is Q.N.K.foo)
-Constant Top.Q.N.K.foo
+Constant Nametab.Q.N.K.foo
   (shorter name to refer to it in current context is Q.N.K.foo)
-Constant Top.Q.N.K.foo
+Constant Nametab.Q.N.K.foo
   (shorter name to refer to it in current context is Q.N.K.foo)
-Constant Top.Q.N.K.foo
-Constant Top.Q.N.K.foo
+Constant Nametab.Q.N.K.foo
+Constant Nametab.Q.N.K.foo
   (shorter name to refer to it in current context is Q.N.K.foo)
-Module Top.Q.N.K (shorter name to refer to it in current context is Q.N.K)
-Module Top.Q.N.K (shorter name to refer to it in current context is Q.N.K)
-Module Top.Q.N.K
-Module Top.Q.N.K (shorter name to refer to it in current context is Q.N.K)
-Module Top.Q.N (shorter name to refer to it in current context is Q.N)
-Module Top.Q.N
-Module Top.Q.N (shorter name to refer to it in current context is Q.N)
-Module Top.Q
-Module Top.Q (shorter name to refer to it in current context is Q)
-Constant Top.Q.N.K.foo
+Module Nametab.Q.N.K
+  (shorter name to refer to it in current context is Q.N.K)
+Module Nametab.Q.N.K
+  (shorter name to refer to it in current context is Q.N.K)
+Module Nametab.Q.N.K
+Module Nametab.Q.N.K
+  (shorter name to refer to it in current context is Q.N.K)
+Module Nametab.Q.N (shorter name to refer to it in current context is Q.N)
+Module Nametab.Q.N
+Module Nametab.Q.N (shorter name to refer to it in current context is Q.N)
+Module Nametab.Q
+Module Nametab.Q (shorter name to refer to it in current context is Q)
+Constant Nametab.Q.N.K.foo
   (shorter name to refer to it in current context is K.foo)
-Constant Top.Q.N.K.foo
-Constant Top.Q.N.K.foo
+Constant Nametab.Q.N.K.foo
+Constant Nametab.Q.N.K.foo
   (shorter name to refer to it in current context is K.foo)
-Constant Top.Q.N.K.foo
+Constant Nametab.Q.N.K.foo
   (shorter name to refer to it in current context is K.foo)
-Constant Top.Q.N.K.foo
+Constant Nametab.Q.N.K.foo
   (shorter name to refer to it in current context is K.foo)
-Module Top.Q.N.K
-Module Top.Q.N.K (shorter name to refer to it in current context is K)
-Module Top.Q.N.K (shorter name to refer to it in current context is K)
-Module Top.Q.N.K (shorter name to refer to it in current context is K)
-Module Top.Q.N (shorter name to refer to it in current context is Q.N)
-Module Top.Q.N
-Module Top.Q.N (shorter name to refer to it in current context is Q.N)
-Module Top.Q
-Module Top.Q (shorter name to refer to it in current context is Q)
+Module Nametab.Q.N.K
+Module Nametab.Q.N.K (shorter name to refer to it in current context is K)
+Module Nametab.Q.N.K (shorter name to refer to it in current context is K)
+Module Nametab.Q.N.K (shorter name to refer to it in current context is K)
+Module Nametab.Q.N (shorter name to refer to it in current context is Q.N)
+Module Nametab.Q.N
+Module Nametab.Q.N (shorter name to refer to it in current context is Q.N)
+Module Nametab.Q
+Module Nametab.Q (shorter name to refer to it in current context is Q)
diff --git a/test-suite/output/Nametab.v b/test-suite/output/Nametab.v
index 357ba98243..4bbc5ca239 100644
--- a/test-suite/output/Nametab.v
+++ b/test-suite/output/Nametab.v
@@ -1,3 +1,4 @@
+(* coq-prog-args: ("-top" "Nametab") *)
 Module Q.
   Module N.
     Module K.
@@ -10,19 +11,19 @@ End Q.
 (* Bad *) Locate K.foo.
 (* Bad *) Locate N.K.foo.
 (* OK  *) Locate Q.N.K.foo.
-(* OK  *) Locate Top.Q.N.K.foo.
+(* OK  *) Locate Nametab.Q.N.K.foo.
 
 (* Bad *) Locate Module K.
 (* Bad *) Locate Module N.K.
 (* OK  *) Locate Module Q.N.K.
-(* OK  *) Locate Module Top.Q.N.K.
+(* OK  *) Locate Module Nametab.Q.N.K.
 
 (* Bad *) Locate Module N.
 (* OK  *) Locate Module Q.N.
-(* OK  *) Locate Module Top.Q.N.
+(* OK  *) Locate Module Nametab.Q.N.
 
 (* OK  *) Locate Module Q.
-(* OK  *) Locate Module Top.Q.
+(* OK  *) Locate Module Nametab.Q.
 
 
 Import Q.N.
@@ -32,16 +33,16 @@ Import Q.N.
 (* OK  *) Locate K.foo.
 (* Bad *) Locate N.K.foo.
 (* OK  *) Locate Q.N.K.foo.
-(* OK  *) Locate Top.Q.N.K.foo.
+(* OK  *) Locate Nametab.Q.N.K.foo.
 
 (* OK  *) Locate Module K.
 (* Bad *) Locate Module N.K.
 (* OK  *) Locate Module Q.N.K.
-(* OK  *) Locate Module Top.Q.N.K.
+(* OK  *) Locate Module Nametab.Q.N.K.
 
 (* Bad *) Locate Module N.
 (* OK  *) Locate Module Q.N.
-(* OK  *) Locate Module Top.Q.N.
+(* OK  *) Locate Module Nametab.Q.N.
 
 (* OK  *) Locate Module Q.
-(* OK  *) Locate Module Top.Q.
+(* OK  *) Locate Module Nametab.Q.
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index 975b2ef7ff..38a16e01c2 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -77,7 +77,7 @@ Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
 Argument x is implicit and maximally inserted
-Expands to: Constant Top.bar
+Expands to: Constant PrintInfos.bar
 *** [ bar : foo ]
 
 Expanded type for implicit arguments
diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v
index 62aa80f8ab..d7c271c3ec 100644
--- a/test-suite/output/PrintInfos.v
+++ b/test-suite/output/PrintInfos.v
@@ -1,3 +1,4 @@
+(* coq-prog-args: ("-top" "PrintInfos") *)
 About existT.
 Print existT.
 Print Implicit existT.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 1e50ba511a..acc37f653c 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -42,10 +42,10 @@ bar@{u} = nat
          *)
 
 bar is universe polymorphic
-foo@{u Top.17 v} = 
-Type@{Top.17} -> Type@{v} -> Type@{u}
-     : Type@{max(u+1,Top.17+1,v+1)}
-(* u Top.17 v |=  *)
+foo@{u UnivBinders.17 v} = 
+Type@{UnivBinders.17} -> Type@{v} -> Type@{u}
+     : Type@{max(u+1,UnivBinders.17+1,v+1)}
+(* u UnivBinders.17 v |=  *)
 
 foo is universe polymorphic
 Type@{i} -> Type@{j}
@@ -86,10 +86,10 @@ Type@{M} -> Type@{N} -> Type@{E}
 (* E M N |=  *)
 
 foo is universe polymorphic
-foo@{u Top.17 v} = 
-Type@{Top.17} -> Type@{v} -> Type@{u}
-     : Type@{max(u+1,Top.17+1,v+1)}
-(* u Top.17 v |=  *)
+foo@{u UnivBinders.17 v} = 
+Type@{UnivBinders.17} -> Type@{v} -> Type@{u}
+     : Type@{max(u+1,UnivBinders.17+1,v+1)}
+(* u UnivBinders.17 v |=  *)
 
 foo is universe polymorphic
 NonCumulative Inductive Empty@{E} : Type@{E} :=  
@@ -104,7 +104,7 @@ punwrap@{K} : forall A : Type@{K}, PWrap@{K} A -> A
 punwrap is universe polymorphic
 Argument scopes are [type_scope _]
 punwrap is transparent
-Expands to: Constant Top.punwrap
+Expands to: Constant UnivBinders.punwrap
 The command has indeed failed with message:
 Universe instance should have length 3
 The command has indeed failed with message:
@@ -163,27 +163,29 @@ inmod@{u} -> Type@{v}
 (* u v |=  *)
 
 Applied.infunct is universe polymorphic
-axfoo@{i Top.55 Top.56} : Type@{Top.55} -> Type@{i}
-(* i Top.55 Top.56 |=  *)
+axfoo@{i UnivBinders.55 UnivBinders.56} :
+Type@{UnivBinders.55} -> Type@{i}
+(* i UnivBinders.55 UnivBinders.56 |=  *)
 
 axfoo is universe polymorphic
 Argument scope is [type_scope]
-Expands to: Constant Top.axfoo
-axbar@{i Top.55 Top.56} : Type@{Top.56} -> Type@{i}
-(* i Top.55 Top.56 |=  *)
+Expands to: Constant UnivBinders.axfoo
+axbar@{i UnivBinders.55 UnivBinders.56} :
+Type@{UnivBinders.56} -> Type@{i}
+(* i UnivBinders.55 UnivBinders.56 |=  *)
 
 axbar is universe polymorphic
 Argument scope is [type_scope]
-Expands to: Constant Top.axbar
-axfoo' : Type@{Top.58} -> Type@{axbar'.i}
+Expands to: Constant UnivBinders.axbar
+axfoo' : Type@{UnivBinders.58} -> Type@{axbar'.i}
 
 axfoo' is not universe polymorphic
 Argument scope is [type_scope]
-Expands to: Constant Top.axfoo'
-axbar' : Type@{Top.58} -> Type@{axbar'.i}
+Expands to: Constant UnivBinders.axfoo'
+axbar' : Type@{UnivBinders.58} -> Type@{axbar'.i}
 
 axbar' is not universe polymorphic
 Argument scope is [type_scope]
-Expands to: Constant Top.axbar'
+Expands to: Constant UnivBinders.axbar'
 The command has indeed failed with message:
 When declaring multiple axioms in one command, only the first is allowed a universe binder (which will be shared by the whole block).
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index 9aebce1b9a..56474a0723 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -1,3 +1,4 @@
+(* coq-prog-args: ("-top" "UnivBinders") *)
 Set Universe Polymorphism.
 Set Printing Universes.
 (* Unset Strict Universe Declaration. *)
@@ -58,7 +59,7 @@ Import mono.
 Check monomono. (* unqualified MONOU *)
 Check mono. (* still qualified mono.u *)
 
-Monomorphic Constraint Set < Top.mono.u.
+Monomorphic Constraint Set < UnivBinders.mono.u.
 
 Module mono2.
   Monomorphic Universe u.
@@ -76,10 +77,10 @@ Module SecLet.
     Definition bobmorane := tt -> ff.
   End foo.
   Print bobmorane. (*
-                     bobmorane@{Top.15 Top.16 ff.u ff.v} =
-                     let tt := Type@{Top.16} in let ff := Type@{ff.v} in tt -> ff
-                     : Type@{max(Top.15,ff.u)}
-                     (* Top.15 Top.16 ff.u ff.v |= Top.16 < Top.15
+                     bobmorane@{UnivBinders.15 UnivBinders.16 ff.u ff.v} =
+                     let tt := Type@{UnivBinders.16} in let ff := Type@{ff.v} in tt -> ff
+                     : Type@{max(UnivBinders.15,ff.u)}
+                     (* UnivBinders.15 UnivBinders.16 ff.u ff.v |= UnivBinders.16 < UnivBinders.15
                      ff.v < ff.u
                     *)
 
diff --git a/test-suite/output/qualification.out b/test-suite/output/qualification.out
index e9c70d1efc..cfa295010f 100644
--- a/test-suite/output/qualification.out
+++ b/test-suite/output/qualification.out
@@ -1,4 +1,5 @@
-File "stdin", line 19, characters 0-7:
+File "stdin", line 20, characters 0-7:
 Error: Signature components for label test do not match: expected type
-"Top.M2.t = Top.M2.M.t" but found type "Top.M2.t = Top.M2.t".
+"qualification.M2.t = qualification.M2.M.t" but found type
+"qualification.M2.t = qualification.M2.t".
 
diff --git a/test-suite/output/qualification.v b/test-suite/output/qualification.v
index d39097e2dd..877bc84d14 100644
--- a/test-suite/output/qualification.v
+++ b/test-suite/output/qualification.v
@@ -1,3 +1,4 @@
+(* coq-prog-args: ("-top" "qualification") *)
 Module Type T1.
   Parameter t : Type.
 End T1.
diff --git a/test-suite/success/unidecls.v b/test-suite/success/unidecls.v
index 014f1834a2..7c298c98b6 100644
--- a/test-suite/success/unidecls.v
+++ b/test-suite/success/unidecls.v
@@ -1,3 +1,4 @@
+(* coq-prog-args: ("-top" "unidecls") *)
 Set Printing Universes.
 
 Module decls.
@@ -39,7 +40,7 @@ Check Type@{Foo.bar}.
 Check Type@{Foo.foo}.
 (** The same *)
 Check Type@{foo}.
-Check Type@{Top.foo}.
+Check Type@{unidecls.foo}.
 
 Universe secfoo.
 Section Foo'.