diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-29 12:13:28 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-29 14:57:12 +0200 |
| commit | cc0dc21e24c2cd45cd1c6723fcd524e6db89f7bd (patch) | |
| tree | d4a275e5be4cf0003b995658cd90832744434899 /test-suite/bugs/closed/3453.v | |
| parent | 9ba2016b81b6ce1d6f024ce674375f7ed54bae85 (diff) | |
Add test-suite file for bug #3453
Diffstat (limited to 'test-suite/bugs/closed/3453.v')
| -rw-r--r-- | test-suite/bugs/closed/3453.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3453.v b/test-suite/bugs/closed/3453.v new file mode 100644 index 000000000..4ee9b400a --- /dev/null +++ b/test-suite/bugs/closed/3453.v @@ -0,0 +1,10 @@ +Set Primitive Projections. +Record Foo := { bar : Set }. +Class Baz (F : Foo) := { qux : F.(bar) }. +Coercion qux : Baz >-> bar. + +Definition f : Foo := {| bar := nat |}. +Canonical Structure f. +Check (fun b : Baz f => b : _.(bar)). + +(* Error: Found target class bar instead of bar. *) |