From ff0a051caf031fb427007714f6325c74b8893702 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 22 Nov 2014 19:34:25 +0100
Subject: Pass around information on the use of template polymorphism for
 inductive types (i.e., ones declared with an explicit anonymous Type at the
 conclusion of their arity). With this change one can force inductives to live
 in higher universes even in the non-fully universe polymorphic case (e.g. bug
 #3821).

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3821.v b/test-suite/bugs/closed/3821.v
new file mode 100644
index 0000000000..8da4f73626
--- /dev/null
+++ b/test-suite/bugs/closed/3821.v
@@ -0,0 +1,2 @@
+Inductive quotient {A : Type@{i}} {B : Type@{j}} : Type@{max(i, j)} := .
+
-- 
cgit v1.2.3