diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-09-24 17:57:37 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2015-10-02 15:54:12 +0200 |
| commit | 96760d8516398ecfa55e4e6f808dd6aa5305e483 (patch) | |
| tree | dba9a9750904ffba00345a65aa305064f60cc1a7 /test-suite/bugs | |
| parent | e51f708ac911f376f09297cad7d7d27510fe8990 (diff) | |
Fix test-suite file for bug #3777
Diffstat (limited to 'test-suite/bugs')
| -rw-r--r-- | test-suite/bugs/closed/3777.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3777.v b/test-suite/bugs/closed/3777.v new file mode 100644 index 000000000..b9b2dd6b3 --- /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 -> _). |