aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_4046.v
blob: c33e2b9febcd29f0448ee4990da657ebd7afd309 (plain)
1
2
3
4
5
6
Module Import Foo.
  Class Foo := { foo : Type }.
End Foo.

Instance f : Foo := { foo := nat }. (* works fine *)
Instance f' : Foo.Foo := { Foo.foo := nat }.