diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
tree | 074182834cb406d1304aec4233718564a9c06ba1 /test-suite/bugs/closed/3777.v | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'test-suite/bugs/closed/3777.v')
-rw-r--r-- | test-suite/bugs/closed/3777.v | 17 |
1 files changed, 17 insertions, 0 deletions
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 -> _). |