13 files changed, 29 insertions, 93 deletions
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index 629a1ab6..2c7b04c6 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -1,13 +1,11 @@
 Nat.sub : nat -> nat -> nat
 
-Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold Nat.sub but avoid exposing match constructs
 Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
-Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold Nat.sub when applied to 1 argument
   but avoid exposing match constructs
@@ -15,7 +13,6 @@ Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
-Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold Nat.sub
   when the 1st argument evaluates to a constructor and
@@ -24,7 +21,6 @@ Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
-Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold Nat.sub when the 1st and
   2nd arguments evaluate to a constructor and when applied to 2 arguments 
@@ -32,7 +28,6 @@ Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
-Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold Nat.sub when the 1st and
   2nd arguments evaluate to a constructor 
@@ -42,7 +37,6 @@ pf :
 forall D1 C1 : Type,
 (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2
 
-pf is not universe polymorphic
 Arguments D2, C2 are implicit
 Arguments D1, C1 are implicit and maximally inserted
 Argument scopes are [foo_scope type_scope _ _ _ _ _]
@@ -51,7 +45,6 @@ pf is transparent
 Expands to: Constant Top.pf
 fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C
 
-fcomp is not universe polymorphic
 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 
@@ -59,20 +52,17 @@ fcomp is transparent
 Expands to: Constant Top.fcomp
 volatile : nat -> nat
 
-volatile is not universe polymorphic
 Argument scope is [nat_scope]
 The reduction tactics always unfold volatile
 volatile is transparent
 Expands to: Constant Top.volatile
 f : T1 -> T2 -> nat -> unit -> nat -> nat
 
-f is not universe polymorphic
 Argument scopes are [_ _ nat_scope _ nat_scope]
 f is transparent
 Expands to: Constant Top.S1.S2.f
 f : T1 -> T2 -> nat -> unit -> nat -> nat
 
-f is not universe polymorphic
 Argument scopes are [_ _ nat_scope _ nat_scope]
 The reduction tactics unfold f when the 3rd, 4th and
   5th arguments evaluate to a constructor 
@@ -80,7 +70,6 @@ f is transparent
 Expands to: Constant Top.S1.S2.f
 f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
-f is not universe polymorphic
 Argument T2 is implicit
 Argument scopes are [type_scope _ _ nat_scope _ nat_scope]
 The reduction tactics unfold f when the 4th, 5th and
@@ -89,7 +78,6 @@ f is transparent
 Expands to: Constant Top.S1.f
 f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
-f is not universe polymorphic
 Arguments T1, T2 are implicit
 Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope]
 The reduction tactics unfold f when the 5th, 6th and
@@ -102,7 +90,6 @@ Expands to: Constant Top.f
      : Prop
 f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
-f is not universe polymorphic
 The reduction tactics unfold f when the 5th, 6th and
   7th arguments evaluate to a constructor 
 f is transparent
@@ -110,8 +97,8 @@ Expands to: Constant Top.f
 forall w : r, w 3 true = tt
      : Prop
 The command has indeed failed with message:
-=> Error: Unknown interpretation for notation "$".
+Error: Unknown interpretation for notation "$".
 w 3 true = tt
      : Prop
 The command has indeed failed with message:
-=> Error: Extra argument _.
+Error: Extra argument _.
diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out
index 71d5fc78..6643c142 100644
--- a/test-suite/output/ArgumentsScope.out
+++ b/test-suite/output/ArgumentsScope.out
@@ -1,70 +1,56 @@
 a : bool -> bool
 
-a is not universe polymorphic
 Argument scope is [bool_scope]
 Expands to: Variable a
 b : bool -> bool
 
-b is not universe polymorphic
 Argument scope is [bool_scope]
 Expands to: Variable b
 negb'' : bool -> bool
 
-negb'' is not universe polymorphic
 Argument scope is [bool_scope]
 negb'' is transparent
 Expands to: Constant Top.A.B.negb''
 negb' : bool -> bool
 
-negb' is not universe polymorphic
 Argument scope is [bool_scope]
 negb' is transparent
 Expands to: Constant Top.A.negb'
 negb : bool -> bool
 
-negb is not universe polymorphic
 Argument scope is [bool_scope]
 negb is transparent
 Expands to: Constant Coq.Init.Datatypes.negb
 a : bool -> bool
 
-a is not universe polymorphic
 Expands to: Variable a
 b : bool -> bool
 
-b is not universe polymorphic
 Expands to: Variable b
 negb : bool -> bool
 
-negb is not universe polymorphic
 negb is transparent
 Expands to: Constant Coq.Init.Datatypes.negb
 negb' : bool -> bool
 
-negb' is not universe polymorphic
 negb' is transparent
 Expands to: Constant Top.A.negb'
 negb'' : bool -> bool
 
-negb'' is not universe polymorphic
 negb'' is transparent
 Expands to: Constant Top.A.B.negb''
 a : bool -> bool
 
-a is not universe polymorphic
 Expands to: Variable a
 negb : bool -> bool
 
-negb is not universe polymorphic
 negb is transparent
 Expands to: Constant Coq.Init.Datatypes.negb
 negb' : bool -> bool
 
-negb' is not universe polymorphic
 negb' is transparent
 Expands to: Constant Top.negb'
 negb'' : bool -> bool
 
-negb'' is not universe polymorphic
 negb'' is transparent
 Expands to: Constant Top.negb''
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index c29f5649..1e3cc37d 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -1,8 +1,8 @@
 The command has indeed failed with message:
-=> Error: To rename arguments the "rename" flag must be specified.
+Error: To rename arguments the "rename" flag must be specified.
 Argument A renamed to B.
 The command has indeed failed with message:
-=> Error: To rename arguments the "rename" flag must be specified.
+Error: To rename arguments the "rename" flag must be specified.
 Argument A renamed to T.
 @eq_refl
      : forall (B : Type) (y : B), y = y
@@ -20,7 +20,6 @@ For eq: Argument scopes are [type_scope _ _]
 For eq_refl: Argument scopes are [type_scope _]
 eq_refl : forall (A : Type) (x : A), x = x
 
-eq_refl is not universe polymorphic
 Arguments are renamed to B, y
 When applied to no arguments:
   Arguments B, y are implicit and maximally inserted
@@ -36,7 +35,6 @@ For myEq: Argument scopes are [type_scope _ _]
 For myrefl: Argument scopes are [type_scope _ _]
 myrefl : forall (B : Type) (x : A), B -> myEq B x x
 
-myrefl is not universe polymorphic
 Arguments are renamed to C, x, _
 Argument C is implicit and maximally inserted
 Argument scopes are [type_scope _ _]
@@ -49,13 +47,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
   end
      : forall T : Type, T -> nat -> nat -> nat
 
-myplus is not universe polymorphic
 Arguments are renamed to Z, t, n, m
 Argument Z is implicit and maximally inserted
 Argument scopes are [type_scope _ nat_scope nat_scope]
 myplus : forall T : Type, T -> nat -> nat -> nat
 
-myplus is not universe polymorphic
 Arguments are renamed to Z, t, n, m
 Argument Z is implicit and maximally inserted
 Argument scopes are [type_scope _ nat_scope nat_scope]
@@ -74,7 +70,6 @@ For myEq: Argument scopes are [type_scope type_scope _ _]
 For myrefl: Argument scopes are [type_scope type_scope _ _]
 myrefl : forall (A B : Type) (x : A), B -> myEq A B x x
 
-myrefl is not universe polymorphic
 Arguments are renamed to A, C, x, _
 Argument C is implicit and maximally inserted
 Argument scopes are [type_scope type_scope _ _]
@@ -89,13 +84,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
   end
      : forall T : Type, T -> nat -> nat -> nat
 
-myplus is not universe polymorphic
 Arguments are renamed to Z, t, n, m
 Argument Z is implicit and maximally inserted
 Argument scopes are [type_scope _ nat_scope nat_scope]
 myplus : forall T : Type, T -> nat -> nat -> nat
 
-myplus is not universe polymorphic
 Arguments are renamed to Z, t, n, m
 Argument Z is implicit and maximally inserted
 Argument scopes are [type_scope _ nat_scope nat_scope]
@@ -106,15 +99,15 @@ Expands to: Constant Top.myplus
 @myplus
      : forall Z : Type, Z -> nat -> nat -> nat
 The command has indeed failed with message:
-=> Error: All arguments lists must declare the same names.
+Error: All arguments lists must declare the same names.
 The command has indeed failed with message:
-=> Error: The following arguments are not declared: x.
+Error: The following arguments are not declared: x.
 The command has indeed failed with message:
-=> Error: Arguments names must be distinct.
+Error: Arguments names must be distinct.
 The command has indeed failed with message:
-=> Error: Argument z cannot be declared implicit.
+Error: Argument z cannot be declared implicit.
 The command has indeed failed with message:
-=> Error: Extra argument y.
+Error: Extra argument y.
 The command has indeed failed with message:
-=> Error: To rename arguments the "rename" flag must be specified.
+Error: To rename arguments the "rename" flag must be specified.
 Argument A renamed to R.
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index d5903483..09f032d4 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -6,8 +6,6 @@ fix F (t : t) : P t :=
   end
      : forall P : t -> Type,
        (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
-
-t_rect is not universe polymorphic
      = fun d : TT => match d with
                      | @CTT _ _ b => b
                      end
@@ -26,7 +24,6 @@ match Nat.eq_dec x y with
 end
      : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
 
-proj is not universe polymorphic
 Argument scopes are [nat_scope nat_scope _ _ _]
 foo = 
 fix foo (A : Type) (l : list A) {struct l} : option A :=
@@ -37,7 +34,6 @@ fix foo (A : Type) (l : list A) {struct l} : option A :=
   end
      : forall A : Type, list A -> option A
 
-foo is not universe polymorphic
 Argument scopes are [type_scope list_scope]
 uncast = 
 fun (A : Type) (x : I A) => match x with
@@ -45,12 +41,9 @@ fun (A : Type) (x : I A) => match x with
                             end
      : forall A : Type, I A -> A
 
-uncast is not universe polymorphic
 Argument scopes are [type_scope _]
 foo' = if A 0 then true else false
      : bool
-
-foo' is not universe polymorphic
 f = 
 fun H : B =>
 match H with
@@ -61,5 +54,3 @@ match H with
      else fun _ : P false => Logic.I) x
 end
      : B -> True
-
-f is not universe polymorphic
diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out
index bcc37b63..6354ad46 100644
--- a/test-suite/output/Errors.out
+++ b/test-suite/output/Errors.out
@@ -1,7 +1,7 @@
 The command has indeed failed with message:
-=> Error: The field t is missing in Top.M.
+The field t is missing in Top.M.
 The command has indeed failed with message:
-=> Error: Unable to unify "nat" with "True".
+Unable to unify "nat" with "True".
 The command has indeed failed with message:
-=> In nested Ltac calls to "f" and "apply x", last call failed.
-Error: Unable to unify "nat" with "True".
+In nested Ltac calls to "f" and "apply x", last call failed.
+Unable to unify "nat" with "True".
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index 0b0f501f..3b65003c 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -5,7 +5,6 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I
 d2 = fun x : nat => d1 (y:=x)
      : forall x x0 : nat, x0 = x -> x0 = x
 
-d2 is not universe polymorphic
 Arguments x, x0 are implicit
 Argument scopes are [nat_scope nat_scope _]
 map id (1 :: nil)
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 60ee72b3..6efd671a 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -41,29 +41,29 @@ fun x : nat => ifn x is succ n then n else 0
 -4
      : Z
 The command has indeed failed with message:
-=> Error: x should not be bound in a recursive pattern of the right-hand side.
+Error: x should not be bound in a recursive pattern of the right-hand side.
 The command has indeed failed with message:
-=> Error: in the right-hand side, y and z should appear in
+Error: in the right-hand side, y and z should appear in
 term position as part of a recursive pattern.
 The command has indeed failed with message:
-=> Error: The reference w was not found in the current environment.
+The reference w was not found in the current environment.
 The command has indeed failed with message:
-=> Error: in the right-hand side, y and z should appear in
+Error: in the right-hand side, y and z should appear in
 term position as part of a recursive pattern.
 The command has indeed failed with message:
-=> Error: z is expected to occur in binding position in the right-hand side.
+Error: z is expected to occur in binding position in the right-hand side.
 The command has indeed failed with message:
-=> Error: as y is a non-closed binder, no such "," is allowed to occur.
+Error: as y is a non-closed binder, no such "," is allowed to occur.
 The command has indeed failed with message:
-=> Error: Cannot find where the recursive pattern starts.
+Error: Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-=> Error: Cannot find where the recursive pattern starts.
+Error: Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-=> Error: Cannot find where the recursive pattern starts.
+Error: Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-=> Error: Cannot find where the recursive pattern starts.
+Error: Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-=> Error: Both ends of the recursive pattern are the same.
+Error: Both ends of the recursive pattern are the same.
 SUM (nat * nat) nat
      : Set
 FST (0; 1)
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index 0457c860..ba076f05 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -25,7 +25,6 @@ For eq: Argument scopes are [type_scope _ _]
 For eq_refl: Argument scopes are [type_scope _]
 eq_refl : forall (A : Type) (x : A), x = x
 
-eq_refl is not universe polymorphic
 When applied to no arguments:
   Arguments A, x are implicit and maximally inserted
 When applied to 1 argument:
@@ -46,11 +45,9 @@ fix add (n m : nat) {struct n} : nat :=
   end
      : nat -> nat -> nat
 
-Nat.add is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 Nat.add : nat -> nat -> nat
 
-Nat.add is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 Nat.add is transparent
 Expands to: Constant Coq.Init.Nat.add
@@ -58,7 +55,6 @@ Nat.add : nat -> nat -> nat
 
 plus_n_O : forall n : nat, n = n + 0
 
-plus_n_O is not universe polymorphic
 Argument scope is [nat_scope]
 plus_n_O is opaque
 Expands to: Constant Coq.Init.Peano.plus_n_O
@@ -80,13 +76,11 @@ For le_n: Argument scope is [nat_scope]
 For le_S: Argument scopes are [nat_scope nat_scope _]
 comparison : Set
 
-comparison is not universe polymorphic
 Expands to: Inductive Coq.Init.Datatypes.comparison
 Inductive comparison : Set :=
     Eq : comparison | Lt : comparison | Gt : comparison
 bar : foo
 
-bar is not universe polymorphic
 Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
@@ -94,14 +88,12 @@ Argument x is implicit and maximally inserted
 Expands to: Constant Top.bar
 *** [ bar : foo ]
 
-bar is not universe polymorphic
 Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
 Argument x is implicit and maximally inserted
 bar : foo
 
-bar is not universe polymorphic
 Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
@@ -109,7 +101,6 @@ Argument x is implicit and maximally inserted
 Expands to: Constant Top.bar
 *** [ bar : foo ]
 
-bar is not universe polymorphic
 Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out
index 67b65d4b..f94ed642 100644
--- a/test-suite/output/TranspModtype.out
+++ b/test-suite/output/TranspModtype.out
@@ -1,15 +1,7 @@
 TrM.A = M.A
      : Set
-
-TrM.A is not universe polymorphic
 OpM.A = M.A
      : Set
-
-OpM.A is not universe polymorphic
 TrM.B = M.B
      : Set
-
-TrM.B is not universe polymorphic
 *** [ OpM.B : Set ]
-
-OpM.B is not universe polymorphic
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index d69baaec..b1952aec 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -4,8 +4,6 @@ fun e : option L => match e with
                     | None => None
                     end
      : option L -> option L
-
-P is not universe polymorphic
 fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H
      : forall m n p : nat, S m <= S n + p -> m <= n + p
 fun n : nat => let x := A n in ?y ?y0:T n
diff --git a/test-suite/output/names.out b/test-suite/output/names.out
index 2892dfd5..9471b892 100644
--- a/test-suite/output/names.out
+++ b/test-suite/output/names.out
@@ -1,5 +1,4 @@
 The command has indeed failed with message:
-=> Error:
 In environment
 y : nat
 The term "a y" has type "{y0 : nat | y = y0}"
diff --git a/test-suite/output/rewrite-2172.out b/test-suite/output/rewrite-2172.out
index 30385072..27b0dc1b 100644
--- a/test-suite/output/rewrite-2172.out
+++ b/test-suite/output/rewrite-2172.out
@@ -1,2 +1,2 @@
 The command has indeed failed with message:
-=> Error: Unable to find an instance for the variable E.
+Unable to find an instance for the variable E.
diff --git a/test-suite/output/simpl.v b/test-suite/output/simpl.v
index 89638eed..5f1926f1 100644
--- a/test-suite/output/simpl.v
+++ b/test-suite/output/simpl.v
@@ -4,10 +4,10 @@ Goal forall x, 0+x = 1+x.
 intro x.
 simpl (_ + x).
 Show.
-Undo 2.
+Undo.
 simpl (_ + x) at 2.
 Show.
-Undo 2.
+Undo.
 simpl (0 + _).
 Show.
-Undo 2.
+Undo.