2 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/output/bug6821.out b/test-suite/output/bug6821.out
new file mode 100644
index 000000000..7b12b5320
--- /dev/null
+++ b/test-suite/output/bug6821.out
@@ -0,0 +1,2 @@
+forall f : nat -> Type, f x where x : nat := 1
+     : Type
diff --git a/test-suite/output/bug6821.v b/test-suite/output/bug6821.v
new file mode 100644
index 000000000..40627e331
--- /dev/null
+++ b/test-suite/output/bug6821.v
@@ -0,0 +1,8 @@
+(* Was failing at printing time with stack overflow due to an infinite
+   eta-expansion *)
+
+Notation "x 'where' y .. z := v " :=
+  ((fun y => .. ((fun z => x) v) ..) v)
+  (at level 11, v at next level, y binder, z binder).
+
+Check forall f, f x where x := 1.