From 6a046f8d3e33701d70e2a391741e65564cc0554d Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 23 Jan 2016 15:55:43 -0500
Subject: Fix bug #4519: oops, global shadowed local universe level bindings.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4519.v b/test-suite/bugs/closed/4519.v
new file mode 100644
index 0000000000..ccbc47d20f
--- /dev/null
+++ b/test-suite/bugs/closed/4519.v
@@ -0,0 +1,21 @@
+Set Universe Polymorphism.
+Section foo.
+  Universe i.
+  Context (foo : Type@{i}) (bar : Type@{i}).
+  Definition qux@{i} (baz : Type@{i}) := foo -> bar.
+End foo.
+Set Printing Universes.
+Print qux. (* qux@{Top.42 Top.43} =
+fun foo bar _ : Type@{Top.42} => foo -> bar
+     : Type@{Top.42} -> Type@{Top.42} -> Type@{Top.42} -> Type@{Top.42}
+(* Top.42 Top.43 |=  *)
+(* This is wrong; the first two types are equal, but the last one is not *)
+
+qux is universe polymorphic
+Argument scopes are [type_scope type_scope type_scope]
+ *)
+Check qux nat nat nat : Set.
+Check qux nat nat Set : Set. (* Error:
+The term "qux@{Top.50 Top.51} ?T ?T0 Set" has type "Type@{Top.50}" while it is 
+expected to have type "Set"
+(universe inconsistency: Cannot enforce Top.50 = Set because Set < Top.50). *)
\ No newline at end of file
-- 
cgit v1.2.3