17 files changed, 92 insertions, 26 deletions
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index a2ee2d4c8e..979396969a 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -97,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 "$".
+Unknown interpretation for notation "$".
 w 3 true = tt
      : Prop
 The command has indeed failed with message:
-Error: Extra arguments: _, _.
+Extra arguments: _, _.
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index b084ad4984..4df21ae353 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -1,5 +1,5 @@
 The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be specified.
+To rename arguments the "rename" flag must be specified.
 Argument A renamed to B.
 File "stdin", line 2, characters 0-25:
 Warning: This command is just asserting the names of arguments of identity.
@@ -103,15 +103,15 @@ Expands to: Constant Top.myplus
 @myplus
      : forall Z : Type, Z -> nat -> nat -> nat
 The command has indeed failed with message:
-Error: Argument lists should agree on the names they provide.
+Argument lists should agree on the names they provide.
 The command has indeed failed with message:
-Error: Sequences of implicit arguments must be of different lengths.
+Sequences of implicit arguments must be of different lengths.
 The command has indeed failed with message:
-Error: Some argument names are duplicated: F
+Some argument names are duplicated: F
 The command has indeed failed with message:
-Error: Argument z cannot be declared implicit.
+Argument z cannot be declared implicit.
 The command has indeed failed with message:
-Error: Extra arguments: y.
+Extra arguments: y.
 The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be specified.
+To rename arguments the "rename" flag must be specified.
 Argument A renamed to R.
diff --git a/test-suite/output/ErrorInModule.out b/test-suite/output/ErrorInModule.out
new file mode 100644
index 0000000000..776dfeb550
--- /dev/null
+++ b/test-suite/output/ErrorInModule.out
@@ -0,0 +1,3 @@
+File "stdin", line 3, characters 20-31:
+Error: The reference nonexistent was not found in the current environment.
+
diff --git a/test-suite/output/ErrorInModule.v b/test-suite/output/ErrorInModule.v
new file mode 100644
index 0000000000..e69e23276b
--- /dev/null
+++ b/test-suite/output/ErrorInModule.v
@@ -0,0 +1,4 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-quick") -*- *)
+Module M.
+  Definition foo := nonexistent.
+End M.
diff --git a/test-suite/output/ErrorInSection.out b/test-suite/output/ErrorInSection.out
new file mode 100644
index 0000000000..776dfeb550
--- /dev/null
+++ b/test-suite/output/ErrorInSection.out
@@ -0,0 +1,3 @@
+File "stdin", line 3, characters 20-31:
+Error: The reference nonexistent was not found in the current environment.
+
diff --git a/test-suite/output/ErrorInSection.v b/test-suite/output/ErrorInSection.v
new file mode 100644
index 0000000000..3036f8f05b
--- /dev/null
+++ b/test-suite/output/ErrorInSection.v
@@ -0,0 +1,4 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-quick") -*- *)
+Section S.
+  Definition foo := nonexistent.
+End S.
diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out
index 06a6b2d157..38d055b28e 100644
--- a/test-suite/output/Errors.out
+++ b/test-suite/output/Errors.out
@@ -7,4 +7,4 @@ In nested Ltac calls to "f" and "apply x", last call failed.
 Unable to unify "nat" with "True".
 The command has indeed failed with message:
 Ltac call to "instantiate ( (ident) := (lglob) )" failed.
-Error: Instance is not well-typed in the environment of ?x.
+Instance is not well-typed in the environment of ?x.
diff --git a/test-suite/output/FunExt.out b/test-suite/output/FunExt.out
index c6786c72ff..8d2a125c1d 100644
--- a/test-suite/output/FunExt.out
+++ b/test-suite/output/FunExt.out
@@ -16,4 +16,4 @@ Tactic failure: Already an intensional equality.
 The command has indeed failed with message:
 In nested Ltac calls to "extensionality in (var)" and
 "clearbody (ne_var_list)", last call failed.
-Error: Hypothesis e depends on the body of H'
+Hypothesis e depends on the body of H'
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 26eaca8272..9d106d2dac 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.
+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
+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:
 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
+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.
+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.
+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.
+Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-Error: Cannot find where the recursive pattern starts.
+Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-Error: Cannot find where the recursive pattern starts.
+Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-Error: Cannot find where the recursive pattern starts.
+Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-Error: Both ends of the recursive pattern are the same.
+Both ends of the recursive pattern are the same.
 SUM (nat * nat) nat
      : Set
 FST (0; 1)
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index ad60aeccce..1ec701ae81 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -32,7 +32,7 @@ let d := 2 in ∃ z : nat, let e := 3 in let f := 4 in x + y = z + d
      : Type -> Prop
 λ A : Type, ∀ n p : A, n = p
      : Type -> Prop
-let' f (x y : nat) (a:=0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2
+let' f (x y : nat) (a := 0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2
      : bool -> nat
 λ (f : nat -> nat) (x : nat), f(x) + S(x)
      : (nat -> nat) -> nat -> nat
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
new file mode 100644
index 0000000000..128bc77673
--- /dev/null
+++ b/test-suite/output/UnivBinders.out
@@ -0,0 +1,6 @@
+bar@{u} = nat
+     : Wrap@{u} Set
+(* u |= Set < u
+         *)
+
+bar is universe polymorphic
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
new file mode 100644
index 0000000000..d9e89e43c6
--- /dev/null
+++ b/test-suite/output/UnivBinders.v
@@ -0,0 +1,7 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+
+Class Wrap A := wrap : A.
+
+Instance bar@{u} : Wrap@{u} Set. Proof nat.
+Print bar.
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index 576fbd7c0b..e83e7176de 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -6,7 +6,7 @@ fun e : option L => match e with
      : option L -> option L
 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 : T n in ?y ?y0 : T n
+fun n : nat => let x : T n := A n in ?y ?y0 : T n
      : forall n : nat, T n
 where
 ?y : [n : nat  x := A n : T n |- ?T -> T n] 
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index 1ff09e3af6..35c3057d84 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -1,5 +1,4 @@
 The command has indeed failed with message:
-Error:
 Ltac variable y depends on pattern variable name z which is not bound in current context.
 Ltac f x y z :=
   symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize
@@ -22,11 +21,11 @@ The term "I" has type "True" while it is expected to have type "False".
 The command has indeed failed with message:
 In nested Ltac calls to "h" and "injection (destruction_arg)", last call
 failed.
-Error: No primitive equality found.
+No primitive equality found.
 The command has indeed failed with message:
 In nested Ltac calls to "h" and "injection (destruction_arg)", last call
 failed.
-Error: No primitive equality found.
+No primitive equality found.
 Hx
 nat
 nat
diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out
new file mode 100644
index 0000000000..172612405f
--- /dev/null
+++ b/test-suite/output/ltac_missing_args.out
@@ -0,0 +1,20 @@
+The command has indeed failed with message:
+A fully applied tactic is expected: missing argument for variable x.
+The command has indeed failed with message:
+A fully applied tactic is expected: missing argument for variable x.
+The command has indeed failed with message:
+A fully applied tactic is expected: missing arguments for variables y and _.
+The command has indeed failed with message:
+A fully applied tactic is expected: missing argument for variable x.
+The command has indeed failed with message:
+A fully applied tactic is expected: missing argument for variable x.
+The command has indeed failed with message:
+A fully applied tactic is expected: missing argument for variable _.
+The command has indeed failed with message:
+A fully applied tactic is expected: missing argument for variable _.
+The command has indeed failed with message:
+A fully applied tactic is expected: missing argument for variable _.
+The command has indeed failed with message:
+A fully applied tactic is expected: missing argument for variable x.
+The command has indeed failed with message:
+A fully applied tactic is expected: missing argument for variable x.
diff --git a/test-suite/output/ltac_missing_args.v b/test-suite/output/ltac_missing_args.v
new file mode 100644
index 0000000000..8ecd97aa56
--- /dev/null
+++ b/test-suite/output/ltac_missing_args.v
@@ -0,0 +1,19 @@
+Ltac foo x := idtac x.
+Ltac bar x := fun y _ => idtac x y.
+Ltac baz := foo.
+Ltac qux := bar.
+Ltac mydo tac := tac ().
+Ltac rec x := rec.
+
+Goal True.
+  Fail foo.
+  Fail bar.
+  Fail bar True.
+  Fail baz.
+  Fail qux.
+  Fail mydo ltac:(fun _ _ => idtac).
+  Fail let tac := (fun _ => idtac) in tac.
+  Fail (fun _ => idtac).
+  Fail rec True.
+  Fail let rec tac x := tac in tac True.
+Abort.
+\ No newline at end of file
diff --git a/test-suite/output/qualification.out b/test-suite/output/qualification.out
index 9300c3f546..e9c70d1efc 100644
--- a/test-suite/output/qualification.out
+++ b/test-suite/output/qualification.out
@@ -1,3 +1,4 @@
 File "stdin", line 19, 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".
+