1 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4394.v b/test-suite/bugs/closed/4394.v
new file mode 100644
index 0000000000..751f1e697d
--- /dev/null
+++ b/test-suite/bugs/closed/4394.v
@@ -0,0 +1,13 @@
+(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+Require Import Equality List.
+Unset Strict Universe Declaration.
+Inductive Foo I A := foo (B : Type) : A -> I B -> Foo I A.
+Definition Family := Type -> Type.
+Definition fooFamily family : Family := Foo family.
+Inductive Empty {T} : T -> Prop := .
+Theorem empty (family : Family) (a : fold_right prod unit (map (Foo family) nil)) (b : unit) :
+  Empty (a, b) -> False.
+Proof.
+  intro e.
+  dependent induction e.
+Qed.
+\ No newline at end of file