From 96760d8516398ecfa55e4e6f808dd6aa5305e483 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 24 Sep 2015 17:57:37 +0200
Subject: Fix test-suite file for bug #3777

---
 test-suite/bugs/closed/3777.v | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 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 0000000000..b9b2dd6b3e
--- /dev/null
+++ b/test-suite/bugs/closed/3777.v
@@ -0,0 +1,16 @@
+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