2 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 04bd169bd..a2857294b 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -53,6 +53,8 @@ Monomorphic mono = Type@{u}
 (* {u} |=  *)
 
 mono is not universe polymorphic
+The command has indeed failed with message:
+Universe u already bound.
 foo@{E M N} = 
 Type@{M} -> Type@{N} -> Type@{E}
      : Type@{max(E+1, M+1, N+1)}
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index f0a990986..013f215b5 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -34,6 +34,9 @@ Print foo.
 Monomorphic Definition mono@{u} := Type@{u}.
 Print mono.
 
+(* fun x x => foo is nonsense with local binders *)
+Fail Definition fo@{u u} := Type@{u}.
+
 (* Using local binders for printing. *)
 Print foo@{E M N}.
 (* Underscores discard the name if there's one. *)