The Coq mailing list

[Richard.Dapoigny AT univ-savoie.fr]

Hi all,
I have some problem with operational type classes. Consider the  
following fragment:

Class N       := nn :> Type.
Class singular.
Parameter M1 : singular -> N. Coercion M1 : singular >-> N.
Class plural.
Parameter M2 : plural -> N. Coercion M2 : plural >-> N.
Class empty.
Parameter M3 : empty -> N. Coercion M3 : empty >-> N.

Parameter Association : relation N.

Parameter is_one_of : relation N. (* argument filtering on the relation *)
Class epsilon (A:singular)(b:N) := eps :> is_one_of A b.

Class LO_exist_at_least (a:singular){A:singular}{e:epsilon A a}.
Variable A    : singular.
Variable B    : singular.
Variable ert  : epsilon A B.
Variable ert' : epsilon B A.
Variable e1   : empty.
Variable p1   : plural.
Variable ert1 : epsilon A p1.
Variable d1   : LO_exist_at_least_plural B.

with the following error:
Error:
Unable to satisfy the following constraints:
?67 : "epsilon ?66 B"
?66 : "singular"

However, it works with A. Is anybody has an idea?
Thanks in advance,
Richard