aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/opened/3682.v
blob: 71baf78cf21a9359b1733d0415063515194f315f (plain)
1
2
3
4
5
Class Foo.
Definition bar `{Foo} (x : Set) := Set.
Instance: Foo.
Definition bar1 := bar nat.
Fail Definition bar2 := bar $(admit)$.