8 files changed, 27 insertions, 2 deletions
diff --git a/test-suite/output/ErrorInModule.out b/test-suite/output/ErrorInModule.out
new file mode 100644
index 0000000000..851ecd9306
--- /dev/null
+++ b/test-suite/output/ErrorInModule.out
@@ -0,0 +1,2 @@
+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..851ecd9306
--- /dev/null
+++ b/test-suite/output/ErrorInSection.out
@@ -0,0 +1,2 @@
+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/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]