diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-09-30 18:13:28 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2015-10-02 15:54:12 +0200 |
| commit | 856a61c1b3c5ee2b4dec08809e5e916d8954d5f8 (patch) | |
| tree | a48404d0b0d8f8fba653b2dddc8be7f1e342ebe8 /test-suite/bugs/closed/4301.v | |
| parent | 0adf0838a59a3fbca1ced05243ccc42c969fcf18 (diff) | |
Univs: test-suite file for #4301, subtyping of poly parameters
Diffstat (limited to 'test-suite/bugs/closed/4301.v')
| -rw-r--r-- | test-suite/bugs/closed/4301.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4301.v b/test-suite/bugs/closed/4301.v new file mode 100644 index 000000000..1a8d3611b --- /dev/null +++ b/test-suite/bugs/closed/4301.v @@ -0,0 +1,19 @@ +Set Universe Polymorphism. + +Module Type Foo. + Parameter U : Type. +End Foo. + +(* Module Lower (X : Foo). *) +(* Definition U' : Prop := X.U@{Prop}. *) +(* End Lower. *) +(* Module Lower (X : Foo with Definition U := Prop). *) +(* Definition U' := X.U@{Prop}. *) +(* End Lower. *) +Module Lower (X : Foo with Definition U := True). + (* Definition U' : Prop := X.U. *) +End Lower. + +Module M : Foo. + Definition U := nat : Type@{i}. +End M. |