Merge PR #8630: Some cleaning in the test suite

28 files changed, 112 insertions, 83 deletions

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/Cases.v b/test-suite/output/Cases.v
index e4fa7044e7..43718a0f07 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -187,6 +187,7 @@ let p := fresh "p" in
   |- eq_refl ?p = _ => pose (match eq_refl p in _ = z return p=p /\ z=z with eq_refl => conj eq_refl eq_refl end)
   end.
 Show.
+Abort.
 
 Set Printing Allow Match Default Clause.
 
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 c9b5091347..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) *)
@@ -31,3 +32,6 @@ Abort.
 Fail Goal forall a f, f a = 0.
 Fail Goal forall f x, id f x = 0.
 Fail Goal forall f P,  P (f 0).
+
+Definition t := unit.
+End M.
diff --git a/test-suite/output/Existentials.v b/test-suite/output/Existentials.v
index 7388468399..924f1f5592 100644
--- a/test-suite/output/Existentials.v
+++ b/test-suite/output/Existentials.v
@@ -12,3 +12,5 @@ clearbody q.
 clear p. (* Error ... *)
 
 Show Existentials.
+Abort.
+End Test.
diff --git a/test-suite/output/Match_subterm.v b/test-suite/output/Match_subterm.v
index 2c44b1879f..bf862c946d 100644
--- a/test-suite/output/Match_subterm.v
+++ b/test-suite/output/Match_subterm.v
@@ -4,3 +4,4 @@ match goal with
   idtac v ; fail
 | _ => idtac 2
 end.
+Abort.
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/Naming.v b/test-suite/output/Naming.v
index 327643dc57..7f3b332d7d 100644
--- a/test-suite/output/Naming.v
+++ b/test-suite/output/Naming.v
@@ -89,3 +89,4 @@ Show.
 apply H with (a:=a). (* test compliance with printing *)
 Abort.
 
+End A.
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/ShowMatch.v b/test-suite/output/ShowMatch.v
index 02b7eada83..9cf6ad35b8 100644
--- a/test-suite/output/ShowMatch.v
+++ b/test-suite/output/ShowMatch.v
@@ -11,3 +11,4 @@ Module B.
   Inductive foo := f.
   (* local foo shadows A.foo, so constructor "f" needs disambiguation *)
   Show Match A.foo. 
+End B.
diff --git a/test-suite/output/ShowProof.v b/test-suite/output/ShowProof.v
index 73ecaf2200..19822ac50e 100644
--- a/test-suite/output/ShowProof.v
+++ b/test-suite/output/ShowProof.v
@@ -4,3 +4,4 @@ Proof.
 split.
 - exact I.
   Show Proof. (* Was not finding an evar name at some time *)
+Abort.
diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v
index 75b66e463a..fa12f09a46 100644
--- a/test-suite/output/Tactics.v
+++ b/test-suite/output/Tactics.v
@@ -21,3 +21,4 @@ Proof.
 intros H.
 Fail intros [H%myid ?].
 Fail destruct 1 as [H%myid ?].
+Abort.
diff --git a/test-suite/output/TypeclassDebug.v b/test-suite/output/TypeclassDebug.v
index d38e2a50e4..2e4008ae56 100644
--- a/test-suite/output/TypeclassDebug.v
+++ b/test-suite/output/TypeclassDebug.v
@@ -6,3 +6,4 @@ Hint Resolve H : foo.
 Goal foo.
 Typeclasses eauto := debug.
 Fail typeclasses eauto 5 with foo.
+Abort.
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/names.v b/test-suite/output/names.v
index f1efd0df2a..e9033bd732 100644
--- a/test-suite/output/names.v
+++ b/test-suite/output/names.v
@@ -7,3 +7,4 @@ Fail Definition b y : {x:nat|x=y} := a y.
 Goal (forall n m, n <= m -> m <= n -> n = m) -> True.
 intro H; epose proof (H _ 3) as H.
 Show.
+Abort.
diff --git a/test-suite/output/optimize_heap.v b/test-suite/output/optimize_heap.v
index e566bd7bab..31b4510397 100644
--- a/test-suite/output/optimize_heap.v
+++ b/test-suite/output/optimize_heap.v
@@ -5,3 +5,4 @@ Goal True.
   Show.
   optimize_heap.
   Show.
+Abort.
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/output/rewrite-2172.out b/test-suite/output/rewrite_2172.out
index 27b0dc1b7b..27b0dc1b7b 100644
--- a/test-suite/output/rewrite-2172.out
+++ b/test-suite/output/rewrite_2172.out
diff --git a/test-suite/output/rewrite-2172.v b/test-suite/output/rewrite_2172.v
index 212b1c1259..864fc21cdd 100644
--- a/test-suite/output/rewrite-2172.v
+++ b/test-suite/output/rewrite_2172.v
@@ -19,3 +19,4 @@ Proof.
    user in rewrite/induction/destruct calls).
 *)
   Fail rewrite <- axiom.
+Abort.