From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Fri, 13 Nov 2015 11:31:34 +0100
Subject: Imported Upstream version 8.5~beta3+dfsg

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

(limited to 'test-suite/bugs/closed/3777.v')

diff --git a/test-suite/bugs/closed/3777.v b/test-suite/bugs/closed/3777.v
new file mode 100644
index 00000000..e203528f
--- /dev/null
+++ b/test-suite/bugs/closed/3777.v
@@ -0,0 +1,17 @@
+Unset Strict Universe Declaration.
+Module WithoutPoly.
+  Unset Universe Polymorphism.
+  Definition foo (A : Type@{i}) (B : Type@{i}) := A -> B.
+  Set Printing Universes.
+  Definition bla := ((@foo : Set -> _ -> _) : _ -> Type -> _).
+  (* ((fun A : Set => foo A):Set -> Type@{Top.55} -> Type@{Top.55})
+:Set -> Type@{Top.55} -> Type@{Top.55}
+     : Set -> Type@{Top.55} -> Type@{Top.55}
+(*  |= Set <= Top.55
+         *) *)
+End WithoutPoly.
+Module WithPoly.
+  Set Universe Polymorphism.
+  Definition foo (A : Type@{i}) (B : Type@{i}) := A -> B.
+  Set Printing Universes.
+  Fail Check ((@foo : Set -> _ -> _) : _ -> Type -> _).
-- 
cgit v1.2.3