From 739d8e50b3681491bd82b516dbbba892ac5b424b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 2 Nov 2015 13:48:53 -0500
Subject: Refresh rigid universes as well, and in 8.4 compatibility mode, make
 them rigid to disallow minimization.

---
 test-suite/bugs/closed/4394.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 test-suite/bugs/closed/4394.v

(limited to 'test-suite')

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
-- 
cgit v1.2.3