The Coq mailing list

[Victor Porton <porton AT narod.ru>]

The following does not verify, because in some reason Coq does not do a 
coercion from Derived to Base.

Maybe it is an intended behavior but for me it seems like a conceptual error 
in Coq type classes.

Please comment.

[[[[
Class Base := {
  n: nat
}.

Class Derived := {
  base :> Base
}.

Definition test (derived: Derived) := @n derived.
]]]]

-- 
Victor Porton - http://portonvictor.org